From 562081433c6bc61ba3122f898e3ba8e1928c1669 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Fri, 17 Jan 2014 13:57:48 +0100
Subject: [PATCH] Implement rule for CL

---
 CoAlgLogicUtils.ml  |  1 +
 CoAlgLogicUtils.mli |  1 +
 CoAlgLogics.ml      | 49 +++++++++++++++++++++++++++++++++++++++++++--
 3 files changed, 49 insertions(+), 2 deletions(-)

diff --git a/CoAlgLogicUtils.ml b/CoAlgLogicUtils.ml
index bea0a51..a7995bb 100644
--- a/CoAlgLogicUtils.ml
+++ b/CoAlgLogicUtils.ml
@@ -14,6 +14,7 @@ module TArray = struct
     let all f = any (fun x -> not (f x))
     let elem (x: 'a) (arr: 'a array) =
         any (fun y -> x == y) arr
+    let included sub sup = all (fun x -> elem x sup) sub
 end
 
 let disjointAgents sort a b =
diff --git a/CoAlgLogicUtils.mli b/CoAlgLogicUtils.mli
index 24982ae..08a4207 100644
--- a/CoAlgLogicUtils.mli
+++ b/CoAlgLogicUtils.mli
@@ -10,6 +10,7 @@ module TArray : sig
     val all : ('a -> bool) -> 'a array -> bool
     val any : ('a -> bool) -> 'a array -> bool
     val elem : 'a -> 'a array -> bool
+    val included : 'a array -> 'a array -> bool
 end
 
 val disjointAgents : sort -> localFormula -> localFormula -> bool
diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index 1c12404..e9629ea 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -210,6 +210,45 @@ let mkRule_CL sort bs sl =
   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 []
+  in
+  let getRule2 diamDb acc = (* diamDb = <D> b *)
+    let d = lfGetDestAg sort diamDb in (* the agent list *)
+    let b = lfGetDest1 sort diamDb in
+    let hasAppropriateAglist f =
+        let aglist = lfGetDestAg sort f in
+        TArray.included aglist d
+    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 []
+        in
+        (* now do rule 2:
+            coalitions  /\ <d> b /\ nCands
+           ————————————————————————————————
+              a_i       /\     b /\ c_j
+        *)
+        let children = bsetMake () in
+        List.iter (bsetAdd children) (b::c_j) ;
+        List.iter (bsetAdd children) (a_i) ;
+        ((fun bs1 -> bs), [(s1, children)])::acc
+    in
+    List.fold_left createSingleRule acc maxdisj
+  in
+  let rules = bsetFold getRule2 dCands [] in
+  let getRule1 acc coalitions =
+    (* do rule 1:
+        coalitions
+       ————————————
+           a_i
+    *)
+    let a_i : bset = bsetMake () in
+    bsetIter (fun f -> bsetAdd a_i (lfGetDest1 sort f)) coalitions ;
+    ((fun bs1 -> bs), [(s1, a_i)])::acc
+  in
+  let rules = List.fold_left getRule1 rules disjoints in
   (*
     mkRule_CL sort bs [s1]
     = { (λ[bs1]. bs, [(s1, { a_i | i∈I })])
@@ -217,8 +256,14 @@ let mkRule_CL sort bs sl =
           C_i pairwise disjoint and I maximal
         }
   *)
-  (* just do this to let it compile... *)
-  mkRule_MultiModalK sort bs sl
+  (* standard return procedure *)
+  let res = ref (Some rules) in
+  fun () ->
+    match !res with
+    | None -> NoMoreRules
+    | Some rules ->
+        res := None;
+        AllInOne rules
 
 let mkRule_Choice sort bs sl =
   assert (List.length sl = 2);
-- 
GitLab