changes in milp permissive scheduler

Former-commit-id: 6b11d01b88

src/permissivesched/MILPPermissiveSchedulers.h

@@ -12,7 +12,7 @@
 #include "../storage/StateActionTargetTuple.h"
 #include "../storage/expressions/Variable.h"
 #include "../solver/LpSolver.h"
-
+#include "../models/sparse/StandardRewardModel.h"
 
 
 namespace storm {
@@ -38,9 +38,10 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
             }
             
                     
-            void calculatePermissiveScheduler(double boundary) override {
-                createMILP(boundary, mPenalties);
+            void calculatePermissiveScheduler(bool lowerBound, double boundary) override {
+                createMILP(lowerBound, boundary, mPenalties);
                 solver.optimize();
+                
                 mCalledOptimizer = true;
             }
             
@@ -50,14 +51,20 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
                 return !solver.isInfeasible();
             }
             
-            MemorylessDeterministicPermissiveScheduler && getScheduler() const override {
+            MemorylessDeterministicPermissiveScheduler getScheduler() const override {
+                assert(mCalledOptimizer);
+                assert(foundSolution());
                 storm::storage::BitVector result(mdp->getNumberOfChoices(), true);
                 for(auto const& entry : multistrategyVariables) {
                     if(!solver.getBinaryValue(entry.second)) {
                         result.set(mdp->getNondeterministicChoiceIndices()[entry.first.getState()]+entry.first.getAction(), false);
                     }
                 }
-                return std::move<MemorylessDeterministicPermissiveScheduler>(result);
+                return MemorylessDeterministicPermissiveScheduler(result);
+            }
+            
+            void dumpLpToFile(std::string const& filename) {
+                solver.writeModelToFile(filename);
             }
             
                     
@@ -107,17 +114,21 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
                                 
                     }
                 }
+                solver.update();
             }
             
-            
-            
-            void createConstraints(double boundary, storm::storage::BitVector const& relevantStates) {
+            void createConstraints(bool lowerBound, double boundary, storm::storage::BitVector const& relevantStates) {
                 // (5) and (7) are omitted on purpose (-- we currenty do not support controllability of actions -- )
                 
                 // (1)
                 assert(mdp->getInitialStates().getNumberOfSetBits() == 1);
                 uint_fast64_t initialStateIndex = mdp->getInitialStates().getNextSetIndex(0);
-                solver.addConstraint("c1", mProbVariables[initialStateIndex] >= solver.getConstant(boundary));
+                assert(relevantStates[initialStateIndex]);
+                if(lowerBound) {
+                    solver.addConstraint("c1", mProbVariables[initialStateIndex] >= solver.getConstant(boundary));
+                } else {
+                    solver.addConstraint("c1", mProbVariables[initialStateIndex] <= solver.getConstant(boundary));
+                }
                 for(uint_fast64_t s : relevantStates) {
                     std::string stateString =  std::to_string(s);
                     storm::expressions::Expression expr = solver.getConstant(0.0);
@@ -139,8 +150,12 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
                             } else if (entry.getValue() != 0 && mGoals.get(entry.getColumn())) {
                                 expr = expr + solver.getConstant(entry.getValue());
                             }
-                        }        
-                        solver.addConstraint("c3-" + sastring, mProbVariables[s] < (solver.getConstant(1) - multistrategyVariables[storage::StateActionPair(s,a)]) + expr);
+                        }
+                        if(lowerBound) {
+                            solver.addConstraint("c3-" + sastring, mProbVariables[s] <= (solver.getConstant(1) - multistrategyVariables[storage::StateActionPair(s,a)]) + expr);
+                        } else {
+                            solver.addConstraint("c3-" + sastring, mProbVariables[s] >= (solver.getConstant(1) - multistrategyVariables[storage::StateActionPair(s,a)]) + expr);
+                        }
                     }
 
                     for(uint_fast64_t a = 0; a < mdp->getNumberOfChoices(s); ++a) {    
@@ -160,12 +175,12 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
                                 storage::StateActionTarget sat = {s,a,entry.getColumn()};
                                 std::string satstring = to_string(sat);
                                 // (8)
-                                assert(mGammaVariables.count(entry.getColumn()) > 0);
-                                assert(mGammaVariables.count(s) > 0);
-                                assert(mBetaVariables.count(sat) > 0);
                                 if(relevantStates[entry.getColumn()]) {
+                                    assert(mGammaVariables.count(entry.getColumn()) > 0);
+                                    assert(mGammaVariables.count(s) > 0);
+                                    assert(mBetaVariables.count(sat) > 0);
                                     solver.addConstraint("c8-" + satstring, mGammaVariables[entry.getColumn()] < mGammaVariables[s] + (solver.getConstant(1) - mBetaVariables[sat]) + mProbVariables[s]); // With rewards, we have to change this.
-                               }
+                                }
                             }
                         }
                                 
@@ -177,14 +192,14 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
             /**
              *
              */
-            void createMILP(double boundary, PermissiveSchedulerPenalties const& penalties) {
+            void createMILP(bool lowerBound, double boundary, PermissiveSchedulerPenalties const& penalties) {
                 storm::storage::BitVector irrelevant = mGoals | mSinks;
                 storm::storage::BitVector relevantStates = ~irrelevant;
                 // Notice that the separated construction of variables and 
                 // constraints slows down the construction of the MILP. 
                 // In the future, we might want to merge this.
                 createVariables(penalties, relevantStates);
-                createConstraints(boundary, relevantStates);
+                createConstraints(lowerBound, boundary, relevantStates);
                 
                 
                 solver.setOptimizationDirection(storm::OptimizationDirection::Minimize);

src/permissivesched/PermissiveSchedulerComputation.h

@@ -26,7 +26,7 @@ namespace storm {
             }
             
                     
-            virtual void calculatePermissiveScheduler(double boundary) = 0;
+            virtual void calculatePermissiveScheduler(bool lowerBound, double boundary) = 0;
             
             void setPenalties(PermissiveSchedulerPenalties penalties) {
                 mPenalties = penalties;
@@ -42,7 +42,7 @@ namespace storm {
             
             virtual bool foundSolution() const = 0;
             
-            virtual MemorylessDeterministicPermissiveScheduler&&  getScheduler() const = 0;
+            virtual MemorylessDeterministicPermissiveScheduler getScheduler() const = 0;
             
        
         };

src/permissivesched/PermissiveSchedulers.cpp

@@ -5,7 +5,8 @@
 #include "../modelchecker/propositional/SparsePropositionalModelChecker.h"
 #include "../modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "MILPPermissiveSchedulers.h"
-
+#include "src/exceptions/NotImplementedException.h"
+#include "src/utility/macros.h"
 
 namespace storm {
     namespace ps {
@@ -18,13 +19,16 @@ namespace storm {
             goalstates = storm::utility::graph::performProb1E(*mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
             storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(*mdp,backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates);
 
-            auto solver = storm::utility::solver::getLpSolver("Gurobi");
+            auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi);
             MilpPermissiveSchedulerComputation comp(*solver, mdp, goalstates, sinkstates);
-            comp.calculatePermissiveScheduler(safeProp.getBound());
+            STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported");
+            comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound());
+            comp.dumpLpToFile("milpdump.lp");
+            std::cout << "Found Solution: " << (comp.foundSolution() ? "yes" : "no") << std::endl;
             if(comp.foundSolution()) {
                 return boost::optional<MemorylessDeterministicPermissiveScheduler>(comp.getScheduler());
             } else {
-                return boost::optional<MemorylessDeterministicPermissiveScheduler>(comp.getScheduler());
+                return boost::optional<MemorylessDeterministicPermissiveScheduler>();
             }
         }
          

src/permissivesched/PermissiveSchedulers.h

@@ -10,13 +10,22 @@ namespace storm {
     namespace ps {
         
         class PermissiveScheduler {
-            
+        public:
+            virtual ~PermissiveScheduler() = default;
         };
         
         class MemorylessDeterministicPermissiveScheduler  : public PermissiveScheduler {
             storm::storage::BitVector memdetschedulers;
         public:
+            virtual ~MemorylessDeterministicPermissiveScheduler() = default;
+            MemorylessDeterministicPermissiveScheduler(MemorylessDeterministicPermissiveScheduler&&) = default;
+            MemorylessDeterministicPermissiveScheduler(MemorylessDeterministicPermissiveScheduler const&) = delete;
+            
+            
             MemorylessDeterministicPermissiveScheduler(storm::storage::BitVector const& allowedPairs) : memdetschedulers(allowedPairs) {}
+            MemorylessDeterministicPermissiveScheduler(storm::storage::BitVector && allowedPairs) : memdetschedulers(std::move(allowedPairs)) {}
+            
+            
         };
         
         boost::optional<MemorylessDeterministicPermissiveScheduler> computePermissiveSchedulerViaMILP(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp);

test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp

@@ -6,25 +6,38 @@
 #include "src/permissivesched/PermissiveSchedulers.h"
 #include "src/builder/ExplicitPrismModelBuilder.h"
 
+#include "src/models/sparse/StandardRewardModel.h"
+
 
 TEST(MilpPermissiveSchedulerTest, DieSelection) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_selection.nm");
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_c1.nm");
     storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
-    std::cout << " We are now here " << std::endl;
-    auto formula = formulaParser.parseSingleFormulaFromString("P<=0.2 [ F \"one\"]")->asProbabilityOperatorFormula();
-    std::cout << formula << std::endl;
+    
+    auto formula02 = formulaParser.parseSingleFormulaFromString("P>=0.10 [ F \"one\"]")->asProbabilityOperatorFormula();
+    ASSERT_TRUE(storm::logic::isLowerBound(formula02.getComparisonType()));
+    auto formula001 = formulaParser.parseSingleFormulaFromString("P>=0.17 [ F \"one\"]")->asProbabilityOperatorFormula();
+    
+    auto formula02b = formulaParser.parseSingleFormulaFromString("P<=0.10 [ F \"one\"]")->asProbabilityOperatorFormula();
+    auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.17 [ F \"one\"]")->asProbabilityOperatorFormula();
     
     // Customize and perform model-building.
     typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
     
-    options = typename storm::builder::ExplicitPrismModelBuilder<double>::Options(formula);
+    options = typename storm::builder::ExplicitPrismModelBuilder<double>::Options(formula02);
     options.addConstantDefinitionsFromString(program, "");
     options.buildCommandLabels = true;
     
     std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options)->as<storm::models::sparse::Mdp<double>>();
     
-    storm::ps::computePermissiveSchedulerViaMILP(mdp, formula);
-    
+     boost::optional<storm::ps::MemorylessDeterministicPermissiveScheduler> perms = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02);
+     EXPECT_NE(perms, boost::none);
+     boost::optional<storm::ps::MemorylessDeterministicPermissiveScheduler> perms2 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001);
+     EXPECT_EQ(perms2, boost::none);
+     
+     boost::optional<storm::ps::MemorylessDeterministicPermissiveScheduler> perms3 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02b);
+     EXPECT_EQ(perms3, boost::none);
+     boost::optional<storm::ps::MemorylessDeterministicPermissiveScheduler> perms4 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001b);
+     EXPECT_NE(perms4, boost::none);
  // 
     
 }