From c4e7fdd5e5474e637bf58cad5d34d71d25f68141 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 20 Nov 2018 22:54:37 +0100
Subject: [PATCH] alternative memoryless scheduler application
---
.../models/sparse/NondeterministicModel.cpp | 19 +++++++++---
src/storm/storage/Scheduler.cpp | 29 +++++++++++++++++++
src/storm/storage/Scheduler.h | 18 +++++++++---
3 files changed, 58 insertions(+), 8 deletions(-)
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<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 {
- storm::storage::SparseModelMemoryProduct<ValueType, RewardModelType> 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<ValueType, RewardModelType> memoryProduct(*this, scheduler);
+ if (!dropUnreachableStates) {
+ memoryProduct.setBuildFullProduct();
+ }
+ return memoryProduct.build();
}
- return memoryProduct.build();
+
+
}
template<typename ValueType, typename RewardModelType>
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 <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");
@@ -65,6 +76,24 @@ namespace storm {
STORM_LOG_ASSERT(modelState < schedulerChoices[memoryState].size(), "Illegal model state index");
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 {
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 <cstdint>
#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<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.
@@ -50,7 +56,12 @@ namespace storm {
* @param memoryState the memory state which we consider.
*/
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_ */