CL: create enough rule 2 applications

The previous optimization in the rule 2 applications of coalition logic
left out some rule applications. Now, do enough but still do not
generate unnecessarily many rule applications.

src/lib/CoAlgLogics.ml

@@ -262,10 +262,13 @@ let mkRule_CL sort bs sl : stateExpander =
   in
   let rules = bsetFold getRule2 dCands [] in
   let getRule2ForFullAgents acc =
-    (* if there are N-diamonds but no diamonds with a proper subset of the agents,
-       then we need an explicit rule 2
+    (* So far, we only applied rule 2 for D a proper subset of N.
+       We still need rule 2 for D=N and b=c_j for some j. (Or equivalently we
+       apply rule2 without the <d> b).
+       If there are not N formulas, we don't need to do this because the
+       created rule 2 applications are just the rule 1 applications.
     *)
-    if not !nCandsEmpty && !dCandsEmpty then begin
+    if not !nCandsEmpty then begin
         (* create rule 2 once for all the diamonds with a full agent set *)
         let maxdisj = maxDisjoints sort boxes in
         let createSingleRule acc coalitions =

src/testsuite/cool-testsuite.ml

@@ -79,6 +79,14 @@ let cl_testcases : testcase_section =
     ; sat   "([{1 3}] C) & ([{ 2 3 }] ~C )"
     ]
 
+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 "[{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))"
+    ]
+
 let kAndKd_testcases : testcase_section =
     use_functor "K * KD" __
     [ sat   "[pi1]True"
@@ -122,6 +130,7 @@ let testcases =
     ; c "Nominals" nominal_testcases
     ; c "KD" kd_testcases
     ; cl_testcases
+    ; cl_testcases_2agents
     ; kAndKd_testcases
     ; kAndK_testcases
     ; c "K+KD" kOrKd_testcases