diff --git a/CoAlgLogics.ml b/CoAlgLogics.ml
index 0fb82d0fe7c06d959e1ab38ef98b6011fd98c6a3..be35511152fccf82e5fa94c5ffb8838cca9ca924 100644
--- a/CoAlgLogics.ml
+++ b/CoAlgLogics.ml
@@ -265,6 +265,9 @@ let mkRule_CL sort bs sl =
res := None;
AllInOne rules
+let mkRule_GML sort bs sl =
+ mkRule_MultiModalK sort bs sl
+
let mkRule_Choice sort bs sl =
assert (List.length sl = 2);
let dep bsl =
@@ -343,5 +346,6 @@ let getExpandingFunctionProducer = function
| MultiModalK -> mkRule_MultiModalK
| MultiModalKD -> mkRule_MultiModalKD
| CoalitionLogic -> mkRule_CL
+ | GML -> mkRule_GML
| Choice -> mkRule_Choice
| Fusion -> mkRule_Fusion
diff --git a/CoAlgMisc.ml b/CoAlgMisc.ml
index d8a6720cc5a38d9ee574bac256e45e8a1af2b9ec..beb4fbd45e6f84eac4f0efe0c15a0c5f0dbfe68a 100644
--- a/CoAlgMisc.ml
+++ b/CoAlgMisc.ml
@@ -69,6 +69,7 @@ type functors =
| MultiModalK
| MultiModalKD
| CoalitionLogic
+ | GML
| Choice
| Fusion
@@ -82,8 +83,10 @@ type formulaType =
| NomF
| ExF (* Existential / diamond *)
| AxF (* Universal / box *)
- | EnforcesF
- | AllowsF
+ | EnforcesF (* diamond of CL *)
+ | AllowsF (* box of CL *)
+ | MinF (* at least n successors *)
+ | MaxF (* at most n successors *)
| ChcF (* Choice *)
| FusF (* Fusion *)
@@ -480,6 +483,7 @@ let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))
let arrayDest1 = ref (Array.make 0 (Array.make 0 (-1))) (* first subformula *)
let arrayDest2 = ref (Array.make 0 (Array.make 0 (-1))) (* second subformula *)
let arrayDest3 = ref (Array.make 0 (Array.make 0 (-1))) (* a role *)
+let arrayDestNum = ref (Array.make 0 (Array.make 0 (-1))) (* an integer *)
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
(** This lookup table maps formulae (represented as integers)
@@ -491,6 +495,7 @@ let lfGetType sort f = !arrayType.(sort).(f)
let lfGetDest1 sort f = !arrayDest1.(sort).(f)
let lfGetDest2 sort f = !arrayDest2.(sort).(f)
let lfGetDest3 sort f = !arrayDest3.(sort).(f)
+let lfGetDestNum sort f = !arrayDestNum.(sort).(f)
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
let lfGetNeg sort f =
let nf = !arrayNeg.(sort).(f) in
@@ -561,8 +566,12 @@ 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 _
- | C.HCMAX _ -> raise (C.CoAlgException "Min/Max functor currently not supported.")
+ | C.HCMIN (_,_,f1)
+ | C.HCMAX (_,_,f1) ->
+ if func <> GML || List.length sortlst <> 1
+ then raise (C.CoAlgException "[{>=,<=}]-formula is used in wrong sort.")
+ else ();
+ detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
| C.HCCHC (f1, f2)
| C.HCCHCN (f1, f2) ->
if func <> Choice || List.length sortlst <> 2 then
@@ -647,8 +656,26 @@ 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 _
- | C.HCMAX _ -> assert false
+ | C.HCMIN (cnt,role,f1) ->
+ !arrayType.(s).(n) <- MinF;
+ !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
+ !arrayDestNum.(s).(n) <- cnt;
+ !arrayDest3.(s).(n) <-
+ if Hashtbl.mem htR role then Hashtbl.find htR role
+ else
+ let size = Hashtbl.length htR in
+ Hashtbl.add htR role size;
+ size
+ | C.HCMAX (cnt,role,f1) ->
+ !arrayType.(s).(n) <- MaxF;
+ !arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
+ !arrayDestNum.(s).(n) <- cnt;
+ !arrayDest3.(s).(n) <-
+ if Hashtbl.mem htR role then Hashtbl.find htR role
+ else
+ let size = Hashtbl.length htR in
+ Hashtbl.add htR role size;
+ size
| C.HCCHC (f1, f2)
| C.HCCHCN (f1, f2) ->
!arrayType.(s).(n) <- ChcF;
@@ -734,6 +761,7 @@ let ppFormulae nomTbl tbox (s, f) =
arrayDest2 := Array.init card (fun _ -> Array.make !size (-1));
arrayDest3 := Array.init card (fun _ -> Array.make !size (-1));
arrayNeg := Array.init card (fun _ -> Array.make !size (-1));
+ arrayDestNum := Array.init card (fun _ -> Array.make !size (-1));
arrayDestAg := Array.init card (fun _ -> Array.make !size (Array.make 0 (-1)));
let htR = Hashtbl.create 128 in
Array.iteri (fun s ht -> C.HcFHt.iter (initTables nomTbl hcF htF htR s) ht) htF;
diff --git a/CoAlgMisc.mli b/CoAlgMisc.mli
index a8ecb13f5b9846d29120663db8df2aabade852db..1c50e0c949e8d05f9629a7f2163cc10493f13baf 100644
--- a/CoAlgMisc.mli
+++ b/CoAlgMisc.mli
@@ -13,6 +13,7 @@ type functors =
| MultiModalK
| MultiModalKD
| CoalitionLogic
+ | GML
| Choice
| Fusion
@@ -28,6 +29,8 @@ type formulaType =
| AxF
| EnforcesF
| AllowsF
+ | MinF
+ | MaxF
| ChcF
| FusF
@@ -275,6 +278,7 @@ val lfGetType : sort -> localFormula -> formulaType
val lfGetDest1 : sort -> localFormula -> localFormula
val lfGetDest2 : sort -> localFormula -> localFormula
val lfGetDest3 : sort -> localFormula -> int
+val lfGetDestNum : sort -> localFormula -> int
val lfGetDestAg : sort -> localFormula -> int array
val lfGetNeg : sort -> localFormula -> localFormula option
val lfGetAt : nominal -> localFormula -> atFormula
diff --git a/coalg.ml b/coalg.ml
index c5200e3a4a90994b94fbfada55a0651f5b4aeb10..16e3e305c9e18f951ade2bcec2835c190595e100 100644
--- a/coalg.ml
+++ b/coalg.ml
@@ -37,7 +37,7 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm
let printUsage () =
print_endline "Usage: \"alc <task> <functor> [<verbose>]\" where";
print_endline " <task> in { sat print }";
- print_endline " <functor> in { MultiModalK MultiModalKD CoalitionLogic";
+ print_endline " <functor> in { MultiModalK MultiModalKD CoalitionLogic GML";
print_endline " (or: K) (or: KD) (or: CL) }";
print_endline " <verbose> = any (second) argument";
print_endline "";
@@ -54,6 +54,7 @@ let parseFunctor str =
| "K" -> CM.MultiModalK
| "KD" -> CM.MultiModalKD
| "CL" -> CM.CoalitionLogic
+ | "GML" -> CM.GML
| "MultiModalK" -> CM.MultiModalK
| "MultiModalKD" -> CM.MultiModalKD
| "CoalitionLogic" -> CM.CoalitionLogic