From 46cd6856c9ccdd0dffe1a37f2ea79be5d259f142 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Fri, 8 Apr 2016 02:26:42 +0200
Subject: [PATCH] Preliminarily mark States with no childs Sat in
propagateSatMu
Should actually happen when the State changes from `Expandable` to
`Open` and trigger the propagateSatMu but for now just do it in
propagateSatMu so we can observe the algorithm working.
---
src/lib/CoAlgReasoner.ml | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 5f5653d..cf35e05 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -129,13 +129,19 @@ let propagateSatMu () =
setAddState setSatStates state
| Expandable
| Open ->
- setAddState setStates state;
- if bsetCompare (stateGetDeferral state) emptySet == 0
+ if stateGetStatus state == Open && List.length (stateGetRules state) == 0
then begin
+ setAddState setSatStates state;
+ stateSetStatus state Sat
+ end else begin
+ setAddState setStates state;
+ if bsetCompare (stateGetDeferral state) emptySet == 0
+ then begin
print_endline (stateToString state);
setAddState setFinishingStates state
end
- else ()
+ else ()
+ end
in
let coreCollector core =
match coreGetStatus core with
--
GitLab