From dcc8167f426d2c6648486f0a078751eb102bccb2 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 22 Feb 2016 15:44:06 +0100
Subject: [PATCH] =?UTF-8?q?Use=20custom=20variables=20for=20CTL=20->=20?=
=?UTF-8?q?=CE=BC?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Makes morally same formulas actually the same. Removes the need to
recalculate some States that have already been fully expanded but with
different variable names only (where this is possible)
---
src/lib/CoAlgFormula.ml | 13 ++++++-------
1 file changed, 6 insertions(+), 7 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 0cd32cd..7ab4346 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
--
GitLab