diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml index 58b3492a76c2214111297eb69cb8e6cef111aa97..d4b321b7ae10e98b1d1e2d7a9be2dff627f0e04d 100644 --- a/src/lib/CoAlgLogics.ml +++ b/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 = diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml index 6e92013100f619c1af73f83c22fdd71d1cfc40e4..35b4b3f9ed3fed05d4035bc5d621c95a260d9f35 100644 --- a/src/testsuite/cool-testsuite.ml +++ b/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