From edfbcc2b0cd836fc387efc158750842a72fe4d86 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Sat, 14 May 2016 23:48:25 +0200
Subject: [PATCH] Fix deferral tracking for new CoalitionLogic code
---
src/lib/CoAlgLogics.ml | 19 ++++++++++++++-----
1 file changed, 14 insertions(+), 5 deletions(-)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 71d9318..fd46280 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -410,8 +410,10 @@ let mkRule_CL sort bs defer sl : stateExpander =
(* 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 []
+ let a_i : (localFormula * bool) list =
+ bsetFold (fun f a -> let nextf = lfGetDest1 sort f in
+ (nextf, (deferral_tracking f nextf))::a)
+ coalitions []
in
(* now do rule 2:
coalitions /\ nCands
@@ -419,9 +421,16 @@ let mkRule_CL sort bs defer sl : stateExpander =
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
+ let defer1 = bsetMakeRealEmpty () in
+ List.iter (fun (f, isdefer) ->
+ bsetAdd children f;
+ if isdefer then bsetAdd defer1 f)
+ c_j ;
+ List.iter (fun (f, isdefer) ->
+ bsetAdd children f;
+ if isdefer then bsetAdd defer1 f)
+ a_i ;
+ ((fun bs1 -> bs), lazylistFromList [(s1, children, defer1)])::acc
in
List.fold_left createSingleRule acc maxdisj
end else acc
--
GitLab