From c855ba913465be19e71062de24cb4cd5e50f90f4 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:32:14 +0200
Subject: [PATCH] Change AtMostProbable to LessProbableThan
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
The actual box of PML (in GMLMIP) is: less probable than. The Diamond
is: At least Probable than.
So now you have ¬[p] C = <p> C.
---
src/lib/CoAlgFormula.ml | 54 ++++++++++++++++++---------------
src/lib/CoAlgFormula.mli | 7 +++--
src/lib/CoAlgLogics.ml | 2 +-
src/lib/CoAlgMisc.ml | 10 +++---
src/lib/CoAlgMisc.mli | 2 +-
src/testsuite/cool-testsuite.ml | 8 ++---
6 files changed, 45 insertions(+), 38 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 2f083d0..8210bd6 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -49,7 +49,7 @@ type formula =
| MAXEXCEPT of int * string * formula (* box of GML *)
| ATLEASTPROB of rational * formula (* = {>= 0.5} C ---> C occurs with *)
(* probability of at least 50% *)
- | ATMOSTPROB of rational * formula
+ | LESSPROB of rational * formula
| CHC of formula * formula
| CHCN of formula * formula
| FUS of bool * formula
@@ -91,7 +91,7 @@ let rec sizeFormula f =
| MIN (_, _, f1)
| MAX (_, _, f1)
| ATLEASTPROB (_, f1)
- | ATMOSTPROB (_, f1)
+ | LESSPROB (_, f1)
| MORETHAN (_, _, f1)
| MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1)
| CHC (f1, f2)
@@ -116,7 +116,7 @@ let rec iter func formula =
| EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
| ENFORCES (_,a) | ALLOWS (_,a)
| MIN (_,_,a) | MAX (_,_,a)
- | ATLEASTPROB (_, a) | ATMOSTPROB (_, a)
+ | ATLEASTPROB (_, a) | LESSPROB (_, a)
| MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
| CHC (a,b) | CHCN (a,b) -> (proc a ; proc b)
| FUS (_,a) -> proc a
@@ -142,7 +142,7 @@ let rec convert_post func formula = (* run over all subformulas in post order *)
| MIN (n,s,a) -> MIN (n,s,c a)
| MAX (n,s,a) -> MAX (n,s,c a)
| ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a)
- | ATMOSTPROB (p,a) -> ATMOSTPROB (p, c a)
+ | LESSPROB (p,a) -> LESSPROB (p, c a)
| MORETHAN (n,s,a) -> MORETHAN (n,s,c a)
| MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a)
| CHC (a,b) -> CHC (c a, c b)
@@ -268,8 +268,8 @@ let rec exportFormula_buffer sb f =
Buffer.add_string sb (string_of_rational p);
Buffer.add_string sb "}";
prio 4 f1
- | ATMOSTPROB (p, f1) ->
- Buffer.add_string sb "{<=";
+ | LESSPROB (p, f1) ->
+ Buffer.add_string sb "{<";
Buffer.add_string sb (string_of_rational p);
Buffer.add_string sb "}";
prio 4 f1
@@ -396,7 +396,7 @@ let rec exportTatlFormula_buffer sb f =
| CHC _
| CHCN _
| ATLEASTPROB _
- | ATMOSTPROB _
+ | LESSPROB _
| FUS _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
let exportTatlFormula f =
@@ -468,7 +468,7 @@ let exportQueryParsable tbox (_,f) =
let lexer = A.make_lexer
[":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
- ;"[{";"}]";"<{";"}>";",";"/"
+ ;"[{";"}]";"<{";"}>";",";"/";"{<"
]
let mk_exn s = CoAlgException s
@@ -629,8 +629,14 @@ and parse_rest ts =
let (n, denom, s) = boxinternals false "}" in
let f1 = parse_rest ts in
if (denom <> 0)
- then ATMOSTPROB (rational_of_int n denom, f1)
+ then A.printError mk_exn ~ts "Can not express {<= probability}"
else MAX (n, s, f1)
+ | A.Kwd "{<" ->
+ let (n, denom, s) = boxinternals false "}" in
+ let f1 = parse_rest ts in
+ if (denom <> 0)
+ then LESSPROB (rational_of_int n denom, f1)
+ else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet"
| A.Kwd "(" -> begin
let f = parse_formula ts in
match Stream.next ts with
@@ -776,8 +782,8 @@ let rec nnfNeg f =
| 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)
- | ATLEASTPROB (p, f1) -> ATMOSTPROB (p, nnf f1)
- | ATMOSTPROB (p, f1) -> ATLEASTPROB (p, nnf f1)
+ | ATLEASTPROB (p, f1) -> LESSPROB (p, nnf f1)
+ | LESSPROB (p, f1) -> ATLEASTPROB (p, nnf f1)
| CHC (f1, f2) -> CHCN (nnfNeg f1, nnfNeg f2)
| CHCN (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
| FUS (first, f1) -> FUS (first, nnfNeg f1)
@@ -838,9 +844,9 @@ and nnf f =
| ATLEASTPROB (p, f1) ->
let ft = nnf f1 in
if ft == f1 then f else ATLEASTPROB (p, ft)
- | ATMOSTPROB (p, f1) ->
+ | LESSPROB (p, f1) ->
let ft = nnf f1 in
- if ft == f1 then f else ATMOSTPROB (p, ft)
+ if ft == f1 then f else LESSPROB (p, ft)
| CHC (f1, f2) ->
let ft1 = nnf f1 in
let ft2 = nnf f2 in
@@ -967,9 +973,9 @@ let rec simplify f =
| FALSE -> TRUE
| _ -> if ft == f1 then f else MAX (n, s, ft)
end
- | ATMOSTPROB (p,f1) ->
+ | LESSPROB (p,f1) ->
let ft1 = simplify f1 in
- if (ft1 == f1) then f else ATMOSTPROB (p,ft1)
+ if (ft1 == f1) then f else LESSPROB (p,ft1)
| ATLEASTPROB (p,f1) ->
let ft1 = simplify f1 in
if (ft1 == f1) then f else ATLEASTPROB (p,ft1)
@@ -1438,7 +1444,7 @@ and hcFormula_node =
| HCMORETHAN of int * string * hcFormula (* GML Diamond *)
| HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
| HCATLEASTPROB of rational * hcFormula
- | HCATMOSTPROB of rational * hcFormula
+ | HCLESSPROB of rational * hcFormula
| HCCHC of hcFormula * hcFormula
| HCCHCN of hcFormula * hcFormula
| HCFUS of bool * hcFormula
@@ -1466,7 +1472,7 @@ let equal_hcFormula_node f1 f2 =
n1 = n2 && compare s1 s2 = 0 && f1 == f2
| HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
p1 = p2 && f1 == f2
- | HCATMOSTPROB (p1, f1), HCATMOSTPROB (p2,f2) ->
+ | HCLESSPROB (p1, f1), HCLESSPROB (p2,f2) ->
p1 = p2 && f1 == f2
| HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
| HCCHCN (f1a, f1b), HCCHCN (f2a, f2b) -> f1a == f2a && f1b == f2b
@@ -1488,7 +1494,7 @@ let equal_hcFormula_node f1 f2 =
| HCMORETHAN _, _
| HCMAXEXCEPT _, _
| HCATLEASTPROB _, _
- | HCATMOSTPROB _, _
+ | HCLESSPROB _, _
| HCCHC _, _
| HCCHCN _, _
| HCFUS _, _ -> false
@@ -1511,7 +1517,7 @@ let hash_hcFormula_node f =
| 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
| HCATLEASTPROB (p,f1) -> 19 * (19 * (19 * p.nominator + p.denominator) + f1.HC.hkey) + 9
- | HCATMOSTPROB (p,f1) -> 19 * (19 * (19 * p.nominator + p.denominator) + f1.HC.hkey) + 10
+ | HCLESSPROB (p,f1) -> 19 * (19 * (19 * p.nominator + p.denominator) + f1.HC.hkey) + 10
| HCCHC (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 11
| HCCHCN (f1, f2) -> 19 * (19 * f1.HC.hkey + f2.HC.hkey) + 12
| HCFUS (first, f1) -> 19 * (19 * (Hashtbl.hash first) + f1.HC.hkey) + 13
@@ -1538,7 +1544,7 @@ let toFml_hcFormula_node f =
| HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
| HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
| HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
- | HCATMOSTPROB (p, f1) -> ATMOSTPROB (p, f1.HC.fml)
+ | HCLESSPROB (p, f1) -> LESSPROB (p, 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)
@@ -1562,8 +1568,8 @@ let negNde_hcFormula_node f =
| HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
| HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
| HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
- | HCATLEASTPROB (p, f1) -> HCATMOSTPROB (p, f1)
- | HCATMOSTPROB (p, f1) -> HCATLEASTPROB (p, f1)
+ | HCATLEASTPROB (p, f1) -> HCLESSPROB (p, f1)
+ | HCLESSPROB (p, f1) -> HCATLEASTPROB (p, f1)
| 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)
@@ -1629,8 +1635,8 @@ let rec hc_formula hcF f =
HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1))
| ATLEASTPROB (p, f1) ->
HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1))
- | ATMOSTPROB (p, f1) ->
- HcFormula.hashcons hcF (HCATMOSTPROB (p, hc_formula hcF f1))
+ | LESSPROB (p, f1) ->
+ HcFormula.hashcons hcF (HCLESSPROB (p, hc_formula hcF f1))
| CHC (f1, f2) ->
let tf1 = hc_formula hcF f1 in
let tf2 = hc_formula hcF f2 in
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 8fc08a9..ea8c662 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -30,9 +30,10 @@ type formula =
| MAX of int * string * formula (* some more intuitive box for GML *)
| MORETHAN of int * string * formula (* diamond of GML *)
| MAXEXCEPT of int * string * formula (* box of GML, means: ¬>_nR.¬C *)
- | ATLEASTPROB of rational * formula (* = {>= 0.5} C ---> C occurs with *)
+ | ATLEASTPROB of rational * formula (* = {>= 1/2} C ---> C occurs with *)
(* probability of at least 50% *)
- | ATMOSTPROB of rational * formula
+ | LESSPROB of rational * formula (* = [1/2] C = {< 1/2} C ---> C occours with *)
+ (* probability of less than 50% *)
| CHC of formula * formula
| CHCN of formula * formula
| FUS of bool * formula
@@ -133,7 +134,7 @@ and hcFormula_node =
| HCMORETHAN of int * string * hcFormula (* GML Diamond *)
| HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
| HCATLEASTPROB of rational * hcFormula
- | HCATMOSTPROB of rational * hcFormula
+ | HCLESSPROB of rational * hcFormula
| HCCHC of hcFormula * hcFormula
| HCCHCN of hcFormula * hcFormula
| HCFUS of bool * hcFormula
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index d656a51..6fa92ae 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -299,7 +299,7 @@ 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 boxes = bsetFilter bs (fun f -> lfGetType sort f = LessProbF) in
let premise: (bool*int*int*int) list =
let modality isDiamond m acc =
let nominator = lfGetDestNum sort m in
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index b5ffc7c..bbc3689 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -124,7 +124,7 @@ type formulaType =
| MoreThanF (* more than n successors = diamond in gml *)
| MaxExceptF(* at most n exceptions = box in gml *)
| AtLeastProbF (* for PML *)
- | AtMostProbF (* for PML *)
+ | LessProbF (* for PML *)
| ChcF (* Choice *)
| FusF (* Fusion *)
@@ -674,9 +674,9 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
else ();
detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
| C.HCATLEASTPROB (_,f1)
- | C.HCATMOSTPROB (_,f1) ->
+ | C.HCLESSPROB (_,f1) ->
if func <> PML || List.length sortlst <> 1
- then raise (C.CoAlgException "[{>=,<=}]-formula with probability is used in wrong sort.")
+ then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
else ();
detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
| C.HCCHC (f1, f2)
@@ -788,8 +788,8 @@ let initTables nomTbl hcF htF htR s f n =
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
!arrayDestNum.(s).(n) <- p.C.nominator;
!arrayDestNum2.(s).(n) <- p.C.denominator
- | C.HCATMOSTPROB (p,f1) ->
- !arrayType.(s).(n) <- AtMostProbF;
+ | C.HCLESSPROB (p,f1) ->
+ !arrayType.(s).(n) <- LessProbF;
!arrayDest1.(s).(n) <- C.HcFHt.find htF.(List.hd sortlst) f1;
!arrayDestNum.(s).(n) <- p.C.nominator;
!arrayDestNum2.(s).(n) <- p.C.denominator
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index dbc602e..f42a548 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -37,7 +37,7 @@ type formulaType =
| MoreThanF
| MaxExceptF
| AtLeastProbF (* for PML *)
- | AtMostProbF (* for PML *)
+ | LessProbF (* for PML *)
| ChcF
| FusF
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index b1cfb47..682b081 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -100,10 +100,10 @@ let kOrKd_testcases : satCheck list =
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"
+ [ 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 =
--
GitLab