diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 15a69513ddf1e61a3d239849eae0b4017fa13bfc..2f083d090123993978359c44815cda9960181c72 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -564,8 +564,13 @@ and parse_rest ts =
end
| _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ")
in
- if (denominator > n) then begin
- A.printError mk_exn ~ts "Nominator must not be larger than the denominator: "
+ if (denominator < n) then begin
+ let explanation =
+ ("nominator="^(string_of_int n)^" but denominator="^(string_of_int denominator))
+ in
+ A.printError mk_exn ~ts ("Nominator must not be larger than the denominator "
+ ^"("^explanation^") at: "
+ )
end;
let _ =
match Stream.next ts with
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 3d51a51f491911d27588efda4b675081702d4bc1..d656a51d02e689e452fbb4a085e52503bc346282 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -273,7 +273,7 @@ let mkRule_GML sort bs sl : stateExpander =
(bsetFold (modality false) boxes [])
in
let conclusion = gml_rules premise in
- (* conclusion is a set of rules, each of the forman \/ /\ lit *)
+ (* conclusion is a set of rules, *each* of the form \/ /\ lit *)
let handleRuleConcl rc acc =
let handleConjunction conj =
let res = bsetMake () in
@@ -295,6 +295,45 @@ let mkRule_GML sort bs sl : stateExpander =
let rules = S.foldBS addRule roles [] in
lazylistFromList rules
+let mkRule_PML sort bs sl : stateExpander =
+ assert (List.length sl = 1);
+ let s1 = List.hd sl in (* [s1] = List.hd sl *)
+ let diamonds = bsetFilter bs (fun f -> lfGetType sort f = AtLeastProbF) in
+ let boxes = bsetFilter bs (fun f -> lfGetType sort f = AtMostProbF) in
+ let premise: (bool*int*int*int) list =
+ let modality isDiamond m acc =
+ let nominator = lfGetDestNum sort m in
+ let denominator = lfGetDestNum2 sort m in
+ (isDiamond,nominator,denominator,lfToInt (lfGetDest1 sort m))::acc
+ in
+ List.append
+ (bsetFold (modality true) diamonds [])
+ (bsetFold (modality false) boxes [])
+ in
+ let conclusion = pml_rules premise in
+ let error message = raise (CoAlgFormula.CoAlgException message) in
+ (* conclusion is a set of rules, *each* of the form \/ /\ lit *)
+ let handleRuleConcl rc acc =
+ let handleConjunction conj =
+ let res = bsetMake () in
+ let handleLiteral = (fun (f,positive) ->
+ let f = lfFromInt f in
+ let f = if positive
+ then f
+ else match lfGetNeg sort f with
+ | Some nf -> nf
+ | None -> error ("Negation of formula missing")
+ in bsetAdd res f)
+ in
+ List.iter handleLiteral conj;
+ (s1,res)
+ in
+ let rc = List.map handleConjunction rc in
+ ((fun bs1 -> bs),lazylistFromList rc)::acc
+ in
+ let rules = List.fold_right handleRuleConcl conclusion [] in
+ lazylistFromList rules
+
let mkRule_Choice sort bs sl : stateExpander =
assert (List.length sl = 2);
let dep bsl =
@@ -362,5 +401,6 @@ let getExpandingFunctionProducer = function
| MultiModalKD -> mkRule_MultiModalKD
| CoalitionLogic -> mkRule_CL
| GML -> mkRule_GML
+ | PML -> mkRule_PML
| Choice -> mkRule_Choice
| Fusion -> mkRule_Fusion
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index ac569c982dff40f3590669b421a8a382affad27e..b5ffc7c1c586a7e2385b74ccb4ecff3a3812f503 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -78,6 +78,7 @@ let unaryfunctor2name : (functors*string) list =
[ (MultiModalK , "MultiModalK")
; (MultiModalKD , "MultiModalKD")
; (GML , "GML")
+ ; (PML , "PML")
; (CoalitionLogic , "CoalitionLogic")
; (MultiModalK , "K")
; (MultiModalKD , "KD")
@@ -575,13 +576,14 @@ let arrayNeg = ref (Array.make 0 (Array.make 0 (-1)))
*)
(*
for PML: arrayDest1 = the subformula
- arrayDest2 = the nominator of the probability
- arrayDest3 = the denominator of the probability
+ arrayNum = the nominator of the probability
+ arrayNum2 = the denominator of the probability
*)
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 arrayDestNum2 = ref (Array.make 0 (Array.make 0 (-1))) (* another integer *)
let arrayDestAg = ref (Array.make 0 (Array.make 0 [|0|])) (* arrays of agents *)
(** This lookup table maps formulae (represented as integers)
@@ -594,6 +596,7 @@ 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 lfGetDestNum2 sort f = !arrayDestNum2.(sort).(f)
let lfGetDestAg sort f = !arrayDestAg.(sort).(f)
let lfGetNeg sort f =
let nf = !arrayNeg.(sort).(f) in
@@ -783,13 +786,13 @@ let initTables nomTbl hcF htF htR s f n =
| C.HCATLEASTPROB (p,f1) ->
!arrayType.(s).(n) <- AtLeastProbF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
- !arrayDest2.(s).(n) <- p.C.nominator;
- !arrayDest3.(s).(n) <- p.C.denominator
+ !arrayDestNum.(s).(n) <- p.C.nominator;
+ !arrayDestNum2.(s).(n) <- p.C.denominator
| C.HCATMOSTPROB (p,f1) ->
!arrayType.(s).(n) <- AtMostProbF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
- !arrayDest2.(s).(n) <- p.C.nominator;
- !arrayDest3.(s).(n) <- p.C.denominator
+ !arrayDestNum.(s).(n) <- p.C.nominator;
+ !arrayDestNum2.(s).(n) <- p.C.denominator
| C.HCCHC (f1, f2)
| C.HCCHCN (f1, f2) ->
!arrayType.(s).(n) <- ChcF;
@@ -882,6 +885,7 @@ let ppFormulae nomTbl tbox (s, f) =
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));
+ arrayDestNum2 := 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/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 54acbe687fc903521f291f5dcfc35862acbe2b80..dbc602ea8ee3b7429273492b82d1e4b20010043f 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -313,6 +313,7 @@ val lfGetDest1 : sort -> localFormula -> localFormula
val lfGetDest2 : sort -> localFormula -> localFormula
val lfGetDest3 : sort -> localFormula -> int
val lfGetDestNum : sort -> localFormula -> int
+val lfGetDestNum2 : sort -> localFormula -> int
val lfGetDestAg : sort -> localFormula -> int array
val lfGetNeg : sort -> localFormula -> localFormula option
val lfGetAt : nominal -> localFormula -> atFormula
diff --git a/src/lib/gmlmip.ml b/src/lib/gmlmip.ml
index 72b47f3fffb937ffa5ee84d754502627240fb424..fa801bd6f0f227e79f6dc2b21d31f85ccbccb40e 100644
--- a/src/lib/gmlmip.ml
+++ b/src/lib/gmlmip.ml
@@ -5,3 +5,4 @@
here positive? means that the formula must be true in order to make the
given conjunct of modalities true *)
external gml_rules : (bool*int*int) list -> (int*bool) list list list = "gmlRules_stub"
+let pml_rules : (bool*int*int*int) list -> (int*bool) list list list = fun _ -> []
diff --git a/src/lib/gmlmip.mli b/src/lib/gmlmip.mli
index 4a911acccb4a7354376b31bff68e3a7f84598848..0a4c5535ac1ddfd62fd91f0739eba9ec2ba10a5c 100644
--- a/src/lib/gmlmip.mli
+++ b/src/lib/gmlmip.mli
@@ -1,5 +1,10 @@
(* transforms list of gml formulas (diamond?,number,formula)
- to list of consequences (positive?,formula),
+ to list of consequences (formula,positive?),
here positive? means that the formula must be true in order to make the
given conjunct of modalities true *)
val gml_rules : (bool*int*int) list -> (int*bool) list list list
+(* transforms list of pml formulas (diamond?,nominator,denominator,formula)
+ to list of consequences (formula,positive?),
+ here positive? means that the formula must be true in order to make the
+ given conjunct of modalities true *)
+val pml_rules : (bool*int*int*int) list -> (int*bool) list list list
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 868fed5c22388973b678d3f3dfc6c11f3a5ba6cc..b1cfb47b0efafa19cd71e09f37d05c057b88841c 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -98,6 +98,14 @@ let kOrKd_testcases : satCheck list =
; c Unsat "((False) + ([R] False))"
]
+let pml_testcases : testcase_section =
+ use_functor "PML"
+ [ sat "{>= 1/3} C & {<= 1/2} D"
+ ; sat "{>= 1/3} C & {<= 1/2} C"
+ ; unsat "{<= 1/3} C & {>= 1/2} C"
+ ; sat "{<= 1/3} C & {<= 1/2} C"
+ ]
+
let testcases =
let c name table = (name,table) in
[ c "DL98 (Sat)" DL98.satCasesList
@@ -108,6 +116,7 @@ let testcases =
; cl_testcases
; kAndKd_testcases
; c "K+KD" kOrKd_testcases
+ ; pml_testcases
]
let main =