From c5105465d05ab2fae329fc9d000bb0d11e3fe598 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 2 Nov 2015 23:08:43 +0100
Subject: [PATCH] =?UTF-8?q?Add=20function=20to=20convert=20CTL=20->=20?=
=?UTF-8?q?=CE=BC=20Calculus?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Needs a #'gensym implementation for variable names still
---
src/lib/CoAlgFormula.ml | 18 ++++++++++++++++++
1 file changed, 18 insertions(+)
diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index fc59e57..4ee7797 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -212,6 +212,24 @@ let convertToGML formula = (* tries to convert a formula to a pure GML formula *
in
convert_post helper formula
+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
+ in
+ convert_post helper formula
+
(** Appends a string representation of a formula to a string buffer.
Parentheses are ommited where possible
where the preference rules are defined as usual.
--
GitLab