From 0a6a3df52a08c1c20ffba449604e2d9f0b926f4e Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Fri, 8 Apr 2016 02:29:33 +0200
Subject: [PATCH] Fix inclusion condition for A_x
---
src/lib/CoAlgReasoner.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 0035ba3..6a54b71 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -216,7 +216,7 @@ let propagateSatMu () =
*)
let checkFinishingState (state : state) =
let ruleiter (dependencies, corelist) : bool =
- List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable) corelist
+ List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable || not (setMemCore setCores core)) corelist
in
if not (List.exists ruleiter (stateGetRules state)) then begin
setAddState allowedStates state;
@@ -227,7 +227,7 @@ let propagateSatMu () =
* to be considered for the fixpoint
*)
and checkFinishingCore (core : core) =
- if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable)
+ if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable || not (setMemState setStates state))
(coreGetChildren core))
then begin
setAddCore allowedCores core;
--
GitLab