From c1a08c365e55349509f44a2c98160524adbc1a23 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Thu, 11 Feb 2016 17:08:38 +0100
Subject: [PATCH] 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 | 9 ++++++---
src/testsuite/cool-testsuite.ml | 9 +++++++++
2 files changed, 15 insertions(+), 3 deletions(-)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 58b3492..d4b321b 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 6e92013..35b4b3f 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
--
GitLab