From a2cd9f2a871d33c2c7412e6f4fb2626948dcaa02 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 9 Nov 2015 20:03:04 +0100
Subject: [PATCH] Add check for guardedness
---
src/lib/CoAlgFormula.ml | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 0dd1215..2245965 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -254,7 +254,19 @@ let verifyMuMonotone forumla =
true
let verifyMuGuarded formula =
+ let helper f =
+ match f with
+ | MU (s, f1)
+ | NU (s, f1) ->
+ (match f1 with
+ | VAR s ->
+ raise (CoAlgException ("formula not guarded"))
+ | _ -> ())
+ | _ -> ()
+ in
+ iter helper formula;
true
+
(** Appends a string representation of a formula to a string buffer.
Parentheses are ommited where possible
where the preference rules are defined as usual.
--
GitLab