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

removed perm schedulers from gspn to circumvent error msg for now 

Former-commit-id: 7d10ec8367
tempestpy_adaptions
sjunges 9 years ago
parent
5db1678528
commit
cb913658cc
8 changed files with 0 additions and 513 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. 0
      src/permissivesched/MCPermissiveSchedulers.h
  2. 218
      src/permissivesched/MILPPermissiveSchedulers.h
  3. 57
      src/permissivesched/PermissiveSchedulerComputation.h
  4. 53
      src/permissivesched/PermissiveSchedulerPenalty.h
  5. 64
      src/permissivesched/PermissiveSchedulers.cpp
  6. 54
      src/permissivesched/PermissiveSchedulers.h
  7. 7
      src/permissivesched/SmtBasedPermissiveSchedulers.h
  8. 60
      test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp

0
src/permissivesched/MCPermissiveSchedulers.h
View File

218
src/permissivesched/MILPPermissiveSchedulers.h
View File

@ -1,218 +0,0 @@
#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"
#include "PermissiveSchedulers.h"
namespace storm {
namespace ps {
template<typename RM>
class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation<RM> {
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, 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, this->mPenalties);
//STORM_LOG_DEBUG("Calling optimizer");
solver.optimize();
//STORM_LOG_DEBUG("Done optimizing.")
mCalledOptimizer = true;
}
bool foundSolution() const override {
assert(mCalledOptimizer);
return !solver.isInfeasible();
}
SubMDPPermissiveScheduler<RM> getScheduler() const override {
assert(mCalledOptimizer);
assert(foundSolution());
SubMDPPermissiveScheduler<RM> result(this->mdp, true);
for(auto const& entry : multistrategyVariables) {
if(!solver.getBinaryValue(entry.second)) {
result.disable(this->mdp.getChoiceIndex(entry.first));
}
}
return result;
}
void dumpLpToFile(std::string const& filename) {
solver.writeModelToFile(filename);
}
private:
/**
* Create variables
*/
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(this->mdp.getInitialStates().getNumberOfSetBits() == 1);
uint_fast64_t initialStateIndex = this->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 < this->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 : 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));
mBetaVariables[sat] = var;
}
}
}
}
solver.update();
}
/**
* Create constraints
*/
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(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));
} 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 < this->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 < this->mdp.getNumberOfChoices(s); ++a) {
std::string sastring(stateString + "_" + std::to_string(a));
expr = solver.getConstant(0.0);
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 && this->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 < this->mdp.getNumberOfChoices(s); ++a) {
// (6)
std::string sastring(stateString + "_" + std::to_string(a));
expr = solver.getConstant(0.0);
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];
}
}
solver.addConstraint("c6-" + sastring, multistrategyVariables[storage::StateActionPair(s,a)] == (solver.getConstant(1) - mAlphaVariables[s]) + expr);
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);
// (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 = 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.
// In the future, we might want to merge this.
createVariables(penalties, relevantStates);
createConstraints(lowerBound, boundary, relevantStates);
solver.setOptimizationDirection(storm::OptimizationDirection::Minimize);
}
};
}
}
#endif /* MILPPERMISSIVESCHEDULERS_H */

57
src/permissivesched/PermissiveSchedulerComputation.h
View File

@ -1,57 +0,0 @@
#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 {
template<typename RM>
class PermissiveSchedulerComputation {
protected:
storm::models::sparse::Mdp<double, RM> const& mdp;
storm::storage::BitVector const& mGoals;
storm::storage::BitVector const& mSinks;
PermissiveSchedulerPenalties mPenalties;
public:
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)
{
}
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 SubMDPPermissiveScheduler<RM> getScheduler() const = 0;
};
}
}
#endif /* PERMISSIVESCHEDULERCOMPUTATION_H */

53
src/permissivesched/PermissiveSchedulerPenalty.h
View File

@ -1,53 +0,0 @@
#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 0.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 */

64
src/permissivesched/PermissiveSchedulers.cpp
View File

@ -1,64 +0,0 @@
#include "PermissiveSchedulers.h"
#include "src/models/sparse/StandardRewardModel.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 {
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();
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);
auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi);
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<RM>>(comp.getScheduler());
} else {
return boost::optional<SubMDPPermissiveScheduler<RM>>();
}
}
template<typename RM>
boost::optional<SubMDPPermissiveScheduler<RM>> computePermissiveSchedulerViaMC(std::shared_ptr<storm::models::sparse::Mdp<double, RM>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
}
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();
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);
/*SmtPermissiveSchedulerComputation comp(mdp, goalstates, sinkstates)
if(comp.foundSolution()) {
return boost::optional<SubMDPPermissiveScheduler>(comp.getScheduler());
} else {
return boost::optional<SubMDPPermissiveScheduler>();
}*/
}
template boost::optional<SubMDPPermissiveScheduler<>> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp<double> const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp);
}
}

54
src/permissivesched/PermissiveSchedulers.h
View File

@ -1,54 +0,0 @@
#ifndef PERMISSIVESCHEDULERS_H
#define PERMISSIVESCHEDULERS_H
#include "../logic/ProbabilityOperatorFormula.h"
#include "../models/sparse/Mdp.h"
#include "../models/sparse/StandardRewardModel.h"
namespace storm {
namespace ps {
class PermissiveScheduler {
public:
virtual ~PermissiveScheduler() = default;
};
template<typename RM= storm::models::sparse::StandardRewardModel<double>>
class SubMDPPermissiveScheduler : public PermissiveScheduler {
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, RM> const &refmdp, bool allEnabled) :
PermissiveScheduler(), mdp(refmdp), enabledChoices(refmdp.getNumberOfChoices(), allEnabled) {
// Intentionally left empty.
}
void disable(uint_fast64_t choiceIndex) {
assert(choiceIndex < enabledChoices.size());
enabledChoices.set(choiceIndex, false);
}
storm::models::sparse::Mdp<double, RM> apply() const {
return mdp.restrictChoices(enabledChoices);
}
};
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);
}
}
#endif /* PERMISSIVESCHEDULERS_H */

7
src/permissivesched/SmtBasedPermissiveSchedulers.h
View File

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

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

@ -1,60 +0,0 @@
#include <src/modelchecker/results/ExplicitQualitativeCheckResult.h>
#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"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.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::SubMDPPermissiveScheduler<>> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02);
EXPECT_NE(perms, boost::none);
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);
EXPECT_EQ(perms3, boost::none);
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)));
std::unique_ptr<storm::modelchecker::CheckResult> result0 = checker0.check(formula02);
storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult();
ASSERT_FALSE(qualitativeResult0[0]);
auto submdp = perms->apply();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker1(submdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
std::unique_ptr<storm::modelchecker::CheckResult> result1 = checker1.check(formula02);
storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult();
EXPECT_TRUE(qualitativeResult1[0]);
//
}
Write Preview
Loading…
Cancel
Save