From 5e185dd3008b1b7ccf6de315a1f74fc8fe8912ab Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Thu, 16 Jan 2014 17:49:50 +0100
Subject: [PATCH] More own helper functions
---
CoAlgLogicUtils.ml | 18 ++++++++++++------
CoAlgLogicUtils.mli | 7 ++++++-
CoAlgLogics.ml | 17 +++++++++++------
CoAlgLogics.mli | 1 +
4 files changed, 30 insertions(+), 13 deletions(-)
diff --git a/CoAlgLogicUtils.ml b/CoAlgLogicUtils.ml
index c264178..bea0a51 100644
--- a/CoAlgLogicUtils.ml
+++ b/CoAlgLogicUtils.ml
@@ -4,11 +4,17 @@ open Graph
open CoAlgMisc
-let elemArray (x: 'a) (arr: 'a array) =
- let res = ref (false) in
- let f y = if (x == y) then res := true else () in
- Array.iter f arr;
- !res
+module TArray = struct
+ let any f arr =
+ let rec g idx =
+ if idx >= Array.length arr then false
+ else if f arr.(idx) then true
+ else g (idx + 1)
+ in g 0
+ let all f = any (fun x -> not (f x))
+ let elem (x: 'a) (arr: 'a array) =
+ any (fun y -> x == y) arr
+end
let disjointAgents sort a b =
assert (lfGetType sort a = EnforcesF || lfGetType sort a = AllowsF);
@@ -17,7 +23,7 @@ let disjointAgents sort a b =
let lb = lfGetDestAg sort b in
let res = ref (true) in
let f idx =
- if (elemArray idx lb) then res := false
+ if (TArray.elem idx lb) then res := false
else ()
in
Array.iter f la;
diff --git a/CoAlgLogicUtils.mli b/CoAlgLogicUtils.mli
index 747b5ef..24982ae 100644
--- a/CoAlgLogicUtils.mli
+++ b/CoAlgLogicUtils.mli
@@ -6,10 +6,15 @@
open CoAlgMisc
+module TArray : sig
+ val all : ('a -> bool) -> 'a array -> bool
+ val any : ('a -> bool) -> 'a array -> bool
+ val elem : 'a -> 'a array -> bool
+end
+
val disjointAgents : sort -> localFormula -> localFormula -> bool
val maxDisjoints : sort -> bset -> bset list
-
diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index fffff30..1c12404 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -193,6 +193,7 @@ let compatible sort (a: bset) formula1 =
/\ n /\ m all C_i ⊆ D
/ \i=1 a_i /\ b / \j=1 c_j
*)
+let agents = [|1;2;3;4;5;6;7;8;9;10|]
let mkRule_CL sort bs sl =
assert (List.length sl = 1); (* TODO: Why? *)
@@ -200,14 +201,18 @@ let mkRule_CL sort bs sl =
let boxes = bsetFilter bs (fun f -> lfGetType sort f = EnforcesF) in
let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AllowsF) in
let disjoints = maxDisjoints sort boxes in
+ let nCands = bsetMake () in (* all N-diamonds *)
+ let hasFullAgentList formula =
+ let aglist = lfGetDestAg sort formula in
+ let value = TArray.all (fun x -> TArray.elem x aglist) agents in
+ if (value) then bsetAdd nCands formula else () ;
+ value
+ in
+ (* Candidates for D in Rule 2 *)
+ let dCands = bsetFilter diamonds (fun f -> not (hasFullAgentList f)) in
(*
mkRule_CL sort bs [s1]
- = { (λ[bs1]. { ∀R.D
- | <D> b ∈ bs
- }
- ∪ { (λ[bs1].{ [C_i]a_i ∈ bs | a_i ∈ bs1}
- , [(s1, { a_i | i∈I })]
- )
+ = { (λ[bs1]. bs, [(s1, { a_i | i∈I })])
| {[C_i]a_i | i∈I} ⊆ bs,
C_i pairwise disjoint and I maximal
}
diff --git a/CoAlgLogics.mli b/CoAlgLogics.mli
index 48d0958..7416575 100644
--- a/CoAlgLogics.mli
+++ b/CoAlgLogics.mli
@@ -6,4 +6,5 @@
open CoAlgMisc
+val agents : int array
val getExpandingFunctionProducer : functors -> sort -> bset -> sort list -> stateExpander
--
GitLab