From 939f5bab8be721c5c626bbf35d58533cbf1b519b Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 18 Nov 2015 14:37:56 +0100
Subject: [PATCH] add fallthrough cases (CTL constructors) for verify*
---
src/lib/CoAlgFormula.ml | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index a8d229c..36d851e 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -667,6 +667,9 @@ let rec verifyMuAltFree formula =
else
("ν", newfree)
| VAR s -> ("none", [s])
+ | AF _ | EF _ | AG _ | EG _ | AU _ | EU _ ->
+ raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
+
(** Process from outside in. For every variable bound keep the tuple
(name, negations). For every negation crossed map a +1 over snd on
@@ -703,6 +706,8 @@ 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 _ ->
+ raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
let rec verifyMuGuarded unguarded formula =
let proc = verifyMuGuarded unguarded in
@@ -730,6 +735,8 @@ 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 _ ->
+ raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
let verifyFormula formula =
verifyMuAltFree formula;
--
GitLab