From 6553983f70e1e15aebace9b4cc43caeb62572b20 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 1 Dec 2015 16:48:33 +0100
Subject: [PATCH] Add fixpoint-unfold to detClosure
should now properly calculate the FL-Closure
---
src/lib/CoAlgMisc.ml | 10 ++++++++++
1 file changed, 10 insertions(+)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 4866e4f..54ff973 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -889,6 +889,16 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
else ();
let s1 = List.nth sortlst (if first then 0 else 1) in
detClosure nomTbl hcF fset atset nomset s1 f1
+ (*
+ FL(μ X . φ) = {μ X . φ} ∪ FL(φ[X|->μ X . φ])
+ *)
+ | C.HCMU (name, f1) ->
+ let unfold = C.hc_replace hcF name f f1 in
+ detClosure nomTbl hcF fset atset nomset s unfold
+ | C.HCNU (name, f1) ->
+ let unfold = C.hc_replace hcF name f f1 in
+ detClosure nomTbl hcF fset atset nomset s unfold
+
let detClosureAt hcF atset name f () =
match f.HC.node with
--
GitLab