Add deferral tracking to CoalitionLogic

src/lib/CoAlgLogics.ml

@@ -322,7 +322,11 @@ let compatible sort (a: bset) formula1 =
 
 let mkRule_CL sort bs defer sl : stateExpander =
   assert (List.length sl = 1); (* TODO: Why? *)
-  let defer1 = bsetMake () in (* TODO: track deferrals *)
+  let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
+  let deferral_tracking f nextf =
+    (refocusing && (lfGetDeferral sort nextf) != (Hashtbl.hash "ε")) ||
+      ((bsetMem defer f) && (lfGetDeferral sort f) = (lfGetDeferral sort nextf))
+  in
   let s1 = List.hd sl in (* [s1] = List.hd sl *)
   let boxes = bsetFilter bs (fun f -> lfGetType sort f = EnforcesF) in
   let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
@@ -337,8 +341,11 @@ let mkRule_CL sort bs defer sl : stateExpander =
   in
   (* Candidates for D in Rule 2 *)
   let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
-  let c_j : localFormula list =
-    bsetFold (fun f a -> (lfGetDest1 sort f)::a) nCands []
+  let c_j : (localFormula * bool) list =
+    bsetFold (fun f a ->
+              let nextf = lfGetDest1 sort f in
+              (nextf, (deferral_tracking f nextf))::a)
+             nCands []
   in
   let getRule2 diamDb acc = (* diamDb = <D> b *)
     (* print_endline "Rule2" ; *)
@@ -350,8 +357,11 @@ let mkRule_CL sort bs defer sl : stateExpander =
     in
     let maxdisj = maxDisjoints sort (bsetFilter boxes hasAppropriateAglist) 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  /\ <d> b /\ nCands
@@ -359,8 +369,18 @@ let mkRule_CL sort bs defer sl : stateExpander =
               a_i       /\     b /\ c_j
         *)
         let children = bsetMakeRealEmpty () in
-        List.iter (bsetAdd children) (b::c_j) ;
-        List.iter (bsetAdd children) (a_i) ;
+        let defer1 = bsetMakeRealEmpty () in
+        bsetAdd children b;
+        if deferral_tracking diamDb b
+        then bsetAdd defer1 b;
+        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
@@ -374,7 +394,13 @@ let mkRule_CL sort bs defer sl : stateExpander =
            a_i
     *)
     let a_i : bset = bsetMakeRealEmpty () in
-    bsetIter (fun f -> bsetAdd a_i (lfGetDest1 sort f)) coalitions ;
+    let defer1 : bset = bsetMakeRealEmpty () in
+    bsetIter (fun f ->
+              let nextf = lfGetDest1 sort f in
+              bsetAdd a_i nextf;
+              if deferral_tracking f nextf
+              then bsetAdd defer1 nextf)
+             coalitions ;
     ((fun bs1 -> bs), lazylistFromList [(s1, a_i, defer1)])::acc
   in
   let rules = List.fold_left getRule1 rules disjoints in