From 17af27949af34db7145f5ecd885ed1fd413b97ca Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 3 Nov 2015 16:53:09 +0100
Subject: [PATCH] =?UTF-8?q?Add=20gensym=20for=20CTL=20->=20=CE=BC?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
src/lib/CoAlgFormula.ml | 32 ++++++++++++++++++--------------
1 file changed, 18 insertions(+), 14 deletions(-)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 4ee7797..8b68635 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -212,21 +212,25 @@ let convertToGML formula = (* tries to convert a formula to a pure GML formula *
in
convert_post helper formula
+let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
+
let convertToMu formula =
- let helper formula = match formula with
- | AF f1 ->
- MU ((VAR ":genX"), (OR (f1, (AX ("", (VAR ":genX"))))))
- | EF f1 ->
- MU ((VAR ":genX"), (OR (f1, (AX ("", (VAR ":genX"))))))
- | AG f1 ->
- NU ((VAR ":genX"), (AND (f1, (AX ("", (VAR ":genX"))))))
- | EG f1 ->
- NU ((VAR ":genX"), (AND (f1, (AX ("", (VAR ":genX"))))))
- | AU (f1, f2) ->
- MU ((VAR ":genX"), (OR (f2, (AND (f1, (AX ("", (VAR ":genX"))))))))
- | EU (f1, f2) ->
- MU ((VAR ":genX"), (OR (f2, (AND (f1, (EX ("", (VAR ":genX"))))))))
- | _ -> formula
+ let helper formula =
+ let symbol = Stream.next gensym in
+ match formula with
+ | AF f1 ->
+ MU ((VAR symbol), (OR (f1, (AX ("", (VAR symbol))))))
+ | EF f1 ->
+ MU ((VAR symbol), (OR (f1, (AX ("", (VAR symbol))))))
+ | AG f1 ->
+ NU ((VAR symbol), (AND (f1, (AX ("", (VAR symbol))))))
+ | EG f1 ->
+ NU ((VAR symbol), (AND (f1, (AX ("", (VAR symbol))))))
+ | AU (f1, f2) ->
+ MU ((VAR symbol), (OR (f2, (AND (f1, (AX ("", (VAR symbol))))))))
+ | EU (f1, f2) ->
+ MU ((VAR symbol), (OR (f2, (AND (f1, (EX ("", (VAR symbol))))))))
+ | _ -> formula
in
convert_post helper formula
--
GitLab