diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml index 71d93189a3245b4a3db82f7921b5c849025894e4..fd46280ae2faeba53026db0dc5be8ff2cccccaf3 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