Merge branch 'future' into python_api

Former-commit-id: eb736f1950

CMakeLists.txt

@@ -102,7 +102,7 @@ if(USE_CARL)
      set(STORM_HAVE_CARL ON)
     endif()
 
-    find_package(smtrat QUIET)
+    #find_package(smtrat QUIET)
     if(smtrat_FOUND)
         set(STORM_HAVE_SMTRAT ON)
     endif()
@@ -412,6 +412,7 @@ file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/sr
 file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp)
 file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp)
+file(GLOB_RECURSE STORM_PERMISSIVESCHEDULER_FILES ${PROJECT_SOURCE_DIR}/src/permissivesched/*.h ${PROJECT_SOURCE_DIR}/src/permissivesched/*.cpp)
 file(GLOB STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp)
 file(GLOB_RECURSE STORM_MODELS_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/models/sparse/*.h ${PROJECT_SOURCE_DIR}/src/models/sparse/*.cpp)
 file(GLOB_RECURSE STORM_MODELS_SYMBOLIC_FILES ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.h ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.cpp)
@@ -462,6 +463,7 @@ source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_
 source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES})
 source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES})
 source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES})
+source_group(permissiveschedulers FILES ${STORM_PERMISSIVESCHEDULER_FILES})
 source_group(models FILES ${STORM_MODELS_FILES})
 source_group(models\\sparse FILES ${STORM_MODELS_SPARSE_FILES})
 source_group(models\\symbolic FILES ${STORM_MODELS_SYMBOLIC_FILES})

src/models/sparse/Ctmc.cpp

@@ -40,9 +40,9 @@ namespace storm {
             
             template class Ctmc<double>;
 
-//#ifdef STORM_HAVE_CARL
-//            template class Ctmc<storm::RationalFunction>;
-//#endif
+#ifdef STORM_HAVE_CARL
+            template class Ctmc<storm::RationalFunction>;
+#endif
             
         } // namespace sparse
     } // namespace models

src/permissivesched/MILPPermissiveSchedulers.h

@@ -0,0 +1,213 @@
+#ifndef MILPPERMISSIVESCHEDULERS_H
+#define	MILPPERMISSIVESCHEDULERS_H
+
+
+#include <memory>
+#include <unordered_map>
+
+#include "PermissiveSchedulerComputation.h"
+
+#include "../storage/BitVector.h"
+#include "../storage/StateActionPair.h"
+#include "../storage/StateActionTargetTuple.h"
+#include "../storage/expressions/Variable.h"
+#include "../solver/LpSolver.h"
+#include "../models/sparse/StandardRewardModel.h"
+
+
+namespace storm {
+    namespace ps {
+        
+class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation {
+        private:
+           
+            bool mCalledOptimizer = false;
+            storm::solver::LpSolver& solver;
+            std::unordered_map<storm::storage::StateActionPair, storm::expressions::Variable> multistrategyVariables;
+            std::unordered_map<uint_fast64_t, storm::expressions::Variable> mProbVariables;
+            std::unordered_map<uint_fast64_t, storm::expressions::Variable> mAlphaVariables;
+            std::unordered_map<storm::storage::StateActionTarget, storm::expressions::Variable> mBetaVariables;
+            std::unordered_map<uint_fast64_t, storm::expressions::Variable> mGammaVariables;
+            
+        public:
+            
+            MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates)
+                :  PermissiveSchedulerComputation(mdp, goalstates, sinkstates), solver(milpsolver)
+            {
+                
+            }
+            
+                    
+            void calculatePermissiveScheduler(bool lowerBound, double boundary) override {
+                createMILP(lowerBound, boundary, mPenalties);
+                solver.optimize();
+                
+                mCalledOptimizer = true;
+            }
+            
+            
+            bool foundSolution() const override {
+                assert(mCalledOptimizer);
+                return !solver.isInfeasible();
+            }
+            
+            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 MemorylessDeterministicPermissiveScheduler(result);
+            }
+            
+            void dumpLpToFile(std::string const& filename) {
+                solver.writeModelToFile(filename);
+            }
+            
+                    
+        private:
+            
+            /**
+             * 
+             */
+            void createVariables(PermissiveSchedulerPenalties const& penalties, storm::storage::BitVector const& relevantStates) {
+                // We need the unique initial state later, so we get that one before looping.
+                assert(mdp->getInitialStates().getNumberOfSetBits() == 1);
+                uint_fast64_t initialStateIndex = mdp->getInitialStates().getNextSetIndex(0);
+                    
+                storm::expressions::Variable var;
+                for(uint_fast64_t s : relevantStates) {
+                    // Create x_s variables
+                    // Notice that only the initial probability appears in the objective.
+                    if(s == initialStateIndex) {
+                        var = solver.addLowerBoundedContinuousVariable("x_" + std::to_string(s), 0.0, -1.0);
+                    } else {
+                        var = solver.addLowerBoundedContinuousVariable("x_" + std::to_string(s), 0.0);
+                    }
+                    mProbVariables[s] = var;
+                    // Create alpha_s variables
+                    var = solver.addBinaryVariable("alp_" + std::to_string(s));
+                    mAlphaVariables[s] = var;
+                    // Create gamma_s variables
+                    var = solver.addBoundedContinuousVariable("gam_" + std::to_string(s), 0.0, 1.0);
+                    mGammaVariables[s] = var;
+                    for(uint_fast64_t a = 0; a < mdp->getNumberOfChoices(s); ++a) {
+                        auto stateAndAction = storage::StateActionPair(s,a);
+                        
+                        // Create y_(s,a) variables
+                        double penalty = penalties.get(stateAndAction);
+                        var = solver.addBinaryVariable("y_"  + std::to_string(s) + "_" + std::to_string(a), -penalty);
+                        multistrategyVariables[stateAndAction] = var;
+                        
+                        // Create beta_(s,a,t) variables
+                        // Iterate over successors of s via a.
+                        for(auto const& entry : mdp->getTransitionMatrix().getRow(mdp->getNondeterministicChoiceIndices()[s]+a)) {
+                            if(entry.getValue() != 0) {
+                                storage::StateActionTarget sat = {s,a,entry.getColumn()};
+                                var = solver.addBinaryVariable("beta_" + to_string(sat));
+                                mBetaVariables[sat] = var;
+                            }
+                        }
+                                
+                    }
+                }
+                solver.update();
+            }
+            
+            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);
+                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);
+                    // (2)
+                    for(uint_fast64_t a = 0; a < mdp->getNumberOfChoices(s); ++a) {
+                        expr = expr + multistrategyVariables[storage::StateActionPair(s,a)];
+                    }   
+                    solver.addConstraint("c2-" + stateString, solver.getConstant(1) <= expr);
+                    // (5)
+                    solver.addConstraint("c5-" + std::to_string(s), mProbVariables[s] <= mAlphaVariables[s]);
+               
+                    // (3) For the relevant states.
+                    for(uint_fast64_t a = 0; a < mdp->getNumberOfChoices(s); ++a) {
+                        std::string sastring(stateString + "_" + std::to_string(a));
+                        expr = solver.getConstant(0.0);       
+                        for(auto const& entry : mdp->getTransitionMatrix().getRow(mdp->getNondeterministicChoiceIndices()[s]+a)) {
+                            if(entry.getValue() != 0 && relevantStates.get(entry.getColumn())) {
+                                expr = expr + solver.getConstant(entry.getValue()) * mProbVariables[entry.getColumn()];
+                            } else if (entry.getValue() != 0 && mGoals.get(entry.getColumn())) {
+                                expr = expr + solver.getConstant(entry.getValue());
+                            }
+                        }
+                        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) {    
+                        // (6)
+                        std::string sastring(stateString + "_" + std::to_string(a));
+                        expr = solver.getConstant(0.0);     
+                        for(auto const& entry : mdp->getTransitionMatrix().getRow(mdp->getNondeterministicChoiceIndices()[s]+a)) {
+                            if(entry.getValue() != 0) {
+                                storage::StateActionTarget sat = {s,a,entry.getColumn()};
+                                expr = expr + mBetaVariables[sat];
+                            }
+                        }        
+                        solver.addConstraint("c6-" + sastring, multistrategyVariables[storage::StateActionPair(s,a)] == (solver.getConstant(1) - mAlphaVariables[s]) + expr);
+                        
+                        for(auto const& entry : mdp->getTransitionMatrix().getRow(mdp->getNondeterministicChoiceIndices()[s]+a)) {
+                            if(entry.getValue() != 0) {
+                                storage::StateActionTarget sat = {s,a,entry.getColumn()};
+                                std::string satstring = to_string(sat);
+                                // (8)
+                                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.
+                                }
+                            }
+                        }
+                                
+                    }
+                }
+            }
+                
+            
+            /**
+             *
+             */
+            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(lowerBound, boundary, relevantStates);
+                
+                
+                solver.setOptimizationDirection(storm::OptimizationDirection::Minimize);
+                
+            }
+        };
+    }
+}
+
+#endif	/* MILPPERMISSIVESCHEDULERS_H */
+

src/permissivesched/PermissiveSchedulerComputation.h

@@ -0,0 +1,55 @@
+#ifndef PERMISSIVESCHEDULERCOMPUTATION_H
+#define	PERMISSIVESCHEDULERCOMPUTATION_H
+
+#include <memory>
+
+#include "../storage/BitVector.h"
+#include "../models/sparse/Mdp.h"
+#include "PermissiveSchedulerPenalty.h"
+#include "PermissiveSchedulers.h"
+
+namespace storm {
+    namespace ps {
+        class PermissiveSchedulerComputation {
+        protected:
+            std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
+            storm::storage::BitVector const& mGoals;
+            storm::storage::BitVector const& mSinks;
+            PermissiveSchedulerPenalties mPenalties;
+            
+        public:
+            
+            PermissiveSchedulerComputation(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates)
+                : mdp(mdp), mGoals(goalstates), mSinks(sinkstates)
+            {
+                
+            }
+            
+                    
+            virtual void calculatePermissiveScheduler(bool lowerBound, double boundary) = 0;
+            
+            void setPenalties(PermissiveSchedulerPenalties penalties) {
+                mPenalties = penalties;
+            }
+            
+            PermissiveSchedulerPenalties const& getPenalties() const {
+                return mPenalties;
+            }
+            
+            PermissiveSchedulerPenalties & getPenalties() {
+                return mPenalties;
+            }
+            
+            virtual bool foundSolution() const = 0;
+            
+            virtual MemorylessDeterministicPermissiveScheduler getScheduler() const = 0;
+            
+       
+        };
+        
+    }
+}
+
+
+#endif	/* PERMISSIVESCHEDULERCOMPUTATION_H */
+

src/permissivesched/PermissiveSchedulerPenalty.h

@@ -0,0 +1,53 @@
+#ifndef PERMISSIVESCHEDULERPENALTY_H
+#define	PERMISSIVESCHEDULERPENALTY_H
+
+#include <unordered_map> 
+
+#include "../storage/StateActionPair.h"
+
+namespace storm {
+    namespace ps {
+
+        class PermissiveSchedulerPenalties {
+                    
+             std::unordered_map<storage::StateActionPair, double> mPenalties;
+
+        public:
+            double get(uint_fast64_t state, uint_fast64_t action) const {
+                return get(storage::StateActionPair(state, action));
+
+            }
+
+
+            double get(storage::StateActionPair const& sap) const {
+                auto it = mPenalties.find(sap);
+                if(it == mPenalties.end()) {
+                    return 1.0;
+                }
+                else {
+                    return it->second;
+                }
+            }
+
+            void set(uint_fast64_t state, uint_fast64_t action, double penalty) {
+                assert(penalty >= 1.0);
+                if(penalty == 1.0) {
+                    auto it = mPenalties.find(std::make_pair(state, action));
+                    if(it != mPenalties.end()) {
+                        mPenalties.erase(it);
+                    }
+                } else {
+                    mPenalties.emplace(std::make_pair(state, action), penalty);
+                }
+            }
+
+            void clear() {
+                mPenalties.clear();
+            }
+        };
+    }
+}
+
+
+#endif	/* PERMISSIVESCHEDULERPENALTY_H */
+

src/permissivesched/PermissiveSchedulers.cpp

@@ -0,0 +1,43 @@
+#include "PermissiveSchedulers.h"
+#include "../storage/BitVector.h"
+#include "../utility/solver.h"
+#include "../utility/graph.h"
+#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 {
+        
+         boost::optional<MemorylessDeterministicPermissiveScheduler> computePermissiveSchedulerViaMILP(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
+            storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<double>> propMC(*mdp);
+            assert(safeProp.getSubformula().isEventuallyFormula());
+            auto backwardTransitions = mdp->getBackwardTransitions();
+            storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            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", storm::solver::LpSolverTypeSelection::Gurobi);
+            MilpPermissiveSchedulerComputation comp(*solver, mdp, goalstates, sinkstates);
+            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>();
+            }
+        }
+         
+         boost::optional<MemorylessDeterministicPermissiveScheduler> computePermissiveSchedulerViaMC(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
+             
+         }
+         
+         boost::optional<MemorylessDeterministicPermissiveScheduler> computerPermissiveSchedulerViaSMT(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
+             
+         }
+    }
+}

src/permissivesched/PermissiveSchedulers.h

@@ -0,0 +1,37 @@
+
+#ifndef PERMISSIVESCHEDULERS_H
+#define	PERMISSIVESCHEDULERS_H
+
+#include "../logic/ProbabilityOperatorFormula.h"
+#include "../models/sparse/Mdp.h"
+
+
+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);
+    }
+}
+
+
+#endif	/* PERMISSIVESCHEDULERS_H */
+

src/permissivesched/SmtBasedPermissiveSchedulers.h

@@ -0,0 +1,7 @@
+#ifndef SMTBASEDPERMISSIVESCHEDULERS_H
+#define	SMTBASEDPERMISSIVESCHEDULERS_H
+
+
+
+#endif	/* SMTBASEDPERMISSIVESCHEDULERS_H */
+

test/functional/builder/die_selection.nm

@@ -0,0 +1,45 @@
+// Knuth's model of a fair die using only fair coins
+mdp
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the dice
+	d : [0..6] init 0;
+	
+	[fair]      s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+        [ufair1]    s=0 -> 0.6 : (s'=1) + 0.4 : (s'=2);
+        [ufair2]    s=0 -> 0.7 : (s'=1) + 0.3 : (s'=2);
+	[fair]      s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[ufair1]    s=1 -> 0.6 : (s'=3) + 0.4 : (s'=4);
+        [ufair2]    s=1 -> 0.7 : (s'=3) + 0.3 : (s'=4);
+        [fair]      s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[ufair1]    s=2 -> 0.6 : (s'=5) + 0.4 : (s'=6);
+	[ufair2]    s=2 -> 0.7 : (s'=5) + 0.3 : (s'=6);
+        [fair]      s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[ufair1]    s=3 -> 0.6 : (s'=1) + 0.4 : (s'=7) & (d'=1);
+	[ufair2]    s=3 -> 0.7 : (s'=1) + 0.3 : (s'=7) & (d'=1);
+	[fair]      s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[ufair1]    s=4 -> 0.6 : (s'=7) & (d'=2) + 0.4 : (s'=7) & (d'=3);
+	[ufair2]    s=4 -> 0.7 : (s'=7) & (d'=2) + 0.3 : (s'=7) & (d'=3);
+	[fair]      s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[ufair1]    s=5 -> 0.6 : (s'=2) + 0.4 : (s'=7) & (d'=6);
+	[ufair2]    s=5 -> 0.7 : (s'=2) + 0.3 : (s'=7) & (d'=6);
+	[]          s=7 -> 1: (s'=7);
+	
+endmodule
+
+rewards "coin_flips"
+	[fair] s<7 : 1;
+	[ufair1] s<7 : 1;
+	[ufair2] s<7 : 1;
+endrewards
+
+label "one" = s=7&d=1;
+label "two" = s=7&d=2;
+label "three" = s=7&d=3;
+label "four" = s=7&d=4;
+label "five" = s=7&d=5;
+label "six" = s=7&d=6;
+label "done" = s=7;

test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp

@@ -0,0 +1,43 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/parser/PrismParser.h"
+#include "src/parser/FormulaParser.h"
+#include "src/logic/Formulas.h"
+#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_c1.nm");
+    storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
+    
+    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(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>>();
+    
+     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);
+ // 
+    
+}