From 7b944a64e176ec8c0e3da8a22666c6b39b29f63d Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 4 Nov 2015 19:19:08 +0100
Subject: [PATCH] =?UTF-8?q?Add=20CTL=20and=20=CE=BC-Calculus=20Constructor?=
 =?UTF-8?q?s=20to=20convert=5Fpost?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Needed e.g. to implement the CTL → μ conversion
---
 src/lib/CoAlgFormula.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/lib/CoAlgFormula.ml b/src/lib/CoAlgFormula.ml
index 422a926..bd52c9d 100644
--- a/src/lib/CoAlgFormula.ml
+++ b/src/lib/CoAlgFormula.ml
@@ -153,7 +153,7 @@ let rec convert_post func formula = (* run over all subformulas in post order *)
   (* replace parts of the formula *)
   let formula = (match formula with
   (* 0-ary constructors *)
-  | TRUE | FALSE | AP _ -> formula
+  | TRUE | FALSE | AP _ | VAR _ -> formula
   | CONST _
   | CONSTN _ -> formula
   (* unary *)
@@ -178,7 +178,15 @@ let rec convert_post func formula = (* run over all subformulas in post order *)
   | NORM(a, b) -> NORM(c a, c b)
   | NORMN(a, b) -> NORMN(c a, c b)
   | CHC (a,b) -> CHC (c a, c b)
-  | FUS (s,a) -> FUS (s, c a)) in
+  | FUS (s,a) -> FUS (s, c a)
+  | MU (n, f1) -> MU (n, c f1)
+  | NU (n, f1) -> NU (n, c f1)
+  | AF f1 -> AF (c f1)
+  | EF f1 -> EF (c f1)
+  | AG f1 -> AG (c f1)
+  | EG f1 -> EG (c f1)
+  | AU (f1, f2) -> AU (c f1, c f2)
+  | EU (f1, f2) -> AU (c f1, c f2))in
   func formula
 
 let convertToK formula = (* tries to convert a formula to a pure K formula *)
-- 
GitLab