From 2ebb5e8383f84d7cb385aa8a0039d32835206c02 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 5 May 2020 14:40:39 +0200
Subject: [PATCH] Fixed detection of fixpoints.

---
 .../modelchecker/ApproximatePOMDPModelchecker.cpp         | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
index d72d56a6d..788c96225 100644
--- a/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
+++ b/src/storm-pomdp/modelchecker/ApproximatePOMDPModelchecker.cpp
@@ -587,14 +587,20 @@ namespace storm {
                                 // First, check whether this action has been rewired since the last refinement of one of the successor observations (i.e. whether rewiring would actually change the successor states)
                                 assert(overApproximation->currentStateHasOldBehavior());
                                 if (overApproximation->getCurrentStateActionExplorationWasDelayed(action) || overApproximation->currentStateHasSuccessorObservationInObservationSet(action, refinedObservations)) {
-                                    fixPoint = false;
                                     // Then, check whether the other criteria for rewiring are satisfied
                                     if (!restoreAllActions && overApproximation->actionAtCurrentStateWasOptimal(action)) {
                                         // Do the rewiring now! (Case 3.1)
                                         expandCurrentAction = true;
+                                        fixPoint = false;
                                     } else {
                                         // Delay the rewiring (Case 3.2.2)
                                         overApproximation->setCurrentChoiceIsDelayed(action);
+                                        if (fixPoint) {
+                                            // Check whether this delay means that a fixpoint has not been reached
+                                            if (!overApproximation->getCurrentStateActionExplorationWasDelayed(action) || (overApproximation->currentStateIsOptimalSchedulerReachable() && overApproximation->actionAtCurrentStateWasOptimal(action) && !storm::utility::isZero(gap))) {
+                                                fixPoint = false;
+                                            }
+                                        }
                                     }
                                 } // else { Case 3.2.1 }
                             }