Fix testcase for K*KD and add K+KD cases

src/testsuite/cool-testsuite.ml

@@ -10,14 +10,6 @@ let k   = [| (CM.MultiModalK,  [0]) |]
 let kd  = [| (CM.MultiModalKD, [0]) |]
 let cl  = [| (CM.CoalitionLogic, [0]) |]
 let gml = [| (CM.GML, [0]) |]
-let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
-               (CoAlgMisc.MultiModalK, [0]);
-               (CoAlgMisc.MultiModalKD, [0])
-            |]
-let kAndKd = [| (CoAlgMisc.Fusion, [1; 2]);
-                (CoAlgMisc.MultiModalK, [0]);
-                (CoAlgMisc.MultiModalKD, [0])
-             |]
 
 let k_testcases: satCheck list =
     let c a b = (a,k,b) in
@@ -72,6 +64,11 @@ let cl_testcases : satCheck list =
     ; c Sat   "([{1 3}] C) & ([{ 2 3 }] ~C )"
     ]
 
+let kAndKd = [| (CoAlgMisc.Fusion, [1; 2]);
+                (CoAlgMisc.MultiModalK, [0]);
+                (CoAlgMisc.MultiModalKD, [0])
+             |]
+
 let kAndKd_testcases : satCheck list =
     let c a b = (a,kAndKd,b) in
     [ c Sat   "[pi1]True"
@@ -79,7 +76,18 @@ let kAndKd_testcases : satCheck list =
     ; c Unsat "[pi2][R]False"
     ; c Sat   "i' => [pi1][R] i'"
     ; c Sat   "i' & [pi1][R] i'"
-    ; c Unsat "i' => [pi2][R] (~i') |- i' & [pi2] [R] i"
+    ; c Unsat "i' => [pi2][R] (~i') |- i' & [pi2] [R] i'"
+    ]
+
+let kOrKd = [| (CoAlgMisc.Choice, [1; 2]);
+               (CoAlgMisc.MultiModalK, [0]);
+               (CoAlgMisc.MultiModalKD, [0])
+            |]
+let kOrKd_testcases : satCheck list =
+    let c a b = (a,kOrKd,b) in
+    [ c Sat   "( True + False )"
+    ; c Sat   "(([R] False) + ([R] False))"
+    ; c Unsat "((False) + ([R] False))"
     ]
 
 let testcases =
@@ -91,6 +99,7 @@ let testcases =
     ; c "KD" kd_testcases
     ; c "CL" cl_testcases
     ; c "K×KD" kAndKd_testcases
+    ; c "K+KD" kOrKd_testcases
     ]
 
 let main =