From 9609611d6dd84656e00411548015b5f9881c65da Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Fri, 5 Feb 2016 14:00:14 +0100
Subject: [PATCH] Fix CL for diamond formula sets with all agents
For the case of two (or more) diamond formulas who all mention the full
agent list, no rule was created, because the former CL algorithm only
created rules for proper subsets of the agent list. This adds the
missing rule and lets cool correctly answer the following query:
$ ./coalg.native sat CL --agents '1' <<< '(~[{1}] p) & ~[{1}] ~p'
unsatisfiable
---
src/lib/CoAlgLogics.ml | 41 ++++++++++++++++++++++++++++++++-
src/testsuite/Testsuite.ml | 2 +-
src/testsuite/cool-testsuite.ml | 1 +
3 files changed, 42 insertions(+), 2 deletions(-)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index c7f4a37..58b3492 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -209,18 +209,32 @@ let mkRule_CL sort bs sl : stateExpander =
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
let disjoints = maxDisjoints sort boxes in
(*print_endline ("disjoints: "^(string_of_coalition_list sort disjoints)); *)
+ let nCandsEmpty = ref (true) in
let nCands = bsetMakeRealEmpty () in (* all N-diamonds *)
+ let dCandsEmpty = ref (true) in
let hasFullAgentList formula =
let aglist = lfGetDestAg sort formula in
let value = TArray.all (fun x -> TArray.elem x aglist) (cl_get_agents ()) in
- if (value) then bsetAdd nCands formula else () ;
+ if (value) then
+ begin
+ bsetAdd nCands formula;
+ nCandsEmpty := false
+ end
+ else dCandsEmpty := false;
value
in
(* Candidates for D in Rule 2 *)
+ (* implicitly fill nCands *)
let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
+ (*
+ print_endline ("For set " ^(CoAlgMisc.bsetToString sort bs));
+ print_endline ("N-Cands: " ^(CoAlgMisc.bsetToString sort nCands));
+ print_endline ("D-Cands: " ^(CoAlgMisc.bsetToString sort dCands));
+ *)
let c_j : localFormula list =
bsetFold (fun f a -> (lfGetDest1 sort f)::a) nCands []
in
+ (* rule 2 for diamaonds where D is a proper subset of the agent set N *)
let getRule2 diamDb acc = (* diamDb = <D> b *)
(* print_endline "Rule2" ; *)
let d = lfGetDestAg sort diamDb in (* the agent list *)
@@ -247,6 +261,31 @@ let mkRule_CL sort bs sl : stateExpander =
List.fold_left createSingleRule acc maxdisj
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
+ *)
+ if not !nCandsEmpty && !dCandsEmpty 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 =
+ let a_i : localFormula list =
+ bsetFold (fun f a -> (lfGetDest1 sort f)::a) coalitions []
+ in
+ (* now do rule 2:
+ coalitions /\ nCands
+ ———————————————————————
+ a_i /\ c_j
+ *)
+ let children = bsetMakeRealEmpty () in
+ List.iter (bsetAdd children) (c_j) ;
+ List.iter (bsetAdd children) (a_i) ;
+ ((fun bs1 -> bs), lazylistFromList [(s1, children)])::acc
+ in
+ List.fold_left createSingleRule acc maxdisj
+ end else acc
+ in
+ let rules = getRule2ForFullAgents rules in
let getRule1 acc coalitions =
(* print_endline "Rule1" ; *)
(* do rule 1:
diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index 63fb1fd..9074919 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -62,7 +62,7 @@ let runSatCheckVerbose (sc:satCheck) =
let res = runSatCheck sc in
(if (res = expectation)
then PF.printf "%s\n" (cs "1;32" "Yes")
- else PF.printf "%s, it is %s\n"
+ else PF.printf "%s, cool claims it is %s\n"
(cs "1;31" "No")
(sotr res));
flush stdout;
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 3e94b75..6bab2be 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -74,6 +74,7 @@ let cl_testcases : testcase_section =
; unsat "[{1}] C & <{ 1 2 }> ~C"
; sat "<{ 1 2 }> C & <{ 1 2 }> ~C"
; 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 )"
]
--
GitLab