From 1b17ef3ccddbc66e4af677882f9910b390bf391f Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 13 Apr 2016 02:18:49 +0200
Subject: [PATCH] Fix bug in FL calculation and refocusing after states
---
src/lib/CoAlgLogics.ml | 14 ++------------
src/lib/CoAlgMisc.ml | 4 +++-
2 files changed, 5 insertions(+), 13 deletions(-)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index ee274e3..853e5ae 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -27,16 +27,6 @@ let mkRuleList_MultiModalK sort bs defer sl : rule list =
*)
assert (List.length sl = 1);
let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
- let deferral =
- if refocusing then begin
- print_endline ("Empty focus (Modal step) at\n" ^ (bsetToString sort bs));
- let newdef = bsetCopy bs in
- bsetRem newdef !S.bstrue;
- newdef
- end
- else
- defer
- in
let dep f bsl = (* dependencies for formula f (f is a diamond) *)
assert (List.length bsl = 1); (* -+ *)
let bs1 = List.hd bsl in (* -+-> [bs1] := bsl *)
@@ -70,8 +60,8 @@ let mkRuleList_MultiModalK sort bs defer sl : rule list =
(* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
let nextf1 = (lfGetDest1 sort f1) in
bsetAdd bs1 nextf1;
- (if (bsetMem deferral f1) &&
- (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1) then
+ (if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
+ ((bsetMem defer f1) && (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1)) then
bsetAdd defer1 nextf1;)
else ()
in
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 2f5fd5e..504a030 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -891,7 +891,9 @@ let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
else ();
if C.HcFHt.mem vset.(s) f &&
- compare (C.HcFHt.find vset.(s) f) deferral = 0 then ()
+ (compare (C.HcFHt.find vset.(s) f) deferral = 0) ||
+ compare deferral "ε" = 0)
+ then ()
else
let () = C.HcFHt.add vset.(s) f deferral in
let () = C.HcFHt.add fset.(s) f () in
--
GitLab