From a25a68494ebbdf06e8b8243ea5eb161704bcdf96 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 29 Feb 2016 10:37:01 +0100
Subject: [PATCH] Make KD a deferral-tracking Logic
---
src/lib/CoAlgLogics.ml | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index 45d99f4..2a738c5 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -135,7 +135,13 @@ let mkRule_MultiModalKD sort bs defer sl : stateExpander =
let f formula =
if lfGetType sort formula = AxF
&& lfGetDest3 sort formula = r
- then ignore (bsetAdd succs (lfGetDest1 sort formula))
+ then
+ let nextf1 = (lfGetDest1 sort formula) in
+ bsetAdd succs nextf1;
+ ignore (if (bsetMem defer formula) &&
+ (lfGetDeferral sort formula) = (lfGetDeferral sort nextf1)
+ then
+ bsetAdd defer1 nextf1;)
else ()
in
bsetIter f bs;
--
GitLab