From b3ce727f6c8e2a31ddc22d9dc02c1eb4b499b4ed Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 13 Oct 2015 18:47:54 +0200
Subject: [PATCH] fixed minor bug, tests for smt-based permissive schedulers
 (for upper-bounded properties) now passing

Former-commit-id: bf0261e9818c9a7c205c740fb3a310482f4b582c
---
 src/permissivesched/SmtBasedPermissiveSchedulers.h        | 8 +-------
 .../permissiveschedulers/SmtPermissiveSchedulerTest.cpp   | 4 ++--
 2 files changed, 3 insertions(+), 9 deletions(-)

diff --git a/src/permissivesched/SmtBasedPermissiveSchedulers.h b/src/permissivesched/SmtBasedPermissiveSchedulers.h
index 86a41cd78..bfc1530b8 100644
--- a/src/permissivesched/SmtBasedPermissiveSchedulers.h
+++ b/src/permissivesched/SmtBasedPermissiveSchedulers.h
@@ -138,6 +138,7 @@ namespace storm {
                         } else {
                             solver.add(storm::expressions::implies(multistrategyVariables[storage::StateActionPair(s,a)], mProbVariables[s] >= storm::expressions::sum(expressions)));
                         }
+                        expressions.clear();
                     }
                     
                     // (6) and (8) are only necessary for lower-bounded properties.
@@ -192,13 +193,11 @@ namespace storm {
                     
                     std::vector<storage::StateActionPair> availableStateActionPairs;
                     for (uint_fast64_t s : relevantStates) {
-                        std::cout << "considering relevant state " << s << std::endl;
                         for(uint_fast64_t a = 0; a < this->mdp.getNumberOfChoices(s); ++a) {
                             auto stateAndAction = storage::StateActionPair(s,a);
                             
                             auto multistrategyVariable = multistrategyVariables.at(stateAndAction);
                             if (model->getBooleanValue(multistrategyVariable)) {
-                                std::cout << "taking " << a << " in " << s << std::endl;
                                 multistrategyVariablesToTakenMap[multistrategyVariable] = true;
                                 solver.add(multistrategyVariable);
                             } else {
@@ -213,19 +212,15 @@ namespace storm {
                     
                     do {
                         auto multistrategyVariable = multistrategyVariables.at(availableStateActionPairs.back());
-                        std::cout << "trying " << multistrategyVariable.getName() << std::endl;
 
                         result = solver.checkWithAssumptions({ multistrategyVariable });
                         
                         if (result == storm::solver::SmtSolver::CheckResult::Sat) {
-                            std::cout << "succeeded." << std::endl;
                             model = solver.getModel();
                             if (model->getBooleanValue(multistrategyVariable)) {
                                 solver.add(multistrategyVariable);
                                 multistrategyVariablesToTakenMap[multistrategyVariable] = true;
                             }
-                        } else {
-                            std::cout << "failed." << std::endl;
                         }
                         availableStateActionPairs.pop_back();
                         
@@ -233,7 +228,6 @@ namespace storm {
                     
                     mFoundSolution = true;
                 } else {
-                    std::cout << "didnt find one" << std::endl;
                     mFoundSolution = false;
                 }
             }
diff --git a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
index e6aaef836..04f706221 100644
--- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
+++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
@@ -18,8 +18,8 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
 //    ASSERT_TRUE(storm::logic::isLowerBound(formula02.getComparisonType()));
 //    auto formula001 = formulaParser.parseSingleFormulaFromString("P>=0.17 [ F \"one\"]")->asProbabilityOperatorFormula();
     
-    auto formula02b = formulaParser.parseSingleFormulaFromString("P<=0.14 [ F \"one\"]")->asProbabilityOperatorFormula();
-    auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.10 [ F \"one\"]")->asProbabilityOperatorFormula();
+    auto formula02b = formulaParser.parseSingleFormulaFromString("P<=0.16 [ F \"one\"]")->asProbabilityOperatorFormula();
+    auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.05 [ F \"one\"]")->asProbabilityOperatorFormula();
     
     // Customize and perform model-building.
     typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;