diff --git a/src/permissivesched/MILPPermissiveSchedulers.h b/src/permissivesched/MILPPermissiveSchedulers.h index fd171bc5a..5b3bd5c91 100644 --- a/src/permissivesched/MILPPermissiveSchedulers.h +++ b/src/permissivesched/MILPPermissiveSchedulers.h @@ -13,12 +13,14 @@ #include "../storage/expressions/Variable.h" #include "../solver/LpSolver.h" #include "../models/sparse/StandardRewardModel.h" +#include "PermissiveSchedulers.h" namespace storm { namespace ps { - -class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation { + + template +class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation { private: bool mCalledOptimizer = false; @@ -31,15 +33,15 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation public: - MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, std::shared_ptr> mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates) - : PermissiveSchedulerComputation(mdp, goalstates, sinkstates), solver(milpsolver) + MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, storm::models::sparse::Mdp const& 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); + createMILP(lowerBound, boundary, this->mPenalties); solver.optimize(); mCalledOptimizer = true; @@ -51,13 +53,13 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation return !solver.isInfeasible(); } - SubMDPPermissiveScheduler getScheduler() const override { + SubMDPPermissiveScheduler getScheduler() const override { assert(mCalledOptimizer); assert(foundSolution()); - SubMDPPermissiveScheduler result(*mdp, true); + SubMDPPermissiveScheduler result(this->mdp, true); for(auto const& entry : multistrategyVariables) { if(!solver.getBinaryValue(entry.second)) { - result.disable(mdp->getChoiceIndex(entry.first)); + result.disable(this->mdp.getChoiceIndex(entry.first)); } } return result; @@ -75,8 +77,8 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation */ 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); + assert(this->mdp.getInitialStates().getNumberOfSetBits() == 1); + uint_fast64_t initialStateIndex = this->mdp.getInitialStates().getNextSetIndex(0); storm::expressions::Variable var; for(uint_fast64_t s : relevantStates) { @@ -94,7 +96,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation // 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) { + for(uint_fast64_t a = 0; a < this->mdp.getNumberOfChoices(s); ++a) { auto stateAndAction = storage::StateActionPair(s,a); // Create y_(s,a) variables @@ -104,7 +106,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation // Create beta_(s,a,t) variables // Iterate over successors of s via a. - for(auto const& entry : mdp->getTransitionMatrix().getRow(mdp->getNondeterministicChoiceIndices()[s]+a)) { + for(auto const& entry : this->mdp.getTransitionMatrix().getRow(this->mdp.getNondeterministicChoiceIndices()[s]+a)) { if(entry.getValue() != 0) { storage::StateActionTarget sat = {s,a,entry.getColumn()}; var = solver.addBinaryVariable("beta_" + to_string(sat)); @@ -123,8 +125,8 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation // (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(this->mdp.getInitialStates().getNumberOfSetBits() == 1); + uint_fast64_t initialStateIndex = this->mdp.getInitialStates().getNextSetIndex(0); assert(relevantStates[initialStateIndex]); if(lowerBound) { solver.addConstraint("c1", mProbVariables[initialStateIndex] >= solver.getConstant(boundary)); @@ -135,7 +137,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation 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) { + for(uint_fast64_t a = 0; a < this->mdp.getNumberOfChoices(s); ++a) { expr = expr + multistrategyVariables[storage::StateActionPair(s,a)]; } solver.addConstraint("c2-" + stateString, solver.getConstant(1) <= expr); @@ -143,13 +145,13 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation 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) { + for(uint_fast64_t a = 0; a < this->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)) { + for(auto const& entry : this->mdp.getTransitionMatrix().getRow(this->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())) { + } else if (entry.getValue() != 0 && this->mGoals.get(entry.getColumn())) { expr = expr + solver.getConstant(entry.getValue()); } } @@ -160,11 +162,11 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation } } - for(uint_fast64_t a = 0; a < mdp->getNumberOfChoices(s); ++a) { + for(uint_fast64_t a = 0; a < this->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)) { + for(auto const& entry : this->mdp.getTransitionMatrix().getRow(this->mdp.getNondeterministicChoiceIndices()[s]+a)) { if(entry.getValue() != 0) { storage::StateActionTarget sat = {s,a,entry.getColumn()}; expr = expr + mBetaVariables[sat]; @@ -172,7 +174,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation } 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)) { + for(auto const& entry : this->mdp.getTransitionMatrix().getRow(this->mdp.getNondeterministicChoiceIndices()[s]+a)) { if(entry.getValue() != 0) { storage::StateActionTarget sat = {s,a,entry.getColumn()}; std::string satstring = to_string(sat); @@ -195,7 +197,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation * */ void createMILP(bool lowerBound, double boundary, PermissiveSchedulerPenalties const& penalties) { - storm::storage::BitVector irrelevant = mGoals | mSinks; + storm::storage::BitVector irrelevant = this->mGoals | this->mSinks; storm::storage::BitVector relevantStates = ~irrelevant; // Notice that the separated construction of variables and // constraints slows down the construction of the MILP. diff --git a/src/permissivesched/PermissiveSchedulerComputation.h b/src/permissivesched/PermissiveSchedulerComputation.h index dd6e28124..372b4a15d 100644 --- a/src/permissivesched/PermissiveSchedulerComputation.h +++ b/src/permissivesched/PermissiveSchedulerComputation.h @@ -10,16 +10,18 @@ namespace storm { namespace ps { + + template class PermissiveSchedulerComputation { protected: - std::shared_ptr> mdp; + storm::models::sparse::Mdp const& mdp; storm::storage::BitVector const& mGoals; storm::storage::BitVector const& mSinks; PermissiveSchedulerPenalties mPenalties; public: - PermissiveSchedulerComputation(std::shared_ptr> mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates) + PermissiveSchedulerComputation(storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates) : mdp(mdp), mGoals(goalstates), mSinks(sinkstates) { @@ -42,7 +44,7 @@ namespace storm { virtual bool foundSolution() const = 0; - virtual SubMDPPermissiveScheduler getScheduler() const = 0; + virtual SubMDPPermissiveScheduler getScheduler() const = 0; }; diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp index 8c8a0efef..fd3df457e 100644 --- a/src/permissivesched/PermissiveSchedulers.cpp +++ b/src/permissivesched/PermissiveSchedulers.cpp @@ -1,5 +1,7 @@ + #include "PermissiveSchedulers.h" -#include "../storage/BitVector.h" + +#include "src/models/sparse/StandardRewardModel.h" #include "../utility/solver.h" #include "../utility/graph.h" #include "../modelchecker/propositional/SparsePropositionalModelChecker.h" @@ -8,37 +10,39 @@ #include "src/exceptions/NotImplementedException.h" #include "src/utility/macros.h" - namespace storm { namespace ps { - - boost::optional computePermissiveSchedulerViaMILP(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { - storm::modelchecker::SparsePropositionalModelChecker> propMC(*mdp); + + template + boost::optional> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { + storm::modelchecker::SparsePropositionalModelChecker> propMC(mdp); assert(safeProp.getSubformula().isEventuallyFormula()); - auto backwardTransitions = mdp->getBackwardTransitions(); + auto backwardTransitions = mdp.getBackwardTransitions(); storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - goalstates = storm::utility::graph::performProb1A(*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); + goalstates = storm::utility::graph::performProb1A(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); + 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(comp.getScheduler()); + return boost::optional>(comp.getScheduler()); } else { - return boost::optional(); + return boost::optional>(); } } - - boost::optional computePermissiveSchedulerViaMC(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { + + template + boost::optional> computePermissiveSchedulerViaMC(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { } - - boost::optional computerPermissiveSchedulerViaSMT(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { - storm::modelchecker::SparsePropositionalModelChecker> propMC(*mdp); + + template + boost::optional> computerPermissiveSchedulerViaSMT(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { + storm::modelchecker::SparsePropositionalModelChecker> propMC(*mdp); assert(safeProp.getSubformula().isEventuallyFormula()); auto backwardTransitions = mdp->getBackwardTransitions(); storm::storage::BitVector goalstates = propMC.check(safeProp.getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); @@ -53,5 +57,8 @@ namespace storm { return boost::optional(); }*/ } + + template boost::optional> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp); + } } diff --git a/src/permissivesched/PermissiveSchedulers.h b/src/permissivesched/PermissiveSchedulers.h index 2ebcd07bf..4c5049401 100644 --- a/src/permissivesched/PermissiveSchedulers.h +++ b/src/permissivesched/PermissiveSchedulers.h @@ -4,28 +4,30 @@ #include "../logic/ProbabilityOperatorFormula.h" #include "../models/sparse/Mdp.h" +#include "../models/sparse/StandardRewardModel.h" -#include "src/models/sparse/StandardRewardModel.h" namespace storm { namespace ps { - + class PermissiveScheduler { public: virtual ~PermissiveScheduler() = default; }; - - class SubMDPPermissiveScheduler : public PermissiveScheduler { - storm::models::sparse::Mdp const& mdp; + + template> + class SubMDPPermissiveScheduler : public PermissiveScheduler { + storm::models::sparse::Mdp const &mdp; storm::storage::BitVector enabledChoices; public: virtual ~SubMDPPermissiveScheduler() = default; - SubMDPPermissiveScheduler(SubMDPPermissiveScheduler&&) = default; - SubMDPPermissiveScheduler(SubMDPPermissiveScheduler const&) = delete; - SubMDPPermissiveScheduler(storm::models::sparse::Mdp const& refmdp, bool allEnabled) : - PermissiveScheduler(), mdp(refmdp), enabledChoices(refmdp.getNumberOfChoices(), allEnabled) - { + SubMDPPermissiveScheduler(SubMDPPermissiveScheduler &&) = default; + + SubMDPPermissiveScheduler(SubMDPPermissiveScheduler const &) = delete; + + SubMDPPermissiveScheduler(storm::models::sparse::Mdp const &refmdp, bool allEnabled) : + PermissiveScheduler(), mdp(refmdp), enabledChoices(refmdp.getNumberOfChoices(), allEnabled) { // Intentionally left empty. } @@ -35,14 +37,15 @@ namespace storm { } - storm::models::sparse::Mdp apply() const { + storm::models::sparse::Mdp apply() const { return mdp.restrictChoices(enabledChoices); } - + }; - - boost::optional computePermissiveSchedulerViaMILP(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp); + + template> + boost::optional> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp const &mdp, storm::logic::ProbabilityOperatorFormula const &safeProp); } } diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index b156d3958..894d1df12 100644 --- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -30,14 +30,14 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options)->as>(); - boost::optional perms = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02); + boost::optional> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02); EXPECT_NE(perms, boost::none); - boost::optional perms2 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001); + boost::optional> perms2 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula001); EXPECT_EQ(perms2, boost::none); - boost::optional perms3 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02b); + boost::optional> perms3 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02b); EXPECT_EQ(perms3, boost::none); - boost::optional perms4 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001b); + boost::optional> perms4 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula001b); EXPECT_NE(perms4, boost::none); storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native)));