diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml index 3eff8863d9829a3320a4dd4c5a31a20b46079908..8d50b9a357a3517302baf67122cf8a10eacb16a6 100644 --- a/src/lib/CoAlgFormula.ml +++ b/src/lib/CoAlgFormula.ml @@ -243,28 +243,29 @@ let convertToGML formula = (* tries to convert a formula to a pure GML formula * let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i)) let convertToMu formula = + let name = Stream.next gensym in let helper formula = match formula with | AF f1 -> - MU ("#CTL#", (OR (f1, (AX ("", (VAR "#CTL#")))))) + MU (name, (OR (f1, (AX ("", (VAR name)))))) | EF f1 -> - MU ("#CTL#", (OR (f1, (EX ("", (VAR "#CTL#")))))) + MU (name, (OR (f1, (EX ("", (VAR name)))))) | AG f1 -> - NU ("#CTL#", (AND (f1, (AX ("", (VAR "#CTL#")))))) + NU (name, (AND (f1, (AX ("", (VAR name)))))) | EG f1 -> - NU ("#CTL#", (AND (f1, (EX ("", (VAR "#CTL#")))))) + NU (name, (AND (f1, (EX ("", (VAR name)))))) | AU (f1, f2) -> - MU ("#CTL#", (OR (f2, (AND (f1, (AX ("", (VAR "#CTL#")))))))) + MU (name, (OR (f2, (AND (f1, (AX ("", (VAR name)))))))) | EU (f1, f2) -> - MU ("#CTL#", (OR (f2, (AND (f1, (EX ("", (VAR "#CTL#")))))))) + MU (name, (OR (f2, (AND (f1, (EX ("", (VAR name)))))))) | AR (f1, f2) -> - NU ("#CTL#", (AND (f2, (OR (f1, (AX ("", (VAR "#CTL#")))))))) + NU (name, (AND (f2, (OR (f1, (AX ("", (VAR name)))))))) | ER (f1, f2) -> - NU ("#CTL#", (AND (f2, (OR (f1, (EX ("", (VAR "#CTL#")))))))) + NU (name, (AND (f2, (OR (f1, (EX ("", (VAR name)))))))) | AB (f1, f2) -> - NOT (MU ("#CTL#", (OR (f2, (AND ((NOT f1), (EX ("", (VAR "#CTL#"))))))))) + NOT (MU (name, (OR (f2, (AND ((NOT f1), (EX ("", (VAR name))))))))) | EB (f1, f2) -> - NOT (MU ("#CTL#", (OR (f2, (AND ((NOT f1), (AX ("", (VAR "#CTL#"))))))))) + NOT (MU (name, (OR (f2, (AND ((NOT f1), (AX ("", (VAR name))))))))) | _ -> formula in convert_post helper formula