Add testcases for K×KD (i.e. for fusion)

src/testsuite/cool-testsuite.ml

@@ -10,6 +10,14 @@ 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
@@ -64,6 +72,16 @@ let cl_testcases : satCheck list =
     ; c Sat   "([{1 3}] C) & ([{ 2 3 }] ~C )"
     ]
 
+let kAndKd_testcases : satCheck list =
+    let c a b = (a,kAndKd,b) in
+    [ c Sat   "[pi1]True"
+    ; c Sat   "[pi1][R]False"
+    ; 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"
+    ]
+
 let testcases =
     let c name table = (name,table) in
     [ c "DL98 (Sat)"    DL98.satCasesList
@@ -72,6 +90,7 @@ let testcases =
     ; c "Nominals" nominal_testcases
     ; c "KD" kd_testcases
     ; c "CL" cl_testcases
+    ; c "K×KD" kAndKd_testcases
     ]
 
 let main =