From e30caa428cb13e6b8000ba8cb03ee3c67df569b6 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 11 Apr 2016 00:12:29 +0200
Subject: [PATCH] Implement {A,E}( .. {R,B} ..) CTL formulas
---
src/lib/CoAlgFormula.ml | 168 ++++++++++++++++++++++++++-------------
src/lib/CoAlgFormula.mli | 2 +
2 files changed, 114 insertions(+), 56 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 7ab4346..3d561d0 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -67,6 +67,8 @@ type formula =
| EG of formula
| AU of formula * formula
| EU of formula * formula
+ | AR of formula * formula
+ | ER of formula * formula
exception ConversionException of formula
@@ -120,7 +122,8 @@ let rec sizeFormula f =
| VAR _ -> 1
| AF _ | EF _
| AG _ | EG _
- | AU _ | EU _ ->
+ | AU _ | EU _
+ | AR _ | ER _ ->
raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
(** Determines the size of a sorted formula.
@@ -153,47 +156,50 @@ let rec iter func formula =
| FUS (_,a) -> proc a
| MU (_, f) | NU (_, f) -> proc f
| AF f | EF f | AG f | EG f -> proc f
- | AU (f1, f2) | EU (f1, f2) -> (proc f1; proc f2)
+ | AU (f1, f2) | EU (f1, f2) | AR (f1, f2) | ER (f1, f2) -> (proc f1; proc f2)
let rec convert_post func formula = (* run over all subformulas in post order *)
let c = convert_post func in (* some shorthand *)
(* replace parts of the formula *)
let formula = (match formula with
- (* 0-ary constructors *)
- | TRUE | FALSE | AP _ | VAR _ -> formula
- | CONST _
- | CONSTN _ -> formula
- (* unary *)
- | NOT a -> NOT (c a)
- | AT (s,a) -> AT (s,c a)
- (* binary *)
- | OR (a,b) -> OR (c a, c b)
- | AND (a,b) -> AND (c a, c b)
- | EQU (a,b) -> EQU (c a, c b)
- | IMP (a,b) -> IMP (c a, c b)
- | EX (s,a) -> EX (s,c a)
- | AX (s,a) -> AX (s,c a)
- | ENFORCES (s,a) -> ENFORCES (s,c a)
- | ALLOWS (s,a) -> ALLOWS (s,c a)
- | 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)
- | 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)
- | ID(a) -> ID (c a)
- | NORM(a, b) -> NORM(c a, c b)
- | NORMN(a, b) -> NORMN(c a, c b)
- | CHC (a,b) -> CHC (c a, c b)
- | FUS (s,a) -> FUS (s, c a)
- | MU (n, f1) -> MU (n, c f1)
- | NU (n, f1) -> NU (n, c f1)
- | AF f1 -> AF (c f1)
- | EF f1 -> EF (c f1)
- | AG f1 -> AG (c f1)
- | EG f1 -> EG (c f1)
- | AU (f1, f2) -> AU (c f1, c f2)
- | EU (f1, f2) -> AU (c f1, c f2))in
+ (* 0-ary constructors *)
+ | TRUE | FALSE | AP _ | VAR _ -> formula
+ | CONST _
+ | CONSTN _ -> formula
+ (* unary *)
+ | NOT a -> NOT (c a)
+ | AT (s,a) -> AT (s,c a)
+ (* binary *)
+ | OR (a,b) -> OR (c a, c b)
+ | AND (a,b) -> AND (c a, c b)
+ | EQU (a,b) -> EQU (c a, c b)
+ | IMP (a,b) -> IMP (c a, c b)
+ | EX (s,a) -> EX (s,c a)
+ | AX (s,a) -> AX (s,c a)
+ | ENFORCES (s,a) -> ENFORCES (s,c a)
+ | ALLOWS (s,a) -> ALLOWS (s,c a)
+ | 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)
+ | 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)
+ | ID(a) -> ID (c a)
+ | NORM(a, b) -> NORM(c a, c b)
+ | NORMN(a, b) -> NORMN(c a, c b)
+ | CHC (a,b) -> CHC (c a, c b)
+ | FUS (s,a) -> FUS (s, c a)
+ | MU (n, f1) -> MU (n, c f1)
+ | NU (n, f1) -> NU (n, c f1)
+ | AF f1 -> AF (c f1)
+ | EF f1 -> EF (c f1)
+ | AG f1 -> AG (c f1)
+ | EG f1 -> EG (c f1)
+ | AU (f1, f2) -> AU (c f1, c f2)
+ | EU (f1, f2) -> EU (c f1, c f2)
+ | AR (f1, f2) -> AR (c f1, c f2)
+ | ER (f1, f2) -> ER (c f1, c f2))
+ in
func formula
let convertToK formula = (* tries to convert a formula to a pure K formula *)
@@ -244,6 +250,11 @@ let convertToMu formula =
MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#"))))))))
| EU (f1, f2) ->
MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#"))))))))
+ | AR (f1, f2) ->
+ NU ("#AR#", (AND (f2, (OR (f1, (AX ("", (VAR "#AR#"))))))))
+ | ER (f1, f2) ->
+ NU ("#ER#", (AND (f2, (OR (f1, (EX ("", (VAR "#ER#"))))))))
+
| _ -> formula
in
convert_post helper formula
@@ -432,6 +443,19 @@ let rec exportFormula_buffer sb f =
Buffer.add_string sb " U ";
prio 4 f2;
Buffer.add_string sb ")"
+ | AR (f1, f2) ->
+ Buffer.add_string sb "A (";
+ prio 4 f1;
+ Buffer.add_string sb " R ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
+ | ER (f1, f2) ->
+ Buffer.add_string sb "E (";
+ prio 4 f1;
+ Buffer.add_string sb " R ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
+
(** Converts a formula into a string representation.
Parentheses are ommited where possible
@@ -526,7 +550,9 @@ let rec exportTatlFormula_buffer sb f =
| AG _
| EG _
| AU _
- | EU _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
+ | EU _
+ | AR _
+ | ER _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
let exportTatlFormula f =
let sb = Buffer.create 128 in
@@ -602,7 +628,7 @@ let lexer = A.make_lexer
[":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
;"μ";"ν";"."
- ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U"
+ ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U";"R";"B"
]
let mk_exn s = CoAlgException s
@@ -668,7 +694,7 @@ let rec verifyMuAltFree formula =
else
("ν", newfree)
| VAR s -> ("none", [s])
- | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ ->
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ ->
raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
@@ -707,7 +733,7 @@ let rec verifyMuMonotone negations formula =
let increment (s, n) = (s, n+1) in
let newNeg = List.map increment negations in
verifyMuMonotone newNeg a
- | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ ->
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ ->
raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
let rec verifyMuGuarded unguarded formula =
@@ -736,7 +762,7 @@ let rec verifyMuGuarded unguarded formula =
let finder x = compare x s == 0 in
if List.exists finder unguarded then
raise (CoAlgException ("formula not guarded"))
- | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ ->
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ ->
raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
let verifyFormula formula =
@@ -990,18 +1016,40 @@ and parse_rest symtab ts =
EG f
| A.Kwd "A" ->
assert (Stream.next ts = A.Kwd "(");
- let f1 = parse_formula symtab ts in
- assert (Stream.next ts = A.Kwd "U");
- let f2 = parse_formula symtab ts in
- assert (Stream.next ts = A.Kwd ")");
- AU (f1, f2)
+ let f1 = parse_formula symtab ts in begin
+ match Stream.next ts with
+ | A.Kwd "U" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ AU (f1, f2)
+ | A.Kwd "R" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ AR (f1, f2)
+ | A.Kwd "B" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ AR (f2, f1)
+ | t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
+ end
| A.Kwd "E" ->
assert (Stream.next ts = A.Kwd "(");
- let f1 = parse_formula symtab ts in
- assert (Stream.next ts = A.Kwd "U");
- let f2 = parse_formula symtab ts in
- assert (Stream.next ts = A.Kwd ")");
- EU (f1, f2)
+ let f1 = parse_formula symtab ts in begin
+ match Stream.next ts with
+ | A.Kwd "U" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ EU (f1, f2)
+ | A.Kwd "R" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ ER (f1, f2)
+ | A.Kwd "B" ->
+ let f2 = parse_formula symtab ts in
+ assert (Stream.next ts = A.Kwd ")");
+ ER (f2, f1)
+ | t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
+ end
| A.Kwd "AX" ->
let f1 = parse_rest symtab ts in
AX ("", f1)
@@ -1153,7 +1201,9 @@ let rec nnfNeg f =
| AG _
| EG _
| AU _
- | EU _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
+ | EU _
+ | AR _
+ | ER _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
(** Converts a formula to negation normal form
by "pushing in" the negations "~".
@@ -1246,7 +1296,9 @@ and nnf f =
| AG _
| EG _
| AU _
- | EU _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point"))
+ | EU _
+ | AR _
+ | ER _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(** Simplifies a formula.
@param f A formula which must be in negation normal form.
@@ -1438,7 +1490,9 @@ let rec simplify f =
| AG _
| EG _
| AU _
- | EU _ ->
+ | EU _
+ | AR _
+ | ER _ ->
raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(** Destructs an atomic proposition.
@@ -2146,7 +2200,9 @@ let rec hc_formula hcF f =
| AG _
| EG _
| AU _
- | EU _ ->
+ | EU _
+ | AR _
+ | ER _ ->
raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(* Replace the Variable name in f with formula formula
diff --git a/src/lib/CoAlgFormula.mli b/src/lib/CoAlgFormula.mli
index 68525e4..ff89471 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -50,6 +50,8 @@ type formula =
| EG of formula
| AU of formula * formula
| EU of formula * formula
+ | AR of formula * formula
+ | ER of formula * formula
exception ConversionException of formula
--
GitLab