From eda515b6c2f78ac8d36ecf5f60211232bb6db300 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Mon, 21 Jul 2014 11:05:31 +0200
Subject: [PATCH] Add ocaml part of PML rule application
---
src/lib/CoAlgFormula.ml | 9 +++++--
src/lib/CoAlgLogics.ml | 42 ++++++++++++++++++++++++++++++++-
src/lib/CoAlgMisc.ml | 16 ++++++++-----
src/lib/CoAlgMisc.mli | 1 +
src/lib/gmlmip.ml | 1 +
src/lib/gmlmip.mli | 7 +++++-
src/testsuite/cool-testsuite.ml | 9 +++++++
7 files changed, 75 insertions(+), 10 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 15a6951..2f083d0 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 3d51a51..d656a51 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 ac569c9..b5ffc7c 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 54acbe6..dbc602e 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 72b47f3..fa801bd 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 4a911ac..0a4c553 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 868fed5..b1cfb47 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 =
--
GitLab