From 9bae2c4f239c82151d97092238c111606ae14d41 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Mon, 21 Jul 2014 13:49:48 +0200
Subject: [PATCH] Implement the REAL box of PML
---
src/lib/CoAlgFormula.ml | 47 ++++++++++++++++++------------------
src/lib/CoAlgFormula.mli | 6 ++---
src/lib/CoAlgLogics.ml | 19 ++++++++++-----
src/lib/CoAlgMisc.ml | 14 +++++++----
src/lib/CoAlgMisc.mli | 4 +--
src/lib/GMLMIP-0.1/onestep.c | 2 +-
6 files changed, 52 insertions(+), 40 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 8210bd6..aba2496 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -49,7 +49,8 @@ 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% *)
- | LESSPROB of rational * formula
+ | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
+ (* probability of less than 50% *)
| CHC of formula * formula
| CHCN of formula * formula
| FUS of bool * formula
@@ -91,7 +92,7 @@ let rec sizeFormula f =
| MIN (_, _, f1)
| MAX (_, _, f1)
| ATLEASTPROB (_, f1)
- | LESSPROB (_, f1)
+ | LESSPROBFAIL (_, f1)
| MORETHAN (_, _, f1)
| MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1)
| CHC (f1, f2)
@@ -116,7 +117,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) | LESSPROB (_, a)
+ | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
| MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
| CHC (a,b) | CHCN (a,b) -> (proc a ; proc b)
| FUS (_,a) -> proc a
@@ -142,7 +143,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)
- | LESSPROB (p,a) -> LESSPROB (p, c a)
+ | LESSPROBFAIL (p,a) -> LESSPROBFAIL (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,10 +269,10 @@ let rec exportFormula_buffer sb f =
Buffer.add_string sb (string_of_rational p);
Buffer.add_string sb "}";
prio 4 f1
- | LESSPROB (p, f1) ->
+ | LESSPROBFAIL (p, f1) ->
Buffer.add_string sb "{<";
Buffer.add_string sb (string_of_rational p);
- Buffer.add_string sb "}";
+ Buffer.add_string sb "} ~ ";
prio 4 f1
| MIN (n, s, f1) ->
Buffer.add_string sb "{>=";
@@ -396,7 +397,7 @@ let rec exportTatlFormula_buffer sb f =
| CHC _
| CHCN _
| ATLEASTPROB _
- | LESSPROB _
+ | LESSPROBFAIL _
| FUS _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
let exportTatlFormula f =
@@ -635,7 +636,7 @@ and parse_rest ts =
let (n, denom, s) = boxinternals false "}" in
let f1 = parse_rest ts in
if (denom <> 0)
- then LESSPROB (rational_of_int n denom, f1)
+ then LESSPROBFAIL (rational_of_int n denom, NOT f1)
else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet"
| A.Kwd "(" -> begin
let f = parse_formula ts in
@@ -782,8 +783,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) -> LESSPROB (p, nnf f1)
- | LESSPROB (p, f1) -> ATLEASTPROB (p, nnf f1)
+ | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1)
+ | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, 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)
@@ -844,9 +845,9 @@ and nnf f =
| ATLEASTPROB (p, f1) ->
let ft = nnf f1 in
if ft == f1 then f else ATLEASTPROB (p, ft)
- | LESSPROB (p, f1) ->
+ | LESSPROBFAIL (p, f1) ->
let ft = nnf f1 in
- if ft == f1 then f else LESSPROB (p, ft)
+ if ft == f1 then f else LESSPROBFAIL (p, ft)
| CHC (f1, f2) ->
let ft1 = nnf f1 in
let ft2 = nnf f2 in
@@ -973,9 +974,9 @@ let rec simplify f =
| FALSE -> TRUE
| _ -> if ft == f1 then f else MAX (n, s, ft)
end
- | LESSPROB (p,f1) ->
+ | LESSPROBFAIL (p,f1) ->
let ft1 = simplify f1 in
- if (ft1 == f1) then f else LESSPROB (p,ft1)
+ if (ft1 == f1) then f else LESSPROBFAIL (p,ft1)
| ATLEASTPROB (p,f1) ->
let ft1 = simplify f1 in
if (ft1 == f1) then f else ATLEASTPROB (p,ft1)
@@ -1444,7 +1445,7 @@ and hcFormula_node =
| HCMORETHAN of int * string * hcFormula (* GML Diamond *)
| HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
| HCATLEASTPROB of rational * hcFormula
- | HCLESSPROB of rational * hcFormula
+ | HCLESSPROBFAIL of rational * hcFormula
| HCCHC of hcFormula * hcFormula
| HCCHCN of hcFormula * hcFormula
| HCFUS of bool * hcFormula
@@ -1472,7 +1473,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
- | HCLESSPROB (p1, f1), HCLESSPROB (p2,f2) ->
+ | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (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
@@ -1494,7 +1495,7 @@ let equal_hcFormula_node f1 f2 =
| HCMORETHAN _, _
| HCMAXEXCEPT _, _
| HCATLEASTPROB _, _
- | HCLESSPROB _, _
+ | HCLESSPROBFAIL _, _
| HCCHC _, _
| HCCHCN _, _
| HCFUS _, _ -> false
@@ -1517,7 +1518,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
- | HCLESSPROB (p,f1) -> 19 * (19 * (19 * p.nominator + p.denominator) + f1.HC.hkey) + 10
+ | HCLESSPROBFAIL (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
@@ -1544,7 +1545,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)
- | HCLESSPROB (p, f1) -> LESSPROB (p, f1.HC.fml)
+ | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (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)
@@ -1568,8 +1569,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) -> HCLESSPROB (p, f1)
- | HCLESSPROB (p, f1) -> HCATLEASTPROB (p, f1)
+ | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
+ | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, 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)
@@ -1635,8 +1636,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))
- | LESSPROB (p, f1) ->
- HcFormula.hashcons hcF (HCLESSPROB (p, hc_formula hcF f1))
+ | LESSPROBFAIL (p, f1) ->
+ HcFormula.hashcons hcF (HCLESSPROBFAIL (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 ea8c662..7e59944 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -32,8 +32,8 @@ type formula =
| MAXEXCEPT of int * string * formula (* box of GML, means: ¬>_nR.¬C *)
| ATLEASTPROB of rational * formula (* = {>= 1/2} C ---> C occurs with *)
(* probability of at least 50% *)
- | LESSPROB of rational * formula (* = [1/2] C = {< 1/2} C ---> C occours with *)
- (* probability of less than 50% *)
+ | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
+ (* probability of less than 50% *)
| CHC of formula * formula
| CHCN of formula * formula
| FUS of bool * formula
@@ -134,7 +134,7 @@ and hcFormula_node =
| HCMORETHAN of int * string * hcFormula (* GML Diamond *)
| HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
| HCATLEASTPROB of rational * hcFormula
- | HCLESSPROB of rational * hcFormula
+ | HCLESSPROBFAIL of rational * hcFormula (* the probability for failing is less than ... *)
| 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 6fa92ae..20c78b4 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -299,12 +299,14 @@ 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 = LessProbF) in
+ let boxes = bsetFilter bs (fun f -> lfGetType sort f = LessProbFailF) 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
+ let nestedFormula = lfToInt (lfGetDest1 sort m) in
+ (*print_endline ("putting formula "^(string_of_int nestedFormula)); *)
+ (isDiamond,nominator,denominator,nestedFormula)::acc
in
List.append
(bsetFold (modality true) diamonds [])
@@ -316,14 +318,19 @@ let mkRule_PML sort bs sl : stateExpander =
let handleRuleConcl rc acc =
let handleConjunction conj =
let res = bsetMake () in
- let handleLiteral = (fun (f,positive) ->
- let f = lfFromInt f in
+ let handleLiteral = fun (f_int,positive) -> begin
+ let f = lfFromInt f_int in
let f = if positive
then f
- else match lfGetNeg sort f with
+ else begin
+ (*print_endline ("getting "^(string_of_int f_int)); *)
+ match lfGetNeg sort f with
| Some nf -> nf
| None -> error ("Negation of formula missing")
- in bsetAdd res f)
+ end
+ in
+ bsetAdd res f
+ end
in
List.iter handleLiteral conj;
(s1,res)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index bbc3689..f34b5fb 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 *)
- | LessProbF (* for PML *)
+ | LessProbFailF (* box for PML *)
| ChcF (* Choice *)
| FusF (* Fusion *)
@@ -674,11 +674,15 @@ 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.HCLESSPROB (_,f1) ->
+ | C.HCLESSPROBFAIL (_,f1) ->
if func <> PML || List.length sortlst <> 1
then raise (C.CoAlgException "[{>=,<}]-formula with probability is used in wrong sort.")
else ();
- detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1
+ detClosure nomTbl hcF fset atset nomset (List.hd sortlst) f1;
+ (*
+ TODO: add ¬ f1 to the closure!
+ detClosure nomTbl hcF fset atset nomset (List.hd sortlst) (f1.HC.node.negNde)
+ *)
| C.HCCHC (f1, f2)
| C.HCCHCN (f1, f2) ->
if func <> Choice || List.length sortlst <> 2 then
@@ -788,8 +792,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.HCLESSPROB (p,f1) ->
- !arrayType.(s).(n) <- LessProbF;
+ | C.HCLESSPROBFAIL (p,f1) ->
+ !arrayType.(s).(n) <- LessProbFailF;
!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 f42a548..33c5577 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -36,8 +36,8 @@ type formulaType =
| AllowsF
| MoreThanF
| MaxExceptF
- | AtLeastProbF (* for PML *)
- | LessProbF (* for PML *)
+ | AtLeastProbF (* diamond for PML *)
+ | LessProbFailF (* box for PML *)
| ChcF
| FusF
diff --git a/src/lib/GMLMIP-0.1/onestep.c b/src/lib/GMLMIP-0.1/onestep.c
index 4d02a2e..ddc0e8b 100644
--- a/src/lib/GMLMIP-0.1/onestep.c
+++ b/src/lib/GMLMIP-0.1/onestep.c
@@ -87,7 +87,7 @@ static bdd tupleModality2Bdd_PML(IFormula* f, const pair<pair<bool,pair<int,int>
return f->modal(b, t.first.second.first, t.first.second.second);
} else {
/* box */
- bdd* b = new bdd(f->variable(t.second));
+ bdd* b = new bdd(bdd_not(f->variable(t.second)));
return bdd_not(f->modal(b, t.first.second.first, t.first.second.second));
}
}
--
GitLab