diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml index 0cd32cdb2b8e9458c6d5f191dc25b5f35fffbca9..7ab43461108d5a1391771c41d36d66f18180189d 100644 --- a/src/lib/CoAlgFormula.ml +++ b/src/lib/CoAlgFormula.ml @@ -231,20 +231,19 @@ let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i)) let convertToMu formula = let helper formula = - let symbol = Stream.next gensym in match formula with | AF f1 -> - MU (symbol, (OR (f1, (AX ("", (VAR symbol)))))) + MU ("#AF#", (OR (f1, (AX ("", (VAR "#AF#")))))) | EF f1 -> - MU (symbol, (OR (f1, (EX ("", (VAR symbol)))))) + MU ("#EF#", (OR (f1, (EX ("", (VAR "#EF#")))))) | AG f1 -> - NU (symbol, (AND (f1, (AX ("", (VAR symbol)))))) + NU ("#AG#", (AND (f1, (AX ("", (VAR "#AG#")))))) | EG f1 -> - NU (symbol, (AND (f1, (EX ("", (VAR symbol)))))) + NU ("#EG#", (AND (f1, (EX ("", (VAR "#EG#")))))) | AU (f1, f2) -> - MU (symbol, (OR (f2, (AND (f1, (AX ("", (VAR symbol)))))))) + MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#")))))))) | EU (f1, f2) -> - MU (symbol, (OR (f2, (AND (f1, (EX ("", (VAR symbol)))))))) + MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#")))))))) | _ -> formula in convert_post helper formula