Add more testcases for K

src/testsuite/Testsuite.ml

@@ -56,7 +56,7 @@ let runSatCheckVerbose (sc:satCheck) =
     let cs = colored_string in
     let sotr = terminal_string_of_testResult in
     let (expectation,_,title) = sc in
-    PF.printf "Is %s " (cs "1" (columnCreate 50 title));
+    PF.printf "Is %s " (cs "1" (columnCreate 60 title));
     PF.printf "%s? → " (sotr expectation);
     let res = runSatCheck sc in
     (if (res = expectation)

src/testsuite/cool-testsuite.ml

@@ -23,8 +23,15 @@ let k_testcases: satCheck list =
     ; c Unsat "<R> ((<R> C) & (<S> False))"
     ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
     ; c Unsat "<X> (<S> False) | <R> ((<R> C) & (<S> False))"
-
-    (* Some DL98-Testcases *)
+    ; c Sat   "<R> A & <R> B |- [R] C"
+    ; c Unsat "<R> A & <R> B |- [R] (~A & ~B)"
+    ; c Unsat "<R> A & <R> B |- [R] ~B"
+    ; c Sat   "<R> A & <R> ~A |- [R] B"
+    ; c Unsat "<R> A & <R> ~A & (B => [R] ~A) |- [R] B"
+    ; c Sat   "<R> A & <R> ~A & (B => [R] ~A) & (C => ~D) & (D => ~E) & <R> C & <R> D & <R> E |- True"
+    ; c Unsat "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
+    ; c Sat   "(<R> D | <R> E) & ((<R> D & <R> E) => [R] E) & ~(D & E) |- True"
+    ; c Sat   "<R> D & <R> E & ((<R> D & <R> E) => [R] E) & (D & E => <R> ~(D&E)) |- True"
     ]