Regression tests

lib/tests/testsuite/cool_testsuite.ml

@@ -20,6 +20,8 @@ let k_testcases onestep =
     ; unsat      "<x> (<s> False) | <r> ((<r> c) & (<s> False))"
     ; unsat      "<x> (<s> False) | <r> ((<r> c) & (<s> False))"
     ; sat        "<r> a & <r> b |- [r] c"
+    ; sat        "< > a & < > b |- [ ] c"
+    ; sat        "<r> a <=> [r]b"
     ; unsat      "<r> a & <r> b |- [r] (~a & ~b)"
     ; unsat      "<r> a & <r> b |- [r] ~b"
     ; sat        "<r> a & <r> ~a |- [r] b"
@@ -188,10 +190,6 @@ let testcases =
   ; "K-mu (aconjunctive fragment)" >::: aconjunctive_testcases
   ; "GML" >::: gml_testcases
   ; "Properties" >::: [prop_onestepFunc_tableau_K]
-  (*
-  ; "K onestep mulitmod" >::: k_onestepFunc
-  ; "K tableau multimod" >::: k_onestepTab
-  *)
   ]
 ;;