diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 7329f9f19..1a5cfd7b1 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/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,11 +47,21 @@ namespace storm { template std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) const { - storm::storage::SparseModelMemoryProduct memoryProduct(*this, scheduler); - if (!dropUnreachableStates) { - memoryProduct.setBuildFullProduct(); + 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 memoryProduct(*this, scheduler); + if (!dropUnreachableStates) { + memoryProduct.setBuildFullProduct(); + } + return memoryProduct.build(); } - return memoryProduct.build(); + + } template diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 7ddc7e457..252cd1ebc 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -52,6 +52,17 @@ namespace storm { schedulerChoice = choice; } + template + bool Scheduler::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 void Scheduler::clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState) { STORM_LOG_ASSERT(memoryState < getNumberOfMemoryStates(), "Illegal memory state index"); @@ -65,6 +76,24 @@ namespace storm { STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index"); return schedulerChoices[memoryState][modelState]; } + + template + storm::storage::BitVector Scheduler::computeActionSupport(std::vector 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 bool Scheduler::isPartialScheduler() const { diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h index f3777cf55..c6aa30b32 100644 --- a/src/storm/storage/Scheduler.h +++ b/src/storm/storage/Scheduler.h @@ -1,11 +1,12 @@ -#ifndef STORM_STORAGE_SCHEDULER_H_ -#define STORM_STORAGE_SCHEDULER_H_ +#pragma once #include #include "storm/storage/memorystructure/MemoryStructure.h" #include "storm/storage/SchedulerChoice.h" namespace storm { + + namespace storage { /* @@ -34,6 +35,11 @@ namespace storm { * @param memoryState The state of the memoryStructure for which to set the choice. */ void setChoice(SchedulerChoice 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. @@ -50,7 +56,12 @@ namespace storm { * @param memoryState the memory state which we consider. */ SchedulerChoice 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 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_ */