diff --git a/CoAlgFormula.ml b/CoAlgFormula.ml
index cecfb1fe5c19444465ea5d023757f2af0fe03b3c..890e3d92f4bf310d9b0e93613049ed6c3b25f313 100644
--- a/CoAlgFormula.ml
+++ b/CoAlgFormula.ml
@@ -38,6 +38,8 @@ type formula =
| ALLOWS of int list * formula
| MIN of int * string * formula
| MAX of int * string * formula
+ | MORETHAN of int * string * formula (* diamond of GML *)
+ | MAXEXCEPT of int * string * formula (* box of GML *)
| CHC of formula * formula
| CHCN of formula * formula
| FUS of bool * formula
@@ -74,7 +76,9 @@ let rec sizeFormula f =
| ENFORCES (_, f1)
| ALLOWS (_, f1) -> succ (sizeFormula f1)
| MIN (_, _, f1)
- | MAX (_, _, f1) -> succ (sizeFormula f1)
+ | MAX (_, _, f1)
+ | MORETHAN (_, _, f1)
+ | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1)
| CHC (f1, f2)
| CHCN (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
| FUS (_, f1) -> succ (sizeFormula f1)
@@ -174,6 +178,20 @@ let rec exportFormula_buffer sb f =
Buffer.add_string sb s;
Buffer.add_string sb "}";
prio 4 f1
+ | MORETHAN (n, s, f1) ->
+ Buffer.add_string sb "{>";
+ Buffer.add_string sb (string_of_int n);
+ Buffer.add_string sb " ";
+ Buffer.add_string sb s;
+ Buffer.add_string sb "}";
+ prio 4 f1
+ | MAXEXCEPT (n, s, f1) ->
+ Buffer.add_string sb "{<=";
+ Buffer.add_string sb (string_of_int n);
+ Buffer.add_string sb " ~ ";
+ Buffer.add_string sb s;
+ Buffer.add_string sb "}";
+ prio 4 f1 (* actually is prio of ~ and not of <= *)
| CHC (f1, f2) ->
Buffer.add_string sb "(";
exportFormula_buffer sb f1;
@@ -528,8 +546,10 @@ let rec nnfNeg f =
| AX (s, f1) -> EX (s, nnfNeg f1)
| ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1)
| ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1)
- | MIN (n, s, f1) -> if n = 0 then FALSE else MAX (n-1, s, nnf f1)
- | MAX (n, s, f1) -> MIN (n+1, s, nnf f1)
+ | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1)
+ | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1)
+ | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1)
+ | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
| CHC (f1, f2) -> CHCN (nnfNeg f1, nnfNeg f2)
| CHCN (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
| FUS (first, f1) -> FUS (first, nnfNeg f1)
@@ -577,10 +597,16 @@ and nnf f =
if n = 0 then TRUE
else
let ft = nnf f1 in
- if ft == f1 then f else MIN (n, s, ft)
+ MORETHAN (n-1,s,f1)
| MAX (n, s, f1) ->
+ let ft = nnfNeg f1 in
+ MAXEXCEPT (n,s, ft)
+ | MORETHAN (n,s,f1) ->
let ft = nnf f1 in
- if ft == f1 then f else MAX (n, s, ft)
+ if ft = f1 then f else MORETHAN (n,s,ft)
+ | MAXEXCEPT (n,s,f1) ->
+ let ft = nnf f1 in
+ if ft = f1 then f else MAXEXCEPT (n,s,ft)
| CHC (f1, f2) ->
let ft1 = nnf f1 in
let ft2 = nnf f2 in
@@ -694,6 +720,12 @@ let rec simplify f =
| FALSE -> FALSE
| _ -> if ft == f1 then f else MIN (n, s, ft)
end
+ | MORETHAN (n,s,f1) ->
+ let ft = simplify f1 in
+ if ft == f1 then f else MORETHAN (n,s,ft)
+ | MAXEXCEPT (n,s,f1) ->
+ let ft = simplify f1 in
+ if ft == f1 then f else MAXEXCEPT (n,s,ft)
| MAX (n, s, f1) ->
let ft = simplify f1 in
begin
@@ -1157,8 +1189,8 @@ and hcFormula_node =
| HCAX of string * hcFormula
| HCENFORCES of int list * hcFormula
| HCALLOWS of int list * hcFormula
- | HCMIN of int * string * hcFormula
- | HCMAX of int * string * hcFormula
+ | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
+ | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
| HCCHC of hcFormula * hcFormula
| HCCHCN of hcFormula * hcFormula
| HCFUS of bool * hcFormula
@@ -1181,8 +1213,8 @@ let equal_hcFormula_node f1 f2 =
| HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2
| HCENFORCES (s1, f1), HCALLOWS (s2, f2)
| HCENFORCES (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
- | HCMIN (n1, s1, f1), HCMIN (n2, s2, f2)
- | HCMAX (n1, s1, f1), HCMAX (n2, s2, f2) ->
+ | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
+ | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
n1 = n2 && compare s1 s2 = 0 && f1 == f2
| HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
| HCCHCN (f1a, f1b), HCCHCN (f2a, f2b) -> f1a == f2a && f1b == f2b
@@ -1201,8 +1233,8 @@ let equal_hcFormula_node f1 f2 =
| HCAX _, _
| HCENFORCES _, _
| HCALLOWS _, _
- | HCMIN _, _
- | HCMAX _, _
+ | HCMORETHAN _, _
+ | HCMAXEXCEPT _, _
| HCCHC _, _
| HCCHCN _, _
| HCFUS _, _ -> false
@@ -1222,8 +1254,8 @@ let hash_hcFormula_node f =
| HCAND (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 6
| HCEX (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 3
| HCAX (s, f1) -> 19 * (19 * (Hashtbl.hash s) + f1.HC.hkey) + 4
- | HCMIN (n, s, f1) -> 19 * (19 * (19 * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
- | HCMAX (n, s, f1) -> 19 * (19 * (19 * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
+ | HCMORETHAN (n, s, f1) -> 19 * (19 * (19 * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
+ | HCMAXEXCEPT (n, s, f1) -> 19 * (19 * (19 * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
| HCCHC (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 9
| HCCHCN (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 10
| HCFUS (first, f1) -> 19 * (19 * (Hashtbl.hash first) + f1.HC.hkey) + 11
@@ -1247,8 +1279,8 @@ let toFml_hcFormula_node f =
| HCAX (s, f1) -> AX (s, f1.HC.fml)
| HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
| HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
- | HCMIN (n, s, f1) -> MIN (n, s, f1.HC.fml)
- | HCMAX (n, s, f1) -> MAX (n, s, f1.HC.fml)
+ | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
+ | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
| HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
| HCCHCN (f1, f2) -> CHCN (f1.HC.fml, f2.HC.fml)
| HCFUS (first, f1) -> FUS (first, f1.HC.fml)
@@ -1270,10 +1302,8 @@ let negNde_hcFormula_node f =
| HCAX (s, f2) -> HCEX (s, f2.HC.neg)
| HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
| HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
- | HCMIN (n, s, f1) ->
- assert (n > 0);
- HCMAX (n-1, s, f1)
- | HCMAX (n, s, f1) -> HCMIN (n+1, s, f1)
+ | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
+ | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
| HCCHC (f1, f2) -> HCCHCN (f1.HC.neg, f2.HC.neg)
| HCCHCN (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
| HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
@@ -1316,6 +1346,8 @@ let rec hc_formula hcF f =
HcFormula.hashcons hcF (HCAND (tf1, tf2))
| NOT _
| EQU _
+ | MIN _
+ | MAX _
| IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
| EX (s, f1) ->
let tf1 = hc_formula hcF f1 in
@@ -1329,12 +1361,12 @@ let rec hc_formula hcF f =
| ALLOWS (s, f1) ->
let tf1 = hc_formula hcF f1 in
HcFormula.hashcons hcF (HCALLOWS (s, tf1))
- | MIN (n, s, f1) ->
+ | MORETHAN (n, s, f1) ->
let tf1 = hc_formula hcF f1 in
- HcFormula.hashcons hcF (HCMIN (n, s, tf1))
- | MAX (n, s, f1) ->
+ HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1))
+ | MAXEXCEPT (n, s, f1) ->
let tf1 = hc_formula hcF f1 in
- HcFormula.hashcons hcF (HCMAX (n, s, tf1))
+ HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1))
| CHC (f1, f2) ->
let tf1 = hc_formula hcF f1 in
let tf2 = hc_formula hcF f2 in
diff --git a/CoAlgFormula.mli b/CoAlgFormula.mli
index bc4a9c40c0001438b09a48fd3871529262334417..69a7ecffa2f89f92c88f1b47f6337f036f0dfb27 100644
--- a/CoAlgFormula.mli
+++ b/CoAlgFormula.mli
@@ -24,6 +24,8 @@ type formula =
| ALLOWS of int list * formula
| MIN of int * string * formula
| MAX of int * string * formula
+ | MORETHAN of int * string * formula (* diamond of GML *)
+ | MAXEXCEPT of int * string * formula (* box of GML *)
| CHC of formula * formula
| CHCN of formula * formula
| FUS of bool * formula
@@ -109,8 +111,8 @@ and hcFormula_node =
| HCAX of string * hcFormula
| HCENFORCES of int list * hcFormula
| HCALLOWS of int list * hcFormula
- | HCMIN of int * string * hcFormula
- | HCMAX of int * string * hcFormula
+ | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
+ | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
| HCCHC of hcFormula * hcFormula
| HCCHCN of hcFormula * hcFormula
| HCFUS of bool * hcFormula
diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index be35511152fccf82e5fa94c5ffb8838cca9ca924..3a088a5c5bfcc862dd4a96da6e55451f648444ff 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -266,7 +266,11 @@ let mkRule_CL sort bs sl =
AllInOne rules
let mkRule_GML sort bs sl =
- mkRule_MultiModalK sort bs sl
+ assert (List.length sl = 1);
+ let s1 = List.hd sl in (* [s1] = List.hd sl *)
+ let boxes = bsetFilter bs (fun f -> lfGetType sort f = MoreThanF) in
+ let diamonds = bsetFilter bs (fun f -> lfGetType sort f = MaxExceptF) in
+ mkRule_MultiModalK sort bs sl
let mkRule_Choice sort bs sl =
assert (List.length sl = 2);
diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index beb4fbd45e6f84eac4f0efe0c15a0c5f0dbfe68a..30f92b0f40748ddbccb532c02948cf2924b786e1 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -85,8 +85,8 @@ type formulaType =
| AxF (* Universal / box *)
| EnforcesF (* diamond of CL *)
| AllowsF (* box of CL *)
- | MinF (* at least n successors *)
- | MaxF (* at most n successors *)
+ | MoreThanF (* more than n successors = diamond in gml *)
+ | MaxExceptF(* at most n exceptions = box in gml *)
| ChcF (* Choice *)
| FusF (* Fusion *)
@@ -566,8 +566,8 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
then raise (C.CoAlgException "[{Agents}]-formula is used in wrong sort.")
else ();
detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
- | C.HCMIN (_,_,f1)
- | C.HCMAX (_,_,f1) ->
+ | C.HCMORETHAN (_,_,f1)
+ | C.HCMAXEXCEPT (_,_,f1) ->
if func <> GML || List.length sortlst <> 1
then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
else ();
@@ -656,8 +656,8 @@ let initTables nomTbl hcF htF htR s f n =
!arrayType.(s).(n) <- AllowsF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
!arrayDestAg.(s).(n) <- Array.of_list aglist
- | C.HCMIN (cnt,role,f1) ->
- !arrayType.(s).(n) <- MinF;
+ | C.HCMORETHAN (cnt,role,f1) ->
+ !arrayType.(s).(n) <- MoreThanF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
!arrayDestNum.(s).(n) <- cnt;
!arrayDest3.(s).(n) <-
@@ -666,8 +666,8 @@ let initTables nomTbl hcF htF htR s f n =
let size = Hashtbl.length htR in
Hashtbl.add htR role size;
size
- | C.HCMAX (cnt,role,f1) ->
- !arrayType.(s).(n) <- MaxF;
+ | C.HCMAXEXCEPT (cnt,role,f1) ->
+ !arrayType.(s).(n) <- MaxExceptF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
!arrayDestNum.(s).(n) <- cnt;
!arrayDest3.(s).(n) <-
diff --git a/CoAlgMisc.mli b/CoAlgMisc.mli
index 1c50e0c949e8d05f9629a7f2163cc10493f13baf..2c80349a9d14ac63b7e789051b54ef18c8703c93 100644
--- a/CoAlgMisc.mli
+++ b/CoAlgMisc.mli
@@ -29,8 +29,8 @@ type formulaType =
| AxF
| EnforcesF
| AllowsF
- | MinF
- | MaxF
+ | MoreThanF
+ | MaxExceptF
| ChcF
| FusF