From 2a36974b70ab857b9354bf7e8b6c4d3a054e9119 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Sat, 14 May 2016 13:38:19 +0200
Subject: [PATCH] Revert to fresh variable names in convertToMu
---
src/lib/CoAlgFormula.ml | 21 +++++++++++----------
1 file changed, 11 insertions(+), 10 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 3eff886..8d50b9a 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
--
GitLab