Skip to content
Snippets Groups Projects
Commit edfbcc2b authored by Christoph's avatar Christoph
Browse files

Fix deferral tracking for new CoalitionLogic code

parent 3e2aa1b8
No related branches found
No related tags found
No related merge requests found
...@@ -410,8 +410,10 @@ let mkRule_CL sort bs defer sl : stateExpander = ...@@ -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 *) (* create rule 2 once for all the diamonds with a full agent set *)
let maxdisj = maxDisjoints sort boxes in let maxdisj = maxDisjoints sort boxes in
let createSingleRule acc coalitions = let createSingleRule acc coalitions =
let a_i : localFormula list = let a_i : (localFormula * bool) list =
bsetFold (fun f a -> (lfGetDest1 sort f)::a) coalitions [] bsetFold (fun f a -> let nextf = lfGetDest1 sort f in
(nextf, (deferral_tracking f nextf))::a)
coalitions []
in in
(* now do rule 2: (* now do rule 2:
coalitions /\ nCands coalitions /\ nCands
...@@ -419,9 +421,16 @@ let mkRule_CL sort bs defer sl : stateExpander = ...@@ -419,9 +421,16 @@ let mkRule_CL sort bs defer sl : stateExpander =
a_i /\ c_j a_i /\ c_j
*) *)
let children = bsetMakeRealEmpty () in let children = bsetMakeRealEmpty () in
List.iter (bsetAdd children) (c_j) ; let defer1 = bsetMakeRealEmpty () in
List.iter (bsetAdd children) (a_i) ; List.iter (fun (f, isdefer) ->
((fun bs1 -> bs), lazylistFromList [(s1, children)])::acc 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 in
List.fold_left createSingleRule acc maxdisj List.fold_left createSingleRule acc maxdisj
end else acc end else acc
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment