sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

updates to perm schedulers 

Former-commit-id: b3404cac21
tempestpy_adaptions
sjunges 9 years ago
parent
98162d1d7e
commit
e4aab761d2
5 changed files with 73 additions and 59 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 44
      src/permissivesched/MILPPermissiveSchedulers.h
  2. 8
      src/permissivesched/PermissiveSchedulerComputation.h
  3. 33
      src/permissivesched/PermissiveSchedulers.cpp
  4. 17
      src/permissivesched/PermissiveSchedulers.h
  5. 8
      test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp

44
src/permissivesched/MILPPermissiveSchedulers.h
View File

@ -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<typename RM>
class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation<RM> {
private:
bool mCalledOptimizer = false;
@ -31,15 +33,15 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation
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)
MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, storm::models::sparse::Mdp<double, RM> const& mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates)
: PermissiveSchedulerComputation<RM>(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<RM> getScheduler() const override {
assert(mCalledOptimizer);
assert(foundSolution());
SubMDPPermissiveScheduler result(*mdp, true);
SubMDPPermissiveScheduler<RM> 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.

8
src/permissivesched/PermissiveSchedulerComputation.h
View File

@ -10,16 +10,18 @@
namespace storm {
namespace ps {
template<typename RM>
class PermissiveSchedulerComputation {
protected:
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
storm::models::sparse::Mdp<double, RM> const& 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)
PermissiveSchedulerComputation(storm::models::sparse::Mdp<double, RM> 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<RM> getScheduler() const = 0;
};

33
src/permissivesched/PermissiveSchedulers.cpp
View File

@ -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<SubMDPPermissiveScheduler> 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);
template<typename RM>
boost::optional<SubMDPPermissiveScheduler<RM>> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp<double, RM> const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<double, RM>> 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<storm::models::sparse::StandardRewardModel<double>> 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<SubMDPPermissiveScheduler>(comp.getScheduler());
return boost::optional<SubMDPPermissiveScheduler<RM>>(comp.getScheduler());
} else {
return boost::optional<SubMDPPermissiveScheduler>();
return boost::optional<SubMDPPermissiveScheduler<RM>>();
}
}
boost::optional<SubMDPPermissiveScheduler> computePermissiveSchedulerViaMC(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
template<typename RM>
boost::optional<SubMDPPermissiveScheduler<RM>> computePermissiveSchedulerViaMC(std::shared_ptr<storm::models::sparse::Mdp<double, RM>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
}
boost::optional<SubMDPPermissiveScheduler> computerPermissiveSchedulerViaSMT(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<double>> propMC(*mdp);
template<typename RM>
boost::optional<SubMDPPermissiveScheduler<RM>> computerPermissiveSchedulerViaSMT(std::shared_ptr<storm::models::sparse::Mdp<double, RM>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<double, RM>> 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<SubMDPPermissiveScheduler>();
}*/
}
template boost::optional<SubMDPPermissiveScheduler<>> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp<double> const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp);
}
}

17
src/permissivesched/PermissiveSchedulers.h
View File

@ -4,8 +4,8 @@
#include "../logic/ProbabilityOperatorFormula.h"
#include "../models/sparse/Mdp.h"
#include "../models/sparse/StandardRewardModel.h"
#include "src/models/sparse/StandardRewardModel.h"
namespace storm {
namespace ps {
@ -15,17 +15,19 @@ namespace storm {
virtual ~PermissiveScheduler() = default;
};
template<typename RM= storm::models::sparse::StandardRewardModel<double>>
class SubMDPPermissiveScheduler : public PermissiveScheduler {
storm::models::sparse::Mdp<double> const& mdp;
storm::models::sparse::Mdp<double, RM> const &mdp;
storm::storage::BitVector enabledChoices;
public:
virtual ~SubMDPPermissiveScheduler() = default;
SubMDPPermissiveScheduler(SubMDPPermissiveScheduler &&) = default;
SubMDPPermissiveScheduler(SubMDPPermissiveScheduler const &) = delete;
SubMDPPermissiveScheduler(storm::models::sparse::Mdp<double> const& refmdp, bool allEnabled) :
PermissiveScheduler(), mdp(refmdp), enabledChoices(refmdp.getNumberOfChoices(), allEnabled)
{
SubMDPPermissiveScheduler(storm::models::sparse::Mdp<double, RM> const &refmdp, bool allEnabled) :
PermissiveScheduler(), mdp(refmdp), enabledChoices(refmdp.getNumberOfChoices(), allEnabled) {
// Intentionally left empty.
}
@ -35,14 +37,15 @@ namespace storm {
}
storm::models::sparse::Mdp<double> apply() const {
storm::models::sparse::Mdp<double, RM> apply() const {
return mdp.restrictChoices(enabledChoices);
}
};
boost::optional<SubMDPPermissiveScheduler> computePermissiveSchedulerViaMILP(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp);
template<typename RM = storm::models::sparse::StandardRewardModel<double>>
boost::optional<SubMDPPermissiveScheduler<RM>> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp<double, RM> const &mdp, storm::logic::ProbabilityOperatorFormula const &safeProp);
}
}

8
test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
View File

@ -30,14 +30,14 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) {
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::SubMDPPermissiveScheduler> perms = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02);
boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02);
EXPECT_NE(perms, boost::none);
boost::optional<storm::ps::SubMDPPermissiveScheduler> perms2 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001);
boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms2 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula001);
EXPECT_EQ(perms2, boost::none);
boost::optional<storm::ps::SubMDPPermissiveScheduler> perms3 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02b);
boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms3 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02b);
EXPECT_EQ(perms3, boost::none);
boost::optional<storm::ps::SubMDPPermissiveScheduler> perms4 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001b);
boost::optional<storm::ps::SubMDPPermissiveScheduler<>> perms4 = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula001b);
EXPECT_NE(perms4, boost::none);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker0(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));

Write Preview
Loading…
Cancel
Save