From 131ab5b674cf883fac5cc340fe0c18340b33bbf3 Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 25 Sep 2015 14:16:58 +0200 Subject: [PATCH] Updates on perm. schedulers Former-commit-id: 16b65774a11f50949a8f28a8968b8b48cb57d7ad --- .../MILPPermissiveSchedulers.h | 16 ++++---- .../PermissiveSchedulerComputation.h | 2 +- src/permissivesched/PermissiveSchedulers.cpp | 10 ++--- src/permissivesched/PermissiveSchedulers.h | 35 +++++++++++------ .../MilpPermissiveSchedulerTest.cpp | 39 +++++++++++++------ 5 files changed, 67 insertions(+), 35 deletions(-) diff --git a/src/permissivesched/MILPPermissiveSchedulers.h b/src/permissivesched/MILPPermissiveSchedulers.h index 6d608436b..fd171bc5a 100644 --- a/src/permissivesched/MILPPermissiveSchedulers.h +++ b/src/permissivesched/MILPPermissiveSchedulers.h @@ -51,16 +51,16 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation return !solver.isInfeasible(); } - MemorylessDeterministicPermissiveScheduler getScheduler() const override { + SubMDPPermissiveScheduler getScheduler() const override { assert(mCalledOptimizer); assert(foundSolution()); - storm::storage::BitVector result(mdp->getNumberOfChoices(), true); + SubMDPPermissiveScheduler result(*mdp, true); for(auto const& entry : multistrategyVariables) { if(!solver.getBinaryValue(entry.second)) { - result.set(mdp->getNondeterministicChoiceIndices()[entry.first.getState()]+entry.first.getAction(), false); + result.disable(mdp->getChoiceIndex(entry.first)); } } - return MemorylessDeterministicPermissiveScheduler(result); + return result; } void dumpLpToFile(std::string const& filename) { @@ -71,7 +71,7 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation 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. @@ -111,12 +111,14 @@ class MilpPermissiveSchedulerComputation : public PermissiveSchedulerComputation 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 -- ) diff --git a/src/permissivesched/PermissiveSchedulerComputation.h b/src/permissivesched/PermissiveSchedulerComputation.h index a0e135a0f..dd6e28124 100644 --- a/src/permissivesched/PermissiveSchedulerComputation.h +++ b/src/permissivesched/PermissiveSchedulerComputation.h @@ -42,7 +42,7 @@ namespace storm { virtual bool foundSolution() const = 0; - virtual MemorylessDeterministicPermissiveScheduler getScheduler() const = 0; + virtual SubMDPPermissiveScheduler getScheduler() const = 0; }; diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp index f484e0ee0..9bf7959ca 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) { + 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(); @@ -26,17 +26,17 @@ namespace storm { comp.dumpLpToFile("milpdump.lp"); std::cout << "Found Solution: " << (comp.foundSolution() ? "yes" : "no") << std::endl; if(comp.foundSolution()) { - return boost::optional(comp.getScheduler()); + return boost::optional(comp.getScheduler()); } else { - return boost::optional(); + return boost::optional(); } } - boost::optional computePermissiveSchedulerViaMC(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { + boost::optional computePermissiveSchedulerViaMC(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { } - boost::optional computerPermissiveSchedulerViaSMT(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { + boost::optional computerPermissiveSchedulerViaSMT(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) { } } diff --git a/src/permissivesched/PermissiveSchedulers.h b/src/permissivesched/PermissiveSchedulers.h index 1f9fcbec8..21c293b81 100644 --- a/src/permissivesched/PermissiveSchedulers.h +++ b/src/permissivesched/PermissiveSchedulers.h @@ -14,21 +14,34 @@ namespace storm { virtual ~PermissiveScheduler() = default; }; - class MemorylessDeterministicPermissiveScheduler : public PermissiveScheduler { - storm::storage::BitVector memdetschedulers; + class SubMDPPermissiveScheduler : public PermissiveScheduler { + storm::models::sparse::Mdp const& mdp; + storm::storage::BitVector enabledChoices; 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)) {} - + 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); + } + }; - boost::optional computePermissiveSchedulerViaMILP(std::shared_ptr> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp); + 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 a6d18d510..b156d3958 100644 --- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -1,3 +1,4 @@ +#include #include "gtest/gtest.h" #include "storm-config.h" #include "src/parser/PrismParser.h" @@ -7,7 +8,7 @@ #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"); @@ -29,15 +30,31 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { 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); - // + 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]); + + // }