diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index fd2e1efdb58b118c0c69e36537920a140a18a2d1..21262934a3fdd8090525e4a991d12d1e3030a98e 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -5,8 +5,10 @@
 
 open CoAlgMisc
 
+module S = MiscSolver
 
-let mkRule_MultiModalK sort bs sl =
+(** directly return a list of rules **)
+let mkRuleList_MultiModalK sort bs sl =
   assert (List.length sl = 1);
   let dep f bsl =                 (* dependencies for formula f *)
     assert (List.length bsl = 1); (* -+                 *)
@@ -52,7 +54,10 @@ let mkRule_MultiModalK sort bs sl =
               | "∃R.C" ∈ bs
               }
   *)
-  let rules = bsetFold getRules bs [] in
+  bsetFold getRules bs []
+
+let mkRule_MultiModalK sort bs sl =
+  let rules = mkRuleList_MultiModalK sort bs sl in
   let res = ref (Some rules) in
   fun () ->
     match !res with
@@ -61,8 +66,46 @@ let mkRule_MultiModalK sort bs sl =
         res := None;
         AllInOne rules
 
+(* TODO: test it with:
+     make && ./coalg sat <<< $'<R> False \n [R] False \n [R] True'
+*)
 let mkRule_MultiModalKD sort bs sl =
-  let rules = bsetFold getRules bs [] in
+  assert (List.length sl = 1); (* TODO: Why? *)
+  let roles = S.makeBS () in
+  (* step 1: for each ∀R._ add R *)
+  let addRoleIfBox formula =
+    if lfGetType sort formula = ExF then
+      ignore (S.addBS roles (lfGetDest3 sort formula))
+    else ()
+  in
+  bsetIter (addRoleIfBox) bs;
+  (* step 2: for each ∃R._ remove R again from roles (optimization) *)
+  let rmRoleIfDiamond formula =
+    if lfGetType sort formula = ExF then
+      S.remBS roles (lfGetDest3 sort formula)
+    else ()
+  in
+  bsetIter (rmRoleIfDiamond) bs;
+  (* 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;
+    in
+    acc
+  in
+  (*
+    mkRule_MultiModalKD sort bs [s1]
+        = { (λ[bs1]. { ∀R.D ∈ bs | D ∈ bs1}
+            , [(s1, {D | "∀R.D" ∈ bs)]
+            )
+          | R ∈ signature(bs) (or R ∈ roles)
+          }
+          ∪ mkRule_MultiModalK sort bs [s1]
+  *)
+  let rules = mkRuleList_MultiModalK sort bs sl in
+  (* extend rules from K with enforcing of successors *)
+  let rules = S.foldBS getRules roles rules in
+  (* TODO: replace cannonical wrapper by helper function *)
   let res = ref (Some rules) in
   fun () ->
     match !res with
@@ -146,7 +189,7 @@ let mkRule_Fusion sort bs sl =
    "plug-in" function.
  *)
 let getExpandingFunctionProducer = function
-  | MultiModalK -> mkRule_MultiModalK
   | MultiModalK -> mkRule_MultiModalKD
+  | MultiModalKD -> mkRule_MultiModalKD
   | Choice -> mkRule_Choice
   | Fusion -> mkRule_Fusion
diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index d856373d4a36a51c721cc9f4b17a7a5ed486f7d9..16fef0d5366fb775a2e4a62737f7473f476ed308 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -421,6 +421,7 @@ let tboxTable = ref (Array.make 0 S.dummyBS)
 let bsetMake () = S.makeBS ()
 let bsetAdd bs lf = S.addBSNoChk bs lf
 let bsetMem bs lf = S.memBS bs lf
+let bsetRem bs lf = S.remBS bs lf
 let bsetFold fkt bs init = S.foldBS fkt bs init
 let bsetIter fkt bset = S.iterBS fkt bset
 let bsetAddTBox sort bs = S.unionBSNoChk bs !tboxTable.(sort)