From 5ec1e2acbed1f5f16e9e48c2f505b742ae209964 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 10 Aug 2015 19:25:03 +0200 Subject: [PATCH 1/9] PermissiveSchedulers are on future now Former-commit-id: d49b7623e6a498bc5380208ddfbb87ca02d2c54f --- src/storage/PermissiveSchedulers.h | 232 +++++++++++++++++++++++++++++ 1 file changed, 232 insertions(+) create mode 100644 src/storage/PermissiveSchedulers.h diff --git a/src/storage/PermissiveSchedulers.h b/src/storage/PermissiveSchedulers.h new file mode 100644 index 000000000..a5d8b5574 --- /dev/null +++ b/src/storage/PermissiveSchedulers.h @@ -0,0 +1,232 @@ + +#ifndef PERMISSIVESCHEDULERS_H +#define PERMISSIVESCHEDULERS_H + +#include +#include "expressions/Variable.h" +#include "StateActionPair.h" +#include "StateActionTargetTuple.h" + +namespace storm { + namespace storage { + class PermissiveSchedulerPenalties { + std::unordered_map mPenalties; + + public: + double get(uint_fast64_t state, uint_fast64_t action) const { + return get(StateActionPair(state, action)); + + } + + + double get(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(); + } + + }; + + class MilpPermissiveSchedulerComputation { + private: + + bool mCalledOptimizer = false; + storm::solver::LpSolver& solver; + std::shared_ptr> mdp; + std::unordered_map multistrategyVariables; + std::unordered_map mProbVariables; + std::unordered_map mAlphaVariables; + std::unordered_map mBetaVariables; + std::unordered_map mGammaVariables; + BitVector const& mGoals; + BitVector const& mSinks; + + public: + + MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, std::shared_ptr> mdp, BitVector const& goalstates, BitVector const& sinkstates) + : solver(milpsolver), mdp(mdp), mGoals(goalstates), mSinks(sinkstates) + { + + } + + + void calculatePermissiveScheduler(double boundary, PermissiveSchedulerPenalties const& penalties, BitVector const& irrelevantStates = BitVector()) { + createMILP(boundary, penalties, irrelevantStates); + solver.optimize(); + mCalledOptimizer = true; + } + + bool foundSolution() { + assert(mCalledOptimizer); + return !solver.isInfeasible(); + } + + BitVector getAllowedStateActionPairs() const { + 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 result; + } + + + private: + + /** + * + */ + void createVariables(PermissiveSchedulerPenalties const& penalties, 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 = 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) { + 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; + // (2) + for(uint_fast64_t a = 0; a < mdp->getNumberOfChoices(s); ++a) { + expr = expr + multistrategyVariables[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 = storm::expressions::Expression(); + 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[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 = storm::expressions::Expression(); + for(auto const& entry : mdp->getTransitionMatrix().getRow(mdp->getNondeterministicChoiceIndices()[s]+a)) { + if(entry.getValue() != 0) { + StateActionTarget sat = {s,a,entry.getColumn()}; + expr = expr + mBetaVariables[sat]; + } + } + solver.addConstraint("c6-" + sastring, multistrategyVariables[StateActionPair(s,a)] == (solver.getConstant(1) - mAlphaVariables[s]) + expr); + + for(auto const& entry : mdp->getTransitionMatrix().getRow(mdp->getNondeterministicChoiceIndices()[s]+a)) { + if(entry.getValue() != 0) { + StateActionTarget sat = {s,a,entry.getColumn()}; + std::string satstring = to_string(sat); + // (8) + solver.addConstraint("c8-" + satstring, mGammaVariables[entry.getColumn()] < mGammaVariables[s] + (solver.getConstant(1) - mBetaVariables[sat])); // With rewards, we have to change this. + } + } + + } + } + } + + + /** + * + */ + void createMILP(double boundary, PermissiveSchedulerPenalties const& penalties, BitVector const& dontCareStates ) { + BitVector irrelevant = mGoals | mSinks; + 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 /* PERMISSIVESCHEDULERS_H */ + From 719ac4fb4e86782fe082519fa12025a13750d5af Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 10 Aug 2015 19:26:48 +0200 Subject: [PATCH 2/9] move perm sched to own dir Former-commit-id: 0bf95c9c33b32e35771efd65805fb7e38f2e6acf --- src/{storage => permissivesched}/PermissiveSchedulers.h | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/{storage => permissivesched}/PermissiveSchedulers.h (100%) diff --git a/src/storage/PermissiveSchedulers.h b/src/permissivesched/PermissiveSchedulers.h similarity index 100% rename from src/storage/PermissiveSchedulers.h rename to src/permissivesched/PermissiveSchedulers.h From 72784d752dc29f3341b62c1d0e4871664ff070d9 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 12 Aug 2015 12:54:33 +0200 Subject: [PATCH 3/9] permissive schedulers - ongoing work Former-commit-id: 0f637998c6738bd064941389309d1103afa03fbf --- CMakeLists.txt | 2 + .../MILPPermissiveSchedulers.h | 196 +++++++++++++++ .../PermissiveSchedulerComputation.h | 55 +++++ .../PermissiveSchedulerPenalty.h | 53 +++++ src/permissivesched/PermissiveSchedulers.cpp | 31 +++ src/permissivesched/PermissiveSchedulers.h | 224 +----------------- .../SmtBasedPermissiveSchedulers.h | 7 + test/functional/builder/die_selection.nm | 45 ++++ .../MilpPermissiveSchedulerTest.cpp | 31 +++ 9 files changed, 430 insertions(+), 214 deletions(-) create mode 100644 src/permissivesched/MILPPermissiveSchedulers.h create mode 100644 src/permissivesched/PermissiveSchedulerComputation.h create mode 100644 src/permissivesched/PermissiveSchedulerPenalty.h create mode 100644 src/permissivesched/PermissiveSchedulers.cpp create mode 100644 src/permissivesched/SmtBasedPermissiveSchedulers.h create mode 100644 test/functional/builder/die_selection.nm create mode 100644 test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 6bdaa29a2..1fc3d1d1a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -383,6 +383,7 @@ file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/sr file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp) file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp) +file(GLOB_RECURSE STORM_PERMISSIVESCHEDULER_FILES ${PROJECT_SOURCE_DIR}/src/permissivesched/*.h ${PROJECT_SOURCE_DIR}/src/permissivesched/*.cpp) file(GLOB STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp) file(GLOB_RECURSE STORM_MODELS_SPARSE_FILES ${PROJECT_SOURCE_DIR}/src/models/sparse/*.h ${PROJECT_SOURCE_DIR}/src/models/sparse/*.cpp) file(GLOB_RECURSE STORM_MODELS_SYMBOLIC_FILES ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.h ${PROJECT_SOURCE_DIR}/src/models/symbolic/*.cpp) @@ -421,6 +422,7 @@ source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_ source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES}) source_group(modelchecker\\results FILES ${STORM_MODELCHECKER_RESULTS_FILES}) source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES}) +source_group(permissiveschedulers FILES ${STORM_PERMISSIVESCHEDULER_FILES}) source_group(models FILES ${STORM_MODELS_FILES}) source_group(models\\sparse FILES ${STORM_MODELS_SPARSE_FILES}) source_group(models\\symbolic FILES ${STORM_MODELS_SYMBOLIC_FILES}) diff --git a/src/permissivesched/MILPPermissiveSchedulers.h b/src/permissivesched/MILPPermissiveSchedulers.h new file mode 100644 index 000000000..abfbf2274 --- /dev/null +++ b/src/permissivesched/MILPPermissiveSchedulers.h @@ -0,0 +1,196 @@ +#ifndef MILPPERMISSIVESCHEDULERS_H +#define MILPPERMISSIVESCHEDULERS_H + + +#include +#include + +#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 multistrategyVariables; + std::unordered_map mProbVariables; + std::unordered_map mAlphaVariables; + std::unordered_map mBetaVariables; + std::unordered_map mGammaVariables; + + 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) + { + + } + + + 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(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 */ + diff --git a/src/permissivesched/PermissiveSchedulerComputation.h b/src/permissivesched/PermissiveSchedulerComputation.h new file mode 100644 index 000000000..5582ffc36 --- /dev/null +++ b/src/permissivesched/PermissiveSchedulerComputation.h @@ -0,0 +1,55 @@ +#ifndef PERMISSIVESCHEDULERCOMPUTATION_H +#define PERMISSIVESCHEDULERCOMPUTATION_H + +#include + +#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> 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) + : 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 */ + diff --git a/src/permissivesched/PermissiveSchedulerPenalty.h b/src/permissivesched/PermissiveSchedulerPenalty.h new file mode 100644 index 000000000..bb680defa --- /dev/null +++ b/src/permissivesched/PermissiveSchedulerPenalty.h @@ -0,0 +1,53 @@ +#ifndef PERMISSIVESCHEDULERPENALTY_H +#define PERMISSIVESCHEDULERPENALTY_H + +#include + +#include "../storage/StateActionPair.h" + +namespace storm { + namespace ps { + + class PermissiveSchedulerPenalties { + + std::unordered_map 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 */ + diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp new file mode 100644 index 000000000..89665859e --- /dev/null +++ b/src/permissivesched/PermissiveSchedulers.cpp @@ -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 computePermissiveSchedulerViaMILP(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(); + 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(comp.getScheduler()); + } else { + return boost::optional(comp.getScheduler()); + } + } + } +} diff --git a/src/permissivesched/PermissiveSchedulers.h b/src/permissivesched/PermissiveSchedulers.h index a5d8b5574..d9bbd4e74 100644 --- a/src/permissivesched/PermissiveSchedulers.h +++ b/src/permissivesched/PermissiveSchedulers.h @@ -2,228 +2,24 @@ #ifndef PERMISSIVESCHEDULERS_H #define PERMISSIVESCHEDULERS_H -#include -#include "expressions/Variable.h" -#include "StateActionPair.h" -#include "StateActionTargetTuple.h" +#include "../logic/ProbabilityOperatorFormula.h" +#include "../models/sparse/Mdp.h" + namespace storm { - namespace storage { - class PermissiveSchedulerPenalties { - std::unordered_map mPenalties; - - public: - double get(uint_fast64_t state, uint_fast64_t action) const { - return get(StateActionPair(state, action)); - - } - - - double get(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(); - } + namespace ps { + + class PermissiveScheduler { }; - class MilpPermissiveSchedulerComputation { - private: - - bool mCalledOptimizer = false; - storm::solver::LpSolver& solver; - std::shared_ptr> mdp; - std::unordered_map multistrategyVariables; - std::unordered_map mProbVariables; - std::unordered_map mAlphaVariables; - std::unordered_map mBetaVariables; - std::unordered_map mGammaVariables; - BitVector const& mGoals; - BitVector const& mSinks; - + class MemorylessDeterministicPermissiveScheduler : public PermissiveScheduler { + storm::storage::BitVector memdetschedulers; public: - - MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, std::shared_ptr> mdp, BitVector const& goalstates, BitVector const& sinkstates) - : solver(milpsolver), mdp(mdp), mGoals(goalstates), mSinks(sinkstates) - { - - } - - - void calculatePermissiveScheduler(double boundary, PermissiveSchedulerPenalties const& penalties, BitVector const& irrelevantStates = BitVector()) { - createMILP(boundary, penalties, irrelevantStates); - solver.optimize(); - mCalledOptimizer = true; - } - - bool foundSolution() { - assert(mCalledOptimizer); - return !solver.isInfeasible(); - } - - BitVector getAllowedStateActionPairs() const { - 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 result; - } - - - private: - - /** - * - */ - void createVariables(PermissiveSchedulerPenalties const& penalties, 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 = 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) { - 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; - // (2) - for(uint_fast64_t a = 0; a < mdp->getNumberOfChoices(s); ++a) { - expr = expr + multistrategyVariables[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 = storm::expressions::Expression(); - 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[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 = storm::expressions::Expression(); - for(auto const& entry : mdp->getTransitionMatrix().getRow(mdp->getNondeterministicChoiceIndices()[s]+a)) { - if(entry.getValue() != 0) { - StateActionTarget sat = {s,a,entry.getColumn()}; - expr = expr + mBetaVariables[sat]; - } - } - solver.addConstraint("c6-" + sastring, multistrategyVariables[StateActionPair(s,a)] == (solver.getConstant(1) - mAlphaVariables[s]) + expr); - - for(auto const& entry : mdp->getTransitionMatrix().getRow(mdp->getNondeterministicChoiceIndices()[s]+a)) { - if(entry.getValue() != 0) { - StateActionTarget sat = {s,a,entry.getColumn()}; - std::string satstring = to_string(sat); - // (8) - solver.addConstraint("c8-" + satstring, mGammaVariables[entry.getColumn()] < mGammaVariables[s] + (solver.getConstant(1) - mBetaVariables[sat])); // With rewards, we have to change this. - } - } - - } - } - } - - - /** - * - */ - void createMILP(double boundary, PermissiveSchedulerPenalties const& penalties, BitVector const& dontCareStates ) { - BitVector irrelevant = mGoals | mSinks; - 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); - - - } - - - - - + MemorylessDeterministicPermissiveScheduler(storm::storage::BitVector const& allowedPairs) : memdetschedulers(allowedPairs) {} }; + boost::optional computePermissiveSchedulerViaMILP(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp); } } diff --git a/src/permissivesched/SmtBasedPermissiveSchedulers.h b/src/permissivesched/SmtBasedPermissiveSchedulers.h new file mode 100644 index 000000000..9af6882ad --- /dev/null +++ b/src/permissivesched/SmtBasedPermissiveSchedulers.h @@ -0,0 +1,7 @@ +#ifndef SMTBASEDPERMISSIVESCHEDULERS_H +#define SMTBASEDPERMISSIVESCHEDULERS_H + + + +#endif /* SMTBASEDPERMISSIVESCHEDULERS_H */ + diff --git a/test/functional/builder/die_selection.nm b/test/functional/builder/die_selection.nm new file mode 100644 index 000000000..819472268 --- /dev/null +++ b/test/functional/builder/die_selection.nm @@ -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; diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp new file mode 100644 index 000000000..a66a6f693 --- /dev/null +++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -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::Options options; + + options = typename storm::builder::ExplicitPrismModelBuilder::Options(formula); + options.addConstantDefinitionsFromString(program, ""); + options.buildRewards = false; + options.buildCommandLabels = true; + + std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options)->as>(); + + storm::ps::computePermissiveSchedulerViaMILP(mdp, formula); + + // + +} From 7d9cc8e90526eab60cd75187ab4f85d6e9ab4004 Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 21 Aug 2015 16:59:56 +0200 Subject: [PATCH 4/9] Minimal progress on perm schedulers Former-commit-id: 9ea6756c6af7fb5c8a4758ac4bdfaae11173309f --- src/permissivesched/MCPermissiveSchedulers.h | 0 src/permissivesched/MILPPermissiveSchedulers.h | 4 +++- src/permissivesched/PermissiveSchedulers.cpp | 4 ++++ 3 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 src/permissivesched/MCPermissiveSchedulers.h diff --git a/src/permissivesched/MCPermissiveSchedulers.h b/src/permissivesched/MCPermissiveSchedulers.h new file mode 100644 index 000000000..e69de29bb diff --git a/src/permissivesched/MILPPermissiveSchedulers.h b/src/permissivesched/MILPPermissiveSchedulers.h index abfbf2274..7f0e7c5b9 100644 --- a/src/permissivesched/MILPPermissiveSchedulers.h +++ b/src/permissivesched/MILPPermissiveSchedulers.h @@ -163,7 +163,9 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation 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. + if(relevantStates[entry.getColumn()]) { + solver.addConstraint("c8-" + satstring, mGammaVariables[entry.getColumn()] < mGammaVariables[s] + (solver.getConstant(1) - mBetaVariables[sat]) + mProbVariables[s]); // With rewards, we have to change this. + } } } diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp index 89665859e..231d4ba14 100644 --- a/src/permissivesched/PermissiveSchedulers.cpp +++ b/src/permissivesched/PermissiveSchedulers.cpp @@ -27,5 +27,9 @@ namespace storm { return boost::optional(comp.getScheduler()); } } + + boost::optional computePermissiveSchedulerViaMC(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { + + } } } From 6d10ba0ad0939fcea9627b8b786f86d24d1cbeab Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 1 Sep 2015 18:22:16 +0200 Subject: [PATCH 5/9] compiles again Former-commit-id: 1c09323cd1c3c7a14582f2446f48ff2afd0be2fc --- .../prctl/helper/MDPModelCheckingHelperReturnType.h | 2 +- src/permissivesched/MILPPermissiveSchedulers.h | 2 +- src/permissivesched/PermissiveSchedulers.cpp | 6 +++++- .../permissiveschedulers/MilpPermissiveSchedulerTest.cpp | 3 +-- 4 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h index d04dd1988..a68a5889e 100644 --- a/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h +++ b/src/modelchecker/prctl/helper/MDPModelCheckingHelperReturnType.h @@ -3,7 +3,7 @@ #include #include -#include "src/storage/partialscheduler.h" +#include "src/storage/PartialScheduler.h" namespace storm { namespace storage { diff --git a/src/permissivesched/MILPPermissiveSchedulers.h b/src/permissivesched/MILPPermissiveSchedulers.h index 7f0e7c5b9..d25179225 100644 --- a/src/permissivesched/MILPPermissiveSchedulers.h +++ b/src/permissivesched/MILPPermissiveSchedulers.h @@ -187,7 +187,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation createConstraints(boundary, relevantStates); - solver.setModelSense(storm::solver::LpSolver::ModelSense::Minimize); + solver.setOptimizationDirection(storm::OptimizationDirection::Minimize); } }; diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp index 231d4ba14..53f1039a8 100644 --- a/src/permissivesched/PermissiveSchedulers.cpp +++ b/src/permissivesched/PermissiveSchedulers.cpp @@ -11,7 +11,7 @@ namespace storm { namespace ps { boost::optional computePermissiveSchedulerViaMILP(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { - storm::modelchecker::SparsePropositionalModelChecker propMC(*mdp); + 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(); @@ -31,5 +31,9 @@ namespace storm { boost::optional computePermissiveSchedulerViaMC(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { } + + boost::optional computerPermissiveSchedulerViaSMT(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { + + } } } diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index a66a6f693..ad300df32 100644 --- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -11,7 +11,7 @@ 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(); + auto formula = formulaParser.parseSingleFormulaFromString("P<=0.2 [ F \"one\"]")->asProbabilityOperatorFormula(); std::cout << formula << std::endl; // Customize and perform model-building. @@ -19,7 +19,6 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { options = typename storm::builder::ExplicitPrismModelBuilder::Options(formula); options.addConstantDefinitionsFromString(program, ""); - options.buildRewards = false; options.buildCommandLabels = true; std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options)->as>(); From 9254e6650cf6f123e31e557c9dbdaaad11e3b3b5 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Sep 2015 10:50:01 +0200 Subject: [PATCH 6/9] Option to force color output for clang/ninja. Former-commit-id: 89e960b383ed3652437311f0873b327322f85d78 --- CMakeLists.txt | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 95a280584..a06b0ce18 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -28,6 +28,7 @@ option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precom option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) option(USE_CARL "Sets whether carl should be included." ON) +option(FORCE_COLOR "Force color output" ON) set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") set(CUDA_ROOT "" CACHE STRING "The root directory of CUDA.") @@ -171,6 +172,10 @@ else(CLANG) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-newline-eof -Wno-mismatched-tags -ftemplate-depth=1024") set (CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic") + if(FORCE_COLOR) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics") + endif() + # Turn on popcnt instruction if desired (yes by default) if (STORM_USE_POPCNT) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt") From f65efdb4bbb0a936984e97689c823d16d57bbda0 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Sep 2015 16:31:32 +0200 Subject: [PATCH 7/9] disable smtrat for now Former-commit-id: 4f63d4cd05227b993884a5df1ad0af8603ff5e56 --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a06b0ce18..274cb0350 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -98,7 +98,7 @@ if(USE_CARL) set(STORM_HAVE_CARL ON) endif() - find_package(smtrat QUIET) + #find_package(smtrat QUIET) if(smtrat_FOUND) set(STORM_HAVE_SMTRAT ON) endif() From 2213b01ece625dba5628182bf4a81987d98d7b88 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 2 Sep 2015 19:11:26 +0200 Subject: [PATCH 8/9] changes in milp permissive scheduler Former-commit-id: 6b11d01b88ab89cf91c78e110c15bd2dbf5db874 --- .../MILPPermissiveSchedulers.h | 49 ++++++++++++------- .../PermissiveSchedulerComputation.h | 4 +- src/permissivesched/PermissiveSchedulers.cpp | 12 +++-- src/permissivesched/PermissiveSchedulers.h | 11 ++++- .../MilpPermissiveSchedulerTest.cpp | 27 +++++++--- 5 files changed, 72 insertions(+), 31 deletions(-) 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); // } From dbe997a43307f707774994521fb50a17219f4e03 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 3 Sep 2015 14:30:51 +0200 Subject: [PATCH 9/9] resolved linker error - sorry Former-commit-id: 6fcb8fa24567cb5dba4510a0d96dd67494a1aae9 --- src/models/sparse/Ctmc.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp index 9f4ddfcd6..371d48270 100644 --- a/src/models/sparse/Ctmc.cpp +++ b/src/models/sparse/Ctmc.cpp @@ -40,9 +40,9 @@ namespace storm { template class Ctmc; -//#ifdef STORM_HAVE_CARL -// template class Ctmc; -//#endif +#ifdef STORM_HAVE_CARL + template class Ctmc; +#endif } // namespace sparse } // namespace models