Updates on perm. schedulers

Former-commit-id: 16b65774a1

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 -- )
                 

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;
             
        
         };

src/permissivesched/PermissiveSchedulers.cpp

@@ -11,7 +11,7 @@
 namespace storm {
     namespace ps {
         
-         boost::optional<MemorylessDeterministicPermissiveScheduler> computePermissiveSchedulerViaMILP(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
+         boost::optional<SubMDPPermissiveScheduler> computePermissiveSchedulerViaMILP(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
             storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Mdp<double>> 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<MemorylessDeterministicPermissiveScheduler>(comp.getScheduler());
+                return boost::optional<SubMDPPermissiveScheduler>(comp.getScheduler());
             } else {
-                return boost::optional<MemorylessDeterministicPermissiveScheduler>();
+                return boost::optional<SubMDPPermissiveScheduler>();
             }
         }
          
-         boost::optional<MemorylessDeterministicPermissiveScheduler> computePermissiveSchedulerViaMC(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
+         boost::optional<SubMDPPermissiveScheduler> computePermissiveSchedulerViaMC(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
              
          }
          
-         boost::optional<MemorylessDeterministicPermissiveScheduler> computerPermissiveSchedulerViaSMT(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
+         boost::optional<SubMDPPermissiveScheduler> computerPermissiveSchedulerViaSMT(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp) {
              
          }
     }

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<double> const& mdp;
+            storm::storage::BitVector enabledChoices;
         public:
-            virtual ~MemorylessDeterministicPermissiveScheduler() = default;
-            MemorylessDeterministicPermissiveScheduler(MemorylessDeterministicPermissiveScheduler&&) = default;
-            MemorylessDeterministicPermissiveScheduler(MemorylessDeterministicPermissiveScheduler const&) = delete;
+            virtual ~SubMDPPermissiveScheduler() = default;
+            SubMDPPermissiveScheduler(SubMDPPermissiveScheduler&&) = default;
+            SubMDPPermissiveScheduler(SubMDPPermissiveScheduler const&) = delete;
+
+            SubMDPPermissiveScheduler(storm::models::sparse::Mdp<double> 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);
+            }
 
 
-            MemorylessDeterministicPermissiveScheduler(storm::storage::BitVector const& allowedPairs) : memdetschedulers(allowedPairs) {}
-            MemorylessDeterministicPermissiveScheduler(storm::storage::BitVector && allowedPairs) : memdetschedulers(std::move(allowedPairs)) {}
+            storm::models::sparse::Mdp<double> apply() const {
+                return mdp.restrictChoices(enabledChoices);
+            }
 
             
         };
         
-        boost::optional<MemorylessDeterministicPermissiveScheduler> computePermissiveSchedulerViaMILP(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp);
+        boost::optional<SubMDPPermissiveScheduler> computePermissiveSchedulerViaMILP(std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, storm::logic::ProbabilityOperatorFormula const& safeProp);
     }
 }
 

test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp

@@ -1,3 +1,4 @@
+#include <src/modelchecker/results/ExplicitQualitativeCheckResult.h>
 #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<storm::models::sparse::Mdp<double>> mdp = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options)->as<storm::models::sparse::Mdp<double>>();
     
-     boost::optional<storm::ps::MemorylessDeterministicPermissiveScheduler> perms = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02);
+    boost::optional<storm::ps::SubMDPPermissiveScheduler> perms = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02);
     EXPECT_NE(perms, boost::none);
-     boost::optional<storm::ps::MemorylessDeterministicPermissiveScheduler> perms2 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001);
+    boost::optional<storm::ps::SubMDPPermissiveScheduler> perms2 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001);
     EXPECT_EQ(perms2, boost::none);
 
-     boost::optional<storm::ps::MemorylessDeterministicPermissiveScheduler> perms3 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02b);
+    boost::optional<storm::ps::SubMDPPermissiveScheduler> perms3 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula02b);
     EXPECT_EQ(perms3, boost::none);
-     boost::optional<storm::ps::MemorylessDeterministicPermissiveScheduler> perms4 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001b);
+    boost::optional<storm::ps::SubMDPPermissiveScheduler> perms4 = storm::ps::computePermissiveSchedulerViaMILP(mdp, formula001b);
     EXPECT_NE(perms4, boost::none);
+
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker0(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
+
+    std::unique_ptr<storm::modelchecker::CheckResult> result0 = checker0.check(formula02);
+    storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult0 = result0->asExplicitQualitativeCheckResult();
+
+    ASSERT_FALSE(qualitativeResult0[0]);
+
+    auto submdp = perms->apply();
+    storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker1(submdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
+
+    std::unique_ptr<storm::modelchecker::CheckResult> result1 = checker1.check(formula02);
+    storm::modelchecker::ExplicitQualitativeCheckResult& qualitativeResult1 = result1->asExplicitQualitativeCheckResult();
+
+    EXPECT_TRUE(qualitativeResult1[0]);
+
     //
     
 }