From 67b07e541336581e11f3f2eb01b793d800a86268 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Thu, 7 Apr 2016 04:16:04 +0200
Subject: [PATCH] Restrict finishing nodes used as startingpoint

Only finishing nodes with enough Open / Sat children are to be
considered as startingpoints

Also accept already Satisfiable nodes when finding paths
---
 src/lib/CoAlgReasoner.ml | 45 ++++++++++++++++++++++++++++++++--------
 1 file changed, 36 insertions(+), 9 deletions(-)

diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index a2cabcf..76151e6 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -164,13 +164,38 @@ let propagateSatMu () =
   *)
 
   let rec fixpointstep setStates setCores =
-    let allowedStates = setFinishingStates in
-    let allowedCores = setFinishingCores in
+    let allowedStates = setEmptyState () in
+    let allowedCores = setEmptyCore () in
+    let initialStates = setEmptyState () in
+    let initialCores = setEmptyCore () in
+
+    let checkFinishingState (state : state) =
+      let ruleiter (dependencies, corelist) : bool =
+        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable) corelist
+      in
+      if not (List.exists ruleiter (stateGetRules state)) then begin
+        setAddState allowedStates state;
+        setAddState initialStates state
+      end
+    in
+    let checkFinishingCore (core : core) =
+      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable)
+                (coreGetChildren core)) then begin
+        setAddCore allowedCores core;
+        setAddCore initialCores core
+      end
+    in
+    setIterState checkFinishingState setFinishingStates;
+    setIterCore checkFinishingCore setFinishingCores;
 
     let rec visitParentStates (core : core) : unit =
-      if setMemCore allowedCores core then () else begin
+      if not (setMemCore setCores core) then ()
+      else begin
         let children = coreGetChildren core in
-        let acceptable = List.exists (fun (state) -> setMemState allowedStates state) children in
+        let acceptable =
+          List.exists (fun (state : state) -> setMemState allowedStates state || stateGetStatus state == Sat)
+            children
+        in
         if acceptable then begin
           print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as allowed");
           setAddCore allowedCores core;
@@ -180,23 +205,25 @@ let propagateSatMu () =
       end
 
     and visitParentCores (state : state) : unit =
-      if setMemState allowedStates state then () else begin
+      if not (setMemState setStates state) then ()
+      else begin
         let rules = stateGetRules state in
         let ruleiter (dependencies, corelist) =
-          List.exists (fun (core) -> setMemCore allowedCores core) corelist
+          List.exists (fun (core : core) -> setMemCore allowedCores core || coreGetStatus core == Sat)
+            corelist
         in
         let acceptable = List.for_all ruleiter rules in
         if acceptable then begin
           print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as allowed");
           setAddState allowedStates state;
-          List.iter (fun core -> visitParentStates core)
+          List.iter (fun core -> if not (setMemCore allowedCores core) then visitParentStates core)
             (stateGetParents state)
         end
       end
     in
 
-    setIterState visitParentCores setFinishingStates;
-    setIterCore visitParentStates setFinishingCores;
+    setIterState visitParentCores initialStates;
+    setIterCore visitParentStates initialCores;
 
     if (setLengthState setStates) = (setLengthState allowedStates) &&
       (setLengthCore setCores) = (setLengthCore allowedCores)
-- 
GitLab