diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 3d561d030e07994b02250a7ef12e3adc2184004d..1a6997fbc0e9804cea2b8e8c1812283f28a34eea 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -69,6 +69,8 @@ type formula =
| EU of formula * formula
| AR of formula * formula
| ER of formula * formula
+ | AB of formula * formula
+ | EB of formula * formula
exception ConversionException of formula
@@ -123,7 +125,8 @@ let rec sizeFormula f =
| AF _ | EF _
| AG _ | EG _
| AU _ | EU _
- | AR _ | ER _ ->
+ | AR _ | ER _
+ | AB _ | EB _ ->
raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
(** Determines the size of a sorted formula.
@@ -156,7 +159,9 @@ 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) | AR (f1, f2) | ER (f1, f2) -> (proc f1; proc f2)
+ | AU (f1, f2) | EU (f1, f2)
+ | AR (f1, f2) | ER (f1, f2)
+ | AB (f1, f2) | EB (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 *)
@@ -198,7 +203,9 @@ let rec convert_post func formula = (* run over all subformulas in post order *)
| 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))
+ | ER (f1, f2) -> ER (c f1, c f2)
+ | AB (f1, f2) -> AB (c f1, c f2)
+ | EB (f1, f2) -> EB (c f1, c f2))
in
func formula
@@ -254,7 +261,10 @@ let convertToMu formula =
NU ("#AR#", (AND (f2, (OR (f1, (AX ("", (VAR "#AR#"))))))))
| ER (f1, f2) ->
NU ("#ER#", (AND (f2, (OR (f1, (EX ("", (VAR "#ER#"))))))))
-
+ | AB (f1, f2) ->
+ NOT (MU ("#AB#", (OR (f2, (AND ((NOT f1), (AX ("", (VAR "#AU#")))))))))
+ | EB (f1, f2) ->
+ NOT (MU ("#EB#", (OR (f2, (AND ((NOT f1), (EX ("", (VAR "#EU#")))))))))
| _ -> formula
in
convert_post helper formula
@@ -455,6 +465,18 @@ let rec exportFormula_buffer sb f =
Buffer.add_string sb " R ";
prio 4 f2;
Buffer.add_string sb ")"
+ | AB (f1, f2) ->
+ Buffer.add_string sb "A (";
+ prio 4 f1;
+ Buffer.add_string sb " B ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
+ | EB (f1, f2) ->
+ Buffer.add_string sb "E (";
+ prio 4 f1;
+ Buffer.add_string sb " B ";
+ prio 4 f2;
+ Buffer.add_string sb ")"
(** Converts a formula into a string representation.
@@ -552,7 +574,9 @@ let rec exportTatlFormula_buffer sb f =
| AU _
| EU _
| AR _
- | ER _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
+ | ER _
+ | AB _
+ | EB _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
let exportTatlFormula f =
let sb = Buffer.create 128 in
@@ -694,7 +718,7 @@ let rec verifyMuAltFree formula =
else
("ν", newfree)
| VAR s -> ("none", [s])
- | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ ->
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
@@ -733,7 +757,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 _ | AR _ | ER _ ->
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
let rec verifyMuGuarded unguarded formula =
@@ -762,7 +786,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 _ | AR _ | ER _ ->
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ | AR _ | ER _ | AB _ | EB _ ->
raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
let verifyFormula formula =
@@ -1029,7 +1053,7 @@ and parse_rest symtab ts =
| A.Kwd "B" ->
let f2 = parse_formula symtab ts in
assert (Stream.next ts = A.Kwd ")");
- AR (f2, f1)
+ AB (f1, f2)
| t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
end
| A.Kwd "E" ->
@@ -1047,7 +1071,7 @@ and parse_rest symtab ts =
| A.Kwd "B" ->
let f2 = parse_formula symtab ts in
assert (Stream.next ts = A.Kwd ")");
- ER (f2, f1)
+ EB (f1, f2)
| t -> A.printError mk_exn ~t ~ts "one of \"U\" \"R\" \"B\" expected: "
end
| A.Kwd "AX" ->
@@ -1196,14 +1220,11 @@ let rec nnfNeg f =
| FUS (first, f1) -> FUS (first, nnfNeg f1)
| MU (s, f1) -> NU(s, nnfNeg f1)
| NU (s, f1) -> MU(s, nnfNeg f1)
- | AF _
- | EF _
- | AG _
- | EG _
- | AU _
- | EU _
- | AR _
- | ER _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _
+ | AR _ | ER _
+ | AB _ | EB _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
(** Converts a formula to negation normal form
by "pushing in" the negations "~".
@@ -1291,14 +1312,12 @@ and nnf f =
| NU (s, f1) ->
let ft = nnf f1 in
if ft == f1 then f else NU (s, ft)
- | AF _
- | EF _
- | AG _
- | EG _
- | AU _
- | EU _
- | AR _
- | ER _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point"))
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _
+ | AR _ | ER _
+ | AB _ | EB _ ->
+ 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.
@@ -1485,15 +1504,12 @@ let rec simplify f =
| TRUE -> TRUE
| _ -> if ft == f1 then f else NU (s, ft)
end
- | AF _
- | EF _
- | AG _
- | EG _
- | AU _
- | EU _
- | AR _
- | ER _ ->
- raise (CoAlgException ("nnf: CTL should have been removed at this point"))
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _
+ | AR _ | ER _
+ | AB _ | EB _ ->
+ raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(** Destructs an atomic proposition.
@param f An atomic proposition.
@@ -2195,14 +2211,11 @@ let rec hc_formula hcF f =
| NU (var, f1) ->
let tf1 = hc_formula hcF f1 in
HcFormula.hashcons hcF (HCNU (var, tf1))
- | AF _
- | EF _
- | AG _
- | EG _
- | AU _
- | EU _
- | AR _
- | ER _ ->
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _
+ | AR _ | ER _
+ | AB _ | EB _ ->
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 ff89471442d0d181b9181b27b1039c8e1c4880dc..7ea6b0f8515081bc7f0cddc6218f7433ba4af04e 100644
--- a/src/lib/CoAlgFormula.mli
+++ b/src/lib/CoAlgFormula.mli
@@ -52,6 +52,8 @@ type formula =
| EU of formula * formula
| AR of formula * formula
| ER of formula * formula
+ | AB of formula * formula
+ | EB of formula * formula
exception ConversionException of formula