CL: more test formulas

src/testsuite/cool-testsuite.ml

@@ -74,15 +74,19 @@ let cl_testcases : testcase_section =
     ; sat   "[{1}] C & <{ 2 }> ~C"
     ; unsat "[{1}] C & <{ 1 2 }> ~C"
     ; sat   "<{ 1 2 }> C & <{ 1 2 }> ~C"
+    ; sat   "~([{ }] ~ phi <=>  ~ [{1 2}] phi)"
     ; unsat "<{ 1 2 }> C & [{ 1 2 }] ~C"
     ; unsat "<{ 1 2 3 4 5 }> C & <{ 1 2 3 4 5 }> ~C"
     ; sat   "([{1 3}] C) & ([{ 2 3 }] ~C )"
+    ; unsat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & ([{}](~(p1 | ~p2)) | [{}](~(p1 | ~p4))) & [{}](~(p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
+    ; sat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & (~[{1 2 }]((p1 | ~p2)) | ~[{1 2}]((p1 | ~p4))) & ~[{1 2}]((p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
     ]
 
 let cl_testcases_2agents : testcase_section =
     use_functor "CL" (fun () -> CoolUtils.cl_set_agents [|1;2|])
     [ unsat "[{1}] C & [{ 2 }] ~C"
     ; unsat "<{ 1 2 }> C & <{ 1 2 }> ~C"
+    ; unsat "~([{ }] ~ phi <=>  ~ [{1 2}] phi)"
     ; unsat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & ([{}](~(p1 | ~p2)) | [{}](~(p1 | ~p4))) & [{}](~(p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
     ; unsat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & (~[{1 2 }]((p1 | ~p2)) | ~[{1 2}]((p1 | ~p4))) & ~[{1 2}]((p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
     ]