alternative memoryless scheduler application

src/storm/models/sparse/NondeterministicModel.cpp

@@ -5,6 +5,7 @@
 #include "storm/storage/Scheduler.h"
 #include "storm/storage/memorystructure/MemoryStructureBuilder.h"
 #include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
+#include "storm/transformer/SubsystemBuilder.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 
@@ -46,6 +47,13 @@ namespace storm {
             
             template<typename ValueType, typename RewardModelType>
             std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> NondeterministicModel<ValueType, RewardModelType>::applyScheduler(storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates) const {
+                if (scheduler.isMemorylessScheduler() && scheduler.isDeterministicScheduler() && !scheduler.isPartialScheduler()) {
+                    // Special case with improved handling.
+                    storm::storage::BitVector actionSelection = scheduler.computeActionSupport(getNondeterministicChoiceIndices());
+                    storm::storage::BitVector allStates(this->getNumberOfStates(), true);
+                    auto res = storm::transformer::buildSubsystem(*this, allStates, actionSelection, !dropUnreachableStates);
+                    return res.model;
+                } else {
                     storm::storage::SparseModelMemoryProduct<ValueType, RewardModelType> memoryProduct(*this, scheduler);
                     if (!dropUnreachableStates) {
                         memoryProduct.setBuildFullProduct();
@@ -53,6 +61,9 @@ namespace storm {
                     return memoryProduct.build();
                 }
 
+
+            }
+            
             template<typename ValueType, typename RewardModelType>
             void NondeterministicModel<ValueType, RewardModelType>::printModelInformationToStream(std::ostream& out) const {
                 this->printModelInformationHeaderToStream(out);

src/storm/storage/Scheduler.cpp

@@ -52,6 +52,17 @@ namespace storm {
             schedulerChoice = choice;
         }
 
+        template <typename ValueType>
+        bool Scheduler<ValueType>::isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState) const {
+            for (auto const& selectedState : selectedStates) {
+                auto& schedulerChoice = schedulerChoices[memoryState][selectedState];
+                if (!schedulerChoice.isDefined()) {
+                    return false;
+                }
+            }
+            return true;
+        }
+
         template <typename ValueType>
         void Scheduler<ValueType>::clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState) {
             STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index");
@@ -66,6 +77,24 @@ namespace storm {
             return schedulerChoices[memoryState][modelState];
         }
 
+        template<typename ValueType>
+        storm::storage::BitVector Scheduler<ValueType>::computeActionSupport(std::vector<uint_fast64_t> const& nondeterministicChoiceIndices) const {
+            auto nrActions = nondeterministicChoiceIndices.back();
+            storm::storage::BitVector result(nrActions);
+
+            for (auto const& choicesPerMemoryNode : schedulerChoices) {
+
+                STORM_LOG_ASSERT(nondeterministicChoiceIndices.size()-2 < choicesPerMemoryNode.size(), "Illegal model state index");
+                for (uint64_t stateId = 0; stateId < nondeterministicChoiceIndices.size()-1; ++stateId) {
+                    for (auto const& schedChoice : choicesPerMemoryNode[stateId].getChoiceAsDistribution()) {
+                        STORM_LOG_ASSERT(schedChoice.first < nondeterministicChoiceIndices[stateId+1] - nondeterministicChoiceIndices[stateId], "Scheduler chooses action indexed " << schedChoice.first << " in state id "  << stateId << " but state contains only " << nondeterministicChoiceIndices[stateId+1] - nondeterministicChoiceIndices[stateId] << " choices .");
+                        result.set(nondeterministicChoiceIndices[stateId] + schedChoice.first);
+                    }
+                }
+            }
+            return result;
+        }
+        
         template <typename ValueType>
         bool Scheduler<ValueType>::isPartialScheduler() const {
             return numOfUndefinedChoices != 0;

src/storm/storage/Scheduler.h

@@ -1,11 +1,12 @@
-#ifndef STORM_STORAGE_SCHEDULER_H_
-#define STORM_STORAGE_SCHEDULER_H_
+#pragma once
 
 #include <cstdint>
 #include "storm/storage/memorystructure/MemoryStructure.h"
 #include "storm/storage/SchedulerChoice.h"
 
 namespace storm {
+
+
     namespace storage {
         
         /*
@@ -35,6 +36,11 @@ namespace storm {
              */
             void setChoice(SchedulerChoice<ValueType> const& choice, uint_fast64_t modelState, uint_fast64_t memoryState = 0);
 
+            /*!
+             * Is the scheduler defined on the states indicated by the selected-states bitvector?
+             */
+            bool isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState = 0) const;
+            
             /*!
              * Clears the choice defined by the scheduler for the given state.
              *
@@ -51,6 +57,11 @@ namespace storm {
              */
             SchedulerChoice<ValueType> const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const;
 
+            /*!
+             * Compute the Action Support: A bit vector that indicates all actions that are selected with positive probability in some memory state
+             */
+            storm::storage::BitVector computeActionSupport(std::vector<uint64_t> const& nondeterministicChoiceIndicies) const;
+
             /*!
              * Retrieves whether there is a pair of model and memory state for which the choice is undefined.
              */
@@ -111,4 +122,3 @@ namespace storm {
     }
 }
 
-#endif /* STORM_STORAGE_SCHEDULER_H_ */