From 2a84977e76cdced261fac446be7cc4041dd07557 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Tue, 17 Dec 2013 22:57:31 +0100
Subject: [PATCH] Implement complete KD rule
---
CoAlgLogics.ml | 28 ++++++++++++++++++++++++----
CoAlgMisc.ml | 5 +++--
2 files changed, 27 insertions(+), 6 deletions(-)
diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index 2126293..81059d4 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -71,10 +71,11 @@ let mkRule_MultiModalK sort bs sl =
*)
let mkRule_MultiModalKD sort bs sl =
assert (List.length sl = 1); (* TODO: Why? *)
+ let s1 = List.hd sl in (* [s1] = List.hd sl *)
let roles = S.makeBS () in
(* step 1: for each ∀R._ add R *)
let addRoleIfBox formula =
- if lfGetType sort formula = ExF then
+ if lfGetType sort formula = AxF then
ignore (S.addBS roles (lfGetDest3 sort formula))
else ()
in
@@ -89,9 +90,28 @@ let mkRule_MultiModalKD sort bs sl =
(* step 3: for each R in roles enforce one successor *)
let getRules r acc = (* add the rule for a concrete R *)
let dep r bsl =
- bsetIter (rmRoleIfDiamond) bs;
+ assert (List.length bsl = 1); (* -+ *)
+ let bs1 = List.hd bsl in (* -+-> [bs1] := bsl *)
+ let res = bsetMake () in (* res := { ∀R.D ∈ bs | D ∈ bs1} *)
+ let f formula =
+ if lfGetType sort formula = AxF
+ && lfGetDest3 sort formula = r
+ && bsetMem bs1 (lfGetDest1 sort formula)
+ then ignore (bsetAdd res formula)
+ else ()
+ in
+ bsetIter f bs; (* fill res *)
+ res
+ in
+ let succs = bsetMake () in (* succs := {D | ∀r.D ∈ bs *)
+ let f formula =
+ if lfGetType sort formula = AxF
+ && lfGetDest3 sort formula = r
+ then ignore (bsetAdd succs (lfGetDest1 sort formula))
+ else ()
in
- acc
+ bsetIter f bs;
+ (dep r, [(s1, succs)])::acc
in
(*
mkRule_MultiModalKD sort bs [s1]
@@ -189,7 +209,7 @@ let mkRule_Fusion sort bs sl =
"plug-in" function.
*)
let getExpandingFunctionProducer = function
- | MultiModalK -> mkRule_MultiModalKD
+ | MultiModalK -> mkRule_MultiModalK
| MultiModalKD -> mkRule_MultiModalKD
| Choice -> mkRule_Choice
| Fusion -> mkRule_Fusion
diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index 16fef0d..c439c12 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -532,8 +532,9 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
detClosure nomTbl hcF fset atset nomset s f2
| C.HCEX (_, f1)
| C.HCAX (_, f1) ->
- if func <> MultiModalK || List.length sortlst <> 1 then
- raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
+ if (func <> MultiModalK && func <> MultiModalKD)
+ || List.length sortlst <> 1
+ then raise (C.CoAlgException "Ex/Ax-formula is used in wrong sort.")
else ();
detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
| C.HCMIN _
--
GitLab