sjunges
10 years ago
9 changed files with 430 additions and 214 deletions
-
2CMakeLists.txt
-
196src/permissivesched/MILPPermissiveSchedulers.h
-
55src/permissivesched/PermissiveSchedulerComputation.h
-
53src/permissivesched/PermissiveSchedulerPenalty.h
-
31src/permissivesched/PermissiveSchedulers.cpp
-
222src/permissivesched/PermissiveSchedulers.h
-
7src/permissivesched/SmtBasedPermissiveSchedulers.h
-
45test/functional/builder/die_selection.nm
-
31test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp
@ -0,0 +1,196 @@ |
|||||
|
#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" |
||||
|
|
||||
|
|
||||
|
|
||||
|
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(double boundary) override { |
||||
|
createMILP(boundary, mPenalties); |
||||
|
solver.optimize(); |
||||
|
mCalledOptimizer = true; |
||||
|
} |
||||
|
|
||||
|
|
||||
|
bool foundSolution() const override { |
||||
|
assert(mCalledOptimizer); |
||||
|
return !solver.isInfeasible(); |
||||
|
} |
||||
|
|
||||
|
MemorylessDeterministicPermissiveScheduler && getScheduler() const override { |
||||
|
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); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
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; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
|
||||
|
|
||||
|
void createConstraints(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)); |
||||
|
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()); |
||||
|
} |
||||
|
} |
||||
|
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) |
||||
|
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(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); |
||||
|
|
||||
|
|
||||
|
solver.setModelSense(storm::solver::LpSolver::ModelSense::Minimize); |
||||
|
|
||||
|
} |
||||
|
}; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
#endif /* MILPPERMISSIVESCHEDULERS_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(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 */ |
||||
|
|
||||
@ -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 */ |
||||
|
|
||||
@ -0,0 +1,31 @@ |
|||||
|
#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"
|
||||
|
|
||||
|
|
||||
|
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<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"); |
||||
|
MilpPermissiveSchedulerComputation comp(*solver, mdp, goalstates, sinkstates); |
||||
|
comp.calculatePermissiveScheduler(safeProp.getBound()); |
||||
|
if(comp.foundSolution()) { |
||||
|
return boost::optional<MemorylessDeterministicPermissiveScheduler>(comp.getScheduler()); |
||||
|
} else { |
||||
|
return boost::optional<MemorylessDeterministicPermissiveScheduler>(comp.getScheduler()); |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,7 @@ |
|||||
|
#ifndef SMTBASEDPERMISSIVESCHEDULERS_H |
||||
|
#define SMTBASEDPERMISSIVESCHEDULERS_H |
||||
|
|
||||
|
|
||||
|
|
||||
|
#endif /* SMTBASEDPERMISSIVESCHEDULERS_H */ |
||||
|
|
||||
@ -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; |
||||
@ -0,0 +1,31 @@ |
|||||
|
#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"
|
||||
|
|
||||
|
|
||||
|
TEST(MilpPermissiveSchedulerTest, DieSelection) { |
||||
|
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die_selection.nm"); |
||||
|
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); |
||||
|
std::cout << " We are now here " << std::endl; |
||||
|
auto formula = formulaParser.parseFromString("P<=0.2 [ F \"one\"]")->asProbabilityOperatorFormula(); |
||||
|
std::cout << formula << std::endl; |
||||
|
|
||||
|
// Customize and perform model-building.
|
||||
|
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options; |
||||
|
|
||||
|
options = typename storm::builder::ExplicitPrismModelBuilder<double>::Options(formula); |
||||
|
options.addConstantDefinitionsFromString(program, ""); |
||||
|
options.buildRewards = false; |
||||
|
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); |
||||
|
|
||||
|
//
|
||||
|
|
||||
|
} |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue