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 <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 */
+
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 <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 */
+
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 <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 */
+
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<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());
+ }
+ }
+ }
+}
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 <unordered_map>
-#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<StateActionPair, double> 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<storm::models::sparse::Mdp<double>> mdp;
- std::unordered_map<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<StateActionTarget, storm::expressions::Variable> mBetaVariables;
- std::unordered_map<uint_fast64_t, storm::expressions::Variable> mGammaVariables;
- BitVector const& mGoals;
- BitVector const& mSinks;
-
+ class MemorylessDeterministicPermissiveScheduler : public PermissiveScheduler {
+ storm::storage::BitVector memdetschedulers;
public:
-
- MilpPermissiveSchedulerComputation(storm::solver::LpSolver& milpsolver, std::shared_ptr<storm::models::sparse::Mdp<double>> 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<MemorylessDeterministicPermissiveScheduler> computePermissiveSchedulerViaMILP(std::shared_ptr<storm::models::sparse::Mdp<double>> 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<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);
+
+ //
+
+}