From e2dc68f7642e239a508b79e3c7f8e2865b776f20 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Tue, 28 Jan 2014 16:07:03 +0100
Subject: [PATCH] Enforce agents to be of the list --agents
---
CoAlgFormula.ml | 5 ++++-
CoAlgLogicUtils.ml | 15 +--------------
CoAlgLogicUtils.mli | 9 +--------
CoAlgLogics.ml | 7 ++-----
CoAlgLogics.mli | 3 ---
CoolUtils.ml | 20 ++++++++++++++++++++
CoolUtils.mli | 14 ++++++++++++++
Makefile | 1 +
coalg.ml | 2 +-
9 files changed, 44 insertions(+), 32 deletions(-)
create mode 100644 CoolUtils.ml
create mode 100644 CoolUtils.mli
diff --git a/CoAlgFormula.ml b/CoAlgFormula.ml
index 890e3d9..4097ef9 100644
--- a/CoAlgFormula.ml
+++ b/CoAlgFormula.ml
@@ -361,8 +361,11 @@ and parse_rest ts =
(n, s)
in
let rec agentlist es =
+ let allAgents = CoolUtils.cl_get_agents () in
match Stream.next ts with
- | A.Int n -> n::(agentlist es)
+ | A.Int n -> if CoolUtils.TArray.elem n allAgents
+ then n::(agentlist es)
+ else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ")
| A.Kwd c when c = es -> []
| _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ")
in
diff --git a/CoAlgLogicUtils.ml b/CoAlgLogicUtils.ml
index 32c35cd..8438f63 100644
--- a/CoAlgLogicUtils.ml
+++ b/CoAlgLogicUtils.ml
@@ -3,20 +3,7 @@
open Graph
open CoAlgMisc
-
-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 arr = not (any (fun x -> not (f x)) arr)
- let elem (x: 'a) (arr: 'a array) =
- any (fun y -> x == y) arr
- let included sub sup = all (fun x -> elem x sup) sub
- let to_string ts arr = "[| " ^ (Array.fold_right (fun i str -> (ts i) ^" "^ str) arr "|]")
-end
+open CoolUtils
let disjointAgents sort a b =
assert (lfGetType sort a = EnforcesF || lfGetType sort a = AllowsF);
diff --git a/CoAlgLogicUtils.mli b/CoAlgLogicUtils.mli
index 867064d..5fc525b 100644
--- a/CoAlgLogicUtils.mli
+++ b/CoAlgLogicUtils.mli
@@ -5,14 +5,7 @@
*)
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
- val included : 'a array -> 'a array -> bool
- val to_string : ('a -> string) -> 'a array -> string
-end
+open CoolUtils
val disjointAgents : sort -> localFormula -> localFormula -> bool
diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index b599064..029747a 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -4,6 +4,7 @@
open CoAlgMisc
+open CoolUtils
open CoAlgLogicUtils
(* open Gmlmip *)
@@ -194,10 +195,6 @@ let compatible sort (a: bset) formula1 =
/\ n /\ m all C_i ⊆ D
/ \i=1 a_i /\ b / \j=1 c_j
*)
-let agents = ref ([|1;2;3;4;5;6;7;8;9;10|])
-
-let cl_get_agents () = !agents
-let cl_set_agents arr = ignore (agents := arr)
let mkRule_CL sort bs sl =
assert (List.length sl = 1); (* TODO: Why? *)
@@ -208,7 +205,7 @@ let mkRule_CL sort bs sl =
let nCands = bsetMakeRealEmpty () 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
+ let value = TArray.all (fun x -> TArray.elem x aglist) (cl_get_agents ()) in
if (value) then bsetAdd nCands formula else () ;
value
in
diff --git a/CoAlgLogics.mli b/CoAlgLogics.mli
index 5cc4b28..48d0958 100644
--- a/CoAlgLogics.mli
+++ b/CoAlgLogics.mli
@@ -6,7 +6,4 @@
open CoAlgMisc
-val cl_get_agents : unit -> int array
-val cl_set_agents : int array -> unit
-
val getExpandingFunctionProducer : functors -> sort -> bset -> sort list -> stateExpander
diff --git a/CoolUtils.ml b/CoolUtils.ml
new file mode 100644
index 0000000..bcd5043
--- /dev/null
+++ b/CoolUtils.ml
@@ -0,0 +1,20 @@
+
+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 arr = not (any (fun x -> not (f x)) arr)
+ let elem (x: 'a) (arr: 'a array) =
+ any (fun y -> x == y) arr
+ let included sub sup = all (fun x -> elem x sup) sub
+ let to_string ts arr = "[| " ^ (Array.fold_right (fun i str -> (ts i) ^" "^ str) arr "|]")
+end
+
+let agents = ref ([|1;2;3;4;5;6;7;8;9;10|])
+
+let cl_get_agents () = !agents
+let cl_set_agents arr = ignore (agents := arr)
+
diff --git a/CoolUtils.mli b/CoolUtils.mli
new file mode 100644
index 0000000..bc2dfe9
--- /dev/null
+++ b/CoolUtils.mli
@@ -0,0 +1,14 @@
+
+(* Some basic utilities as they are known from haskell prelude and so on... *)
+
+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
+ val to_string : ('a -> string) -> 'a array -> string
+end
+
+val cl_get_agents : unit -> int array
+val cl_set_agents : int array -> unit
+
diff --git a/Makefile b/Makefile
index e3b3c63..cc064a3 100644
--- a/Makefile
+++ b/Makefile
@@ -101,6 +101,7 @@ gmlmip.cmxa: gmlmip.cmx gmlmip_stub.o $(GMLOBJS)
# Object files... sorted topologically by their dependency...
COALG_OBJS := minisat$(SUFFIXLIB) \
+ CoolUtils$(SUFFIX) \
genAndComp$(SUFFIX) MiscSolver$(SUFFIX) altGenlex$(SUFFIX) HashConsing$(SUFFIX) \
ALCFormula$(SUFFIX) ALCMisc$(SUFFIX) ALCGraph$(SUFFIX) \
CoAlgFormula$(SUFFIX) \
diff --git a/coalg.ml b/coalg.ml
index 93933ed..c36f0e3 100644
--- a/coalg.ml
+++ b/coalg.ml
@@ -117,7 +117,7 @@ let rec parseFlags arr offs : unit =
| "--agents" ->
let strAglist = getParam () in
let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
- CoAlgLogics.cl_set_agents (Array.of_list aglist)
+ CoolUtils.cl_set_agents (Array.of_list aglist)
| _ ->
raise (CoAlgFormula.CoAlgException ("Unknown flag »" ^ (arr.(!offs)) ^ "«"))
) ; parseFlags arr (!offs + 1)
--
GitLab