diff --git a/src/permissivesched/MILPPermissiveSchedulers.h b/src/permissivesched/MILPPermissiveSchedulers.h index d25179225..6d608436b 100644 --- a/src/permissivesched/MILPPermissiveSchedulers.h +++ b/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(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); diff --git a/src/permissivesched/PermissiveSchedulerComputation.h b/src/permissivesched/PermissiveSchedulerComputation.h index 5582ffc36..a0e135a0f 100644 --- a/src/permissivesched/PermissiveSchedulerComputation.h +++ b/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; }; diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp index 53f1039a8..f484e0ee0 100644 --- a/src/permissivesched/PermissiveSchedulers.cpp +++ b/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(comp.getScheduler()); } else { - return boost::optional(comp.getScheduler()); + return boost::optional(); } } diff --git a/src/permissivesched/PermissiveSchedulers.h b/src/permissivesched/PermissiveSchedulers.h index d9bbd4e74..1f9fcbec8 100644 --- a/src/permissivesched/PermissiveSchedulers.h +++ b/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 computePermissiveSchedulerViaMILP(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp); diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index ad300df32..a6d18d510 100644 --- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/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::Options options; - options = typename storm::builder::ExplicitPrismModelBuilder::Options(formula); + options = typename storm::builder::ExplicitPrismModelBuilder::Options(formula02); options.addConstantDefinitionsFromString(program, ""); options.buildCommandLabels = true; std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options)->as>(); - storm::ps::computePermissiveSchedulerViaMILP(mdp, formula); - + boost::optional perms = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02); + EXPECT_NE(perms, boost::none); + boost::optional perms2 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001); + EXPECT_EQ(perms2, boost::none); + + boost::optional perms3 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02b); + EXPECT_EQ(perms3, boost::none); + boost::optional perms4 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001b); + EXPECT_NE(perms4, boost::none); // }