Implement complete KD rule

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

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 _