From 8cac089767d7eda28de7088a47f20587ab53cdd2 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Thu, 5 Nov 2015 15:20:04 +0100
Subject: [PATCH] CTL is expected to be removed early on
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Create pattern-matching cases for all CTL language elements and raise an
error if encountered. We are assuming that CTL is replaced by plain
μ-Calculus early on
---
src/lib/CoAlgFormula.ml | 42 +++++++++++++++++++++++++++++++++++++++--
1 file changed, 40 insertions(+), 2 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index bd52c9d..14e2806 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -118,6 +118,10 @@ let rec sizeFormula f =
| MU (_, f1)
| NU (_, f1) -> succ (succ (sizeFormula f1))
| VAR _ -> 1
+ | AF _ | EF _
+ | AG _ | EG _
+ | AU _ | EU _ ->
+ raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
(** Determines the size of a sorted formula.
@param f A sorted formula.
@@ -509,7 +513,16 @@ let rec exportTatlFormula_buffer sb f =
| ID _
| NORM _
| NORMN _
- | FUS _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
+ | FUS _
+ | MU _
+ | NU _
+ | VAR _
+ | AF _
+ | EF _
+ | AG _
+ | EG _
+ | AU _
+ | EU _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
let exportTatlFormula f =
let sb = Buffer.create 128 in
@@ -983,6 +996,12 @@ let rec nnfNeg f =
| NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
| CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
| FUS (first, f1) -> FUS (first, nnfNeg f1)
+ | AF _
+ | EF _
+ | AG _
+ | EG _
+ | AU _
+ | EU _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
(** Converts a formula to negation normal form
by "pushing in" the negations "~".
@@ -1064,6 +1083,12 @@ and nnf f =
let ft = nnf f1 in
if ft == f1 then f else FUS (first, ft)
+ | AF _
+ | EF _
+ | AG _
+ | EG _
+ | AU _
+ | EU _ -> 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.
@@ -1235,6 +1260,13 @@ let rec simplify f =
| _ -> if ft == f1 then f else FUS (first, ft)
end
+ | AF _
+ | EF _
+ | AG _
+ | EG _
+ | AU _
+ | EU _ ->
+ raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(** Destructs an atomic proposition.
@param f An atomic proposition.
@@ -1914,7 +1946,13 @@ let rec hc_formula hcF f =
| FUS (first, f1) ->
let tf1 = hc_formula hcF f1 in
HcFormula.hashcons hcF (HCFUS (first, tf1))
-
+ | AF _
+ | EF _
+ | AG _
+ | EG _
+ | AU _
+ | EU _ ->
+ raise (CoAlgException ("nnf: CTL should have been removed at this point"))
(** An instantiation of a hash table (of the standard library)
for hash-consed formulae. The test for equality
--
GitLab