From 0aa3467526ca026be02ab39a22f9ccca1a41708c Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Fri, 30 Oct 2015 18:24:45 +0100
Subject: [PATCH] Read/Write CTL
---
src/lib/CoAlgFormula.ml | 57 +++++++++++++++++++++++++++++++++++++++++
1 file changed, 57 insertions(+)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 5b44359..fc59e57 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -372,6 +372,28 @@ let rec exportFormula_buffer sb f =
prio 4 f1
| VAR s ->
Buffer.add_string sb s
+ | AF f1 ->
+ Buffer.add_string sb "AF ";
+ prio 4 f1
+ | EF f1 ->
+ Buffer.add_string sb "EF ";
+ prio 4 f1
+ | AG f1 ->
+ Buffer.add_string sb "AG ";
+ prio 4 f1
+ | EG f1 ->
+ Buffer.add_string sb "EG ";
+ prio 4 f1
+ | AU (f1, f2) ->
+ Buffer.add_string sb "A ";
+ prio 4 f1;
+ Buffer.add_string sb " U ";
+ prio 4 f2
+ | EU (f1, f2) ->
+ Buffer.add_string sb "E ";
+ prio 4 f1;
+ Buffer.add_string sb " U ";
+ prio 4 f2
(** Converts a formula into a string representation.
Parentheses are ommited where possible
@@ -533,6 +555,7 @@ let lexer = A.make_lexer
[":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
;"μ";"ν";"."
+ ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U"
]
let mk_exn s = CoAlgException s
@@ -759,6 +782,40 @@ and parse_rest ts =
let (_, _, s) = boxinternals true "." in
let f1 = parse_rest ts in
NU (VAR s, f1)
+ | A.Kwd "AF" ->
+ let f = parse_rest ts in
+ AF f
+ | A.Kwd "EF" ->
+ let f = parse_rest ts in
+ EF f
+ | A.Kwd "AG" ->
+ let f = parse_rest ts in
+ AG f
+ | A.Kwd "EG" ->
+ let f = parse_rest ts in
+ EG f
+ | A.Kwd "A" ->
+ let f1 = parse_rest ts in
+ let _ = match Stream.next ts with
+ | A.Kwd "U" -> "U"
+ | t -> A.printError mk_exn ~t ~ts "String \"U\" from CTL expected: "
+ in
+ let f2 = parse_rest ts in
+ AU (f1, f2)
+ | A.Kwd "E" ->
+ let f1 = parse_rest ts in
+ let _ = match Stream.next ts with
+ | A.Kwd "U" -> "U"
+ | t -> A.printError mk_exn ~t ~ts "String \"U\" from CTL expected: "
+ in
+ let f2 = parse_rest ts in
+ EU (f1, f2)
+ | A.Kwd "AX" ->
+ let f1 = parse_rest ts in
+ AX ("", f1)
+ | A.Kwd "EX" ->
+ let f1 = parse_rest ts in
+ EX ("", f1)
| t -> A.printError mk_exn ~t ~ts
"\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\",
\"True\", \"False\", \"=\", \"=o\", \"O\" or <ident> expected: "
--
GitLab