Add prototypes for checker functions

We need to enforce some assumptions for μ-Calculus. Add (still empty)
checker function and call them when importing the forumla

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 "<=>") ->