diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml index 5e20c9746910cb93abf3ddbecd89a7615f8acc8f..0dd1215441474a55875ac4a2c6ddbd900ab1159c 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 "<=>") ->