From d2db7e403b45ba7fc1dc12ffddf126031673e2c3 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 9 Nov 2015 15:04:15 +0100
Subject: [PATCH] Add prototypes for checker functions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
We need to enforce some assumptions for μ-Calculus. Add (still empty)
checker function and call them when importing the forumla
---
src/lib/CoAlgFormula.ml | 9 +++++++++
1 file changed, 9 insertions(+)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 5e20c97..0dd1215 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -247,6 +247,14 @@ let convertToMu formula =
in
convert_post helper formula
+let verifyMuAltFree formula =
+ true
+
+let verifyMuMonotone forumla =
+ true
+
+let verifyMuGuarded 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.
@@ -612,6 +620,7 @@ let mk_exn s = CoAlgException s
*)
let rec parse_formula (symtab: 'a list) ts =
let f1 = convertToMu (parse_imp symtab ts) in
+ assert (verifyMuAltFree f1 && verifyMuMonotone f1 && verifyMuGuarded f1);
match Stream.peek ts with
| None -> f1
| Some (A.Kwd "<=>") ->
--
GitLab