From 3f0733729c7f42338e69ac3905c363ddc48cbc21 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Sun, 10 Apr 2016 23:12:14 +0200
Subject: [PATCH] Treat Sat states like finishing states
With Sat states only treated like other states in the second fixpoint
iteration, the outer fixpoint was not ncessarily monononously decreasing
causing wrong results when in the first round the same number of nodes
got removed as added due to sat states.
---
src/lib/CoAlgReasoner.ml | 10 +++-------
1 file changed, 3 insertions(+), 7 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 1a87848..facbe45 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -118,20 +118,18 @@ let propagateSatMu () =
let setFinishingCores = setEmptyCore () in
let setStates = setEmptyState () in
let setCores = setEmptyCore () in
- let setSatStates = setEmptyState () in
- let setSatCores = setEmptyCore () in
let emptySet = bsetMakeRealEmpty () in
let stateCollector state =
match stateGetStatus state with
| Unsat -> ()
| Sat ->
- setAddState setSatStates state
+ setAddState setFinishingStates state
| Expandable -> ()
| Open ->
if stateGetStatus state == Open && List.length (stateGetRules state) == 0 || bsetCompare (bsetMake ()) (stateGetBs state) == 0
then begin
- setAddState setSatStates state;
+ setAddState setFinishingStates state;
stateSetStatus state Sat
end else begin
setAddState setStates state;
@@ -147,7 +145,7 @@ let propagateSatMu () =
match coreGetStatus core with
| Unsat -> ()
| Sat ->
- setAddCore setSatCores core
+ setAddCore setFinishingCores core
| Expandable
| Open ->
setAddCore setCores core;
@@ -240,8 +238,6 @@ let propagateSatMu () =
in
setIterState checkFinishingState setFinishingStates;
setIterCore checkFinishingCore setFinishingCores;
- setIterState visitParentCores setSatStates;
- setIterCore visitParentStates setSatCores;
if (setLengthState setStates) = (setLengthState allowedStates) &&
--
GitLab