From 005e23d5d52369a7a464016de3e2d1f3d809328e Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Sun, 10 May 2020 18:28:52 -0700
Subject: [PATCH] two fixes after encoding from non-empty winning regions

---
 .../analysis/MemlessStrategySearchQualitative.cpp   | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp
index 0b1ce1d63..09ec8a8c2 100644
--- a/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp
+++ b/src/storm-pomdp/analysis/MemlessStrategySearchQualitative.cpp
@@ -423,7 +423,7 @@ namespace storm {
             if (!atLeastOneOfStates.empty()) {
                 smtSolver->add(storm::expressions::disjunction(atLeastOneOfStates));
             }
-            smtSolver->push();
+
 
             std::set<storm::expressions::Expression> allOfTheseAssumption;
 
@@ -447,11 +447,13 @@ namespace storm {
                 for (auto const &statesForObservation : statesPerObservation) {
                     schedulerForObs.push_back(0);
                     for (auto const& winningSet : winningRegion.getWinningSetsPerObservation(obs)) {
+                        assert(!winningSet.empty());
+                        assert(obs < schedulerForObs.size());
+                        ++(schedulerForObs[obs]);
+                        auto constant = expressionManager->integer(schedulerForObs[obs]);
                         for (auto const &stateOffset : ~winningSet) {
                             uint64_t state = statesForObservation[stateOffset];
-                            assert(obs < schedulerForObs.size());
-                            ++(schedulerForObs[obs]);
-                            auto constant = expressionManager->integer(schedulerForObs[obs]);
+                            STORM_LOG_TRACE("State " << state << " with observation " << obs << " does not allow scheduler " << constant);
                             // PAPER COMMENT 14:
                             smtSolver->add(!(continuationVarExpressions[state] &&
                                              (schedulerVariableExpressions[obs] == constant)));
@@ -473,14 +475,13 @@ namespace storm {
 
             }
 
+            smtSolver->push();
             for (uint64_t obs = 0; obs < pomdp.getNrObservations(); ++obs) {
                 auto constant = expressionManager->integer(schedulerForObs[obs]);
                 smtSolver->add(schedulerVariableExpressions[obs] <= constant);
                 smtSolver->add(storm::expressions::iff(observationUpdatedExpressions[obs], updateForObservationExpressions[obs]));
             }
 
-
-
             assert(pomdp.getNrObservations() == schedulerForObs.size());