diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml index 0dd1215441474a55875ac4a2c6ddbd900ab1159c..2245965b130230b944ba7bfd2cf54d5eb0a96166 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.