diff --git a/src/permissivesched/MCPermissiveSchedulers.h b/src/permissivesched/MCPermissiveSchedulers.h deleted file mode 100644 index e69de29bb..000000000 diff --git a/src/permissivesched/MILPPermissiveSchedulers.h b/src/permissivesched/MILPPermissiveSchedulers.h deleted file mode 100644 index 9c2549127..000000000 --- a/src/permissivesched/MILPPermissiveSchedulers.h +++ /dev/null @@ -1,218 +0,0 @@ -#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" -#include "../models/sparse/StandardRewardModel.h" -#include "PermissiveSchedulers.h" - - -namespace storm { - namespace ps { - - template -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, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& goalstates, storm::storage::BitVector const& sinkstates) - : PermissiveSchedulerComputation(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 getScheduler() const override { - assert(mCalledOptimizer); - assert(foundSolution()); - SubMDPPermissiveScheduler 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 */ - diff --git a/src/permissivesched/PermissiveSchedulerComputation.h b/src/permissivesched/PermissiveSchedulerComputation.h deleted file mode 100644 index 372b4a15d..000000000 --- a/src/permissivesched/PermissiveSchedulerComputation.h +++ /dev/null @@ -1,57 +0,0 @@ -#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 { - - template - class PermissiveSchedulerComputation { - protected: - storm::models::sparse::Mdp const& mdp; - storm::storage::BitVector const& mGoals; - storm::storage::BitVector const& mSinks; - PermissiveSchedulerPenalties mPenalties; - - public: - - PermissiveSchedulerComputation(storm::models::sparse::Mdp 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 getScheduler() const = 0; - - - }; - - } -} - - -#endif /* PERMISSIVESCHEDULERCOMPUTATION_H */ - diff --git a/src/permissivesched/PermissiveSchedulerPenalty.h b/src/permissivesched/PermissiveSchedulerPenalty.h deleted file mode 100644 index 66f75cea2..000000000 --- a/src/permissivesched/PermissiveSchedulerPenalty.h +++ /dev/null @@ -1,53 +0,0 @@ -#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 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 */ - diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp deleted file mode 100644 index fd3df457e..000000000 --- a/src/permissivesched/PermissiveSchedulers.cpp +++ /dev/null @@ -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 - boost::optional> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp const& 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::performProb1A(mdp, backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); - storm::storage::BitVector sinkstates = storm::utility::graph::performProb0A(mdp,backwardTransitions, storm::storage::BitVector(goalstates.size(), true), goalstates); - - auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi); - MilpPermissiveSchedulerComputation> comp(*solver, mdp, goalstates, sinkstates); - 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>(); - } - } - - template - boost::optional> computePermissiveSchedulerViaMC(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { - - } - - template - boost::optional> computerPermissiveSchedulerViaSMT(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::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(comp.getScheduler()); - } else { - return boost::optional(); - }*/ - } - - template boost::optional> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp const& mdp, storm::logic::ProbabilityOperatorFormula const& safeProp); - - } -} diff --git a/src/permissivesched/PermissiveSchedulers.h b/src/permissivesched/PermissiveSchedulers.h deleted file mode 100644 index 4c5049401..000000000 --- a/src/permissivesched/PermissiveSchedulers.h +++ /dev/null @@ -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> - class SubMDPPermissiveScheduler : public PermissiveScheduler { - storm::models::sparse::Mdp const &mdp; - storm::storage::BitVector enabledChoices; - public: - virtual ~SubMDPPermissiveScheduler() = default; - - SubMDPPermissiveScheduler(SubMDPPermissiveScheduler &&) = default; - - SubMDPPermissiveScheduler(SubMDPPermissiveScheduler const &) = delete; - - SubMDPPermissiveScheduler(storm::models::sparse::Mdp 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 apply() const { - return mdp.restrictChoices(enabledChoices); - } - - - }; - - template> - boost::optional> computePermissiveSchedulerViaMILP(storm::models::sparse::Mdp const &mdp, storm::logic::ProbabilityOperatorFormula const &safeProp); - } -} - - -#endif /* PERMISSIVESCHEDULERS_H */ - diff --git a/src/permissivesched/SmtBasedPermissiveSchedulers.h b/src/permissivesched/SmtBasedPermissiveSchedulers.h deleted file mode 100644 index 9af6882ad..000000000 --- a/src/permissivesched/SmtBasedPermissiveSchedulers.h +++ /dev/null @@ -1,7 +0,0 @@ -#ifndef SMTBASEDPERMISSIVESCHEDULERS_H -#define SMTBASEDPERMISSIVESCHEDULERS_H - - - -#endif /* SMTBASEDPERMISSIVESCHEDULERS_H */ - diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp deleted file mode 100644 index 5dec78f8d..000000000 --- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ /dev/null @@ -1,60 +0,0 @@ -#include -#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::Options options; - - options = typename storm::builder::ExplicitPrismModelBuilder::Options(formula02); - options.addConstantDefinitionsFromString(program, ""); - options.buildCommandLabels = true; - - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); - - 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); - - storm::modelchecker::SparseMdpPrctlModelChecker> checker0(*mdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - - std::unique_ptr result0 = checker0.check(formula02); - storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult(); - - ASSERT_FALSE(qualitativeResult0[0]); - - auto submdp = perms->apply(); - storm::modelchecker::SparseMdpPrctlModelChecker> checker1(submdp, std::unique_ptr>(new storm::utility::solver::MinMaxLinearEquationSolverFactory(storm::solver::EquationSolverTypeSelection::Native))); - - std::unique_ptr result1 = checker1.check(formula02); - storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult(); - - EXPECT_TRUE(qualitativeResult1[0]); - - // - -}