From fe81b9880a1ec821dd1dfca9b59bebbcf879503a Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Sat, 9 Apr 2016 03:17:52 +0200
Subject: [PATCH] Make real empty set for deferral (not including True)
---
src/lib/CoAlgLogics.ml | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index c151b7f..ee274e3 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -28,8 +28,12 @@ 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
- bsetCopy bs
+ 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
@@ -131,7 +135,7 @@ let mkRule_MultiModalKD sort bs defer sl : stateExpander =
res
in
let succs = bsetMake () in (* succs := {D | ∀r.D ∈ bs *)
- let defer1 = bsetMake () in (* TODO: actually track deferrals *)
+ let defer1 = bsetMakeRealEmpty () in (* TODO: actually track deferrals *)
let f formula =
if lfGetType sort formula = AxF
&& lfGetDest3 sort formula = r
--
GitLab