sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

uint_fast64_t -> uint64_t

tempestpy_adaptions
TimQu 7 years ago
parent
11b9c60515
commit
9bccae9c5c
2 changed files with 82 additions and 82 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 150
      src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
  2. 14
      src/storm/storage/memorystructure/SparseModelMemoryProduct.h

150
src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp
View File

@ -24,10 +24,10 @@ namespace storm {
template <typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> SparseModelMemoryProduct<ValueType>::build() {
uint_fast64_t modelStateCount = model.getNumberOfStates();
uint_fast64_t memoryStateCount = memory.getNumberOfStates();
uint64_t modelStateCount = model.getNumberOfStates();
uint64_t memoryStateCount = memory.getNumberOfStates();
std::vector<uint_fast64_t> memorySuccessors = computeMemorySuccessors();
std::vector<uint64_t> memorySuccessors = computeMemorySuccessors();
// Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
storm::storage::BitVector initialStates(modelStateCount * memoryStateCount, false);
@ -41,8 +41,8 @@ namespace storm {
storm::storage::BitVector reachableStates = computeReachableStates(memorySuccessors, initialStates);
// Compute the mapping to the states of the result
uint_fast64_t reachableStateCount = 0;
toResultStateMapping = std::vector<uint_fast64_t> (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits<uint_fast64_t>::max());
uint64_t reachableStateCount = 0;
toResultStateMapping = std::vector<uint64_t> (model.getNumberOfStates() * memory.getNumberOfStates(), std::numeric_limits<uint64_t>::max());
for (auto const& reachableState : reachableStates) {
toResultStateMapping[reachableState] = reachableStateCount;
++reachableStateCount;
@ -64,18 +64,18 @@ namespace storm {
}
template <typename ValueType>
uint_fast64_t const& SparseModelMemoryProduct<ValueType>::getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const {
uint64_t const& SparseModelMemoryProduct<ValueType>::getResultState(uint64_t const& modelState, uint64_t const& memoryState) const {
return toResultStateMapping[modelState * memory.getNumberOfStates() + memoryState];
}
template <typename ValueType>
std::vector<uint_fast64_t> SparseModelMemoryProduct<ValueType>::computeMemorySuccessors() const {
uint_fast64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount();
uint_fast64_t memoryStateCount = memory.getNumberOfStates();
std::vector<uint_fast64_t> result(modelTransitionCount * memoryStateCount, std::numeric_limits<uint_fast64_t>::max());
std::vector<uint64_t> SparseModelMemoryProduct<ValueType>::computeMemorySuccessors() const {
uint64_t modelTransitionCount = model.getTransitionMatrix().getEntryCount();
uint64_t memoryStateCount = memory.getNumberOfStates();
std::vector<uint64_t> result(modelTransitionCount * memoryStateCount, std::numeric_limits<uint64_t>::max());
for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
for (uint_fast64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) {
for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
for (uint64_t transitionGoal = 0; transitionGoal < memoryStateCount; ++transitionGoal) {
auto const& memoryTransition = memory.getTransitionMatrix()[memoryState][transitionGoal];
if (memoryTransition) {
for (auto const& modelTransitionIndex : memoryTransition.get()) {
@ -88,25 +88,25 @@ namespace storm {
}
template <typename ValueType>
storm::storage::BitVector SparseModelMemoryProduct<ValueType>::computeReachableStates(std::vector<uint_fast64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates) const {
uint_fast64_t memoryStateCount = memory.getNumberOfStates();
storm::storage::BitVector SparseModelMemoryProduct<ValueType>::computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates) const {
uint64_t memoryStateCount = memory.getNumberOfStates();
// Explore the reachable states via DFS.
// A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
storm::storage::BitVector reachableStates = initialStates;
std::vector<uint_fast64_t> stack(reachableStates.begin(), reachableStates.end());
std::vector<uint64_t> stack(reachableStates.begin(), reachableStates.end());
while (!stack.empty()) {
uint_fast64_t stateIndex = stack.back();
uint64_t stateIndex = stack.back();
stack.pop_back();
uint_fast64_t modelState = stateIndex / memoryStateCount;
uint_fast64_t memoryState = stateIndex % memoryStateCount;
uint64_t modelState = stateIndex / memoryStateCount;
uint64_t memoryState = stateIndex % memoryStateCount;
auto const& rowGroup = model.getTransitionMatrix().getRowGroup(modelState);
for (auto modelTransitionIt = rowGroup.begin(); modelTransitionIt != rowGroup.end(); ++modelTransitionIt) {
if (!storm::utility::isZero(modelTransitionIt->getValue())) {
uint_fast64_t successorModelState = modelTransitionIt->getColumn();
uint_fast64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin();
uint_fast64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState];
uint_fast64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState;
uint64_t successorModelState = modelTransitionIt->getColumn();
uint64_t modelTransitionId = modelTransitionIt - model.getTransitionMatrix().begin();
uint64_t successorMemoryState = memorySuccessors[modelTransitionId * memoryStateCount + memoryState];
uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState;
if (!reachableStates.get(successorStateIndex)) {
reachableStates.set(successorStateIndex, true);
stack.push_back(successorStateIndex);
@ -118,23 +118,23 @@ namespace storm {
}
template <typename ValueType>
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint_fast64_t> const& memorySuccessors) const {
uint_fast64_t memoryStateCount = memory.getNumberOfStates();
uint_fast64_t numResStates = reachableStates.getNumberOfSetBits();
uint_fast64_t numResTransitions = 0;
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint64_t> const& memorySuccessors) const {
uint64_t memoryStateCount = memory.getNumberOfStates();
uint64_t numResStates = reachableStates.getNumberOfSetBits();
uint64_t numResTransitions = 0;
for (auto const& stateIndex : reachableStates) {
numResTransitions += model.getTransitionMatrix().getRow(stateIndex / memoryStateCount).getNumberOfEntries();
}
storm::storage::SparseMatrixBuilder<ValueType> builder(numResStates, numResStates, numResTransitions, true);
uint_fast64_t currentRow = 0;
uint64_t currentRow = 0;
for (auto const& stateIndex : reachableStates) {
uint_fast64_t modelState = stateIndex / memoryStateCount;
uint_fast64_t memoryState = stateIndex % memoryStateCount;
uint64_t modelState = stateIndex / memoryStateCount;
uint64_t memoryState = stateIndex % memoryStateCount;
auto const& modelRow = model.getTransitionMatrix().getRow(modelState);
for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) {
uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
++currentRow;
@ -144,30 +144,30 @@ namespace storm {
}
template <typename ValueType>
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint_fast64_t> const& memorySuccessors) const {
uint_fast64_t memoryStateCount = memory.getNumberOfStates();
uint_fast64_t numResStates = reachableStates.getNumberOfSetBits();
uint_fast64_t numResChoices = 0;
uint_fast64_t numResTransitions = 0;
storm::storage::SparseMatrix<ValueType> SparseModelMemoryProduct<ValueType>::buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint64_t> const& memorySuccessors) const {
uint64_t memoryStateCount = memory.getNumberOfStates();
uint64_t numResStates = reachableStates.getNumberOfSetBits();
uint64_t numResChoices = 0;
uint64_t numResTransitions = 0;
for (auto const& stateIndex : reachableStates) {
uint_fast64_t modelState = stateIndex / memoryStateCount;
for (uint_fast64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) {
uint64_t modelState = stateIndex / memoryStateCount;
for (uint64_t modelRow = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRow < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRow) {
++numResChoices;
numResTransitions += model.getTransitionMatrix().getRow(modelRow).getNumberOfEntries();
}
}
storm::storage::SparseMatrixBuilder<ValueType> builder(numResChoices, numResStates, numResTransitions, true, true, numResStates);
uint_fast64_t currentRow = 0;
uint64_t currentRow = 0;
for (auto const& stateIndex : reachableStates) {
uint_fast64_t modelState = stateIndex / memoryStateCount;
uint_fast64_t memoryState = stateIndex % memoryStateCount;
uint64_t modelState = stateIndex / memoryStateCount;
uint64_t memoryState = stateIndex % memoryStateCount;
builder.newRowGroup(currentRow);
for (uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) {
for (uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState]; modelRowIndex < model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]; ++modelRowIndex) {
auto const& modelRow = model.getTransitionMatrix().getRow(modelRowIndex);
for (auto entryIt = modelRow.begin(); entryIt != modelRow.end(); ++entryIt) {
uint_fast64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t transitionId = entryIt - model.getTransitionMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(currentRow, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
++currentRow;
@ -179,18 +179,18 @@ namespace storm {
template <typename ValueType>
storm::models::sparse::StateLabeling SparseModelMemoryProduct<ValueType>::buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) const {
uint_fast64_t modelStateCount = model.getNumberOfStates();
uint_fast64_t memoryStateCount = memory.getNumberOfStates();
uint64_t modelStateCount = model.getNumberOfStates();
uint64_t memoryStateCount = memory.getNumberOfStates();
uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount();
uint64_t numResStates = resultTransitionMatrix.getRowGroupCount();
storm::models::sparse::StateLabeling resultLabeling(numResStates);
for (std::string modelLabel : model.getStateLabeling().getLabels()) {
if (modelLabel != "init") {
storm::storage::BitVector resLabeledStates(numResStates, false);
for (auto const& modelState : model.getStateLabeling().getStates(modelLabel)) {
for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
uint_fast64_t const& resState = getResultState(modelState, memoryState);
for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
uint64_t const& resState = getResultState(modelState, memoryState);
// Check if the state exists in the result (i.e. if it is reachable)
if (resState < numResStates) {
resLabeledStates.set(resState, true);
@ -204,8 +204,8 @@ namespace storm {
STORM_LOG_THROW(!resultLabeling.containsLabel(memoryLabel), storm::exceptions::InvalidOperationException, "Failed to build the product of model and memory structure: State labelings are not disjoint as both structures contain the label " << memoryLabel << ".");
storm::storage::BitVector resLabeledStates(numResStates, false);
for (auto const& memoryState : memory.getStateLabeling().getStates(memoryLabel)) {
for (uint_fast64_t modelState = 0; modelState < modelStateCount; ++modelState) {
uint_fast64_t const& resState = getResultState(modelState, memoryState);
for (uint64_t modelState = 0; modelState < modelStateCount; ++modelState) {
uint64_t const& resState = getResultState(modelState, memoryState);
// Check if the state exists in the result (i.e. if it is reachable)
if (resState < numResStates) {
resLabeledStates.set(resState, true);
@ -218,20 +218,20 @@ namespace storm {
}
template <typename ValueType>
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> SparseModelMemoryProduct<ValueType>::buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint_fast64_t> const& memorySuccessors) const {
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> SparseModelMemoryProduct<ValueType>::buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint64_t> const& memorySuccessors) const {
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> result;
uint_fast64_t memoryStateCount = memory.getNumberOfStates();
uint_fast64_t numResStates = resultTransitionMatrix.getRowGroupCount();
uint64_t memoryStateCount = memory.getNumberOfStates();
uint64_t numResStates = resultTransitionMatrix.getRowGroupCount();
for (auto const& rewardModel : model.getRewardModels()) {
boost::optional<std::vector<ValueType>> stateRewards;
if (rewardModel.second.hasStateRewards()) {
stateRewards = std::vector<ValueType>(numResStates, storm::utility::zero<ValueType>());
uint_fast64_t modelState = 0;
uint64_t modelState = 0;
for (auto const& modelStateReward : rewardModel.second.getStateRewardVector()) {
if (!storm::utility::isZero(modelStateReward)) {
for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
uint_fast64_t const& resState = getResultState(modelState, memoryState);
for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
uint64_t const& resState = getResultState(modelState, memoryState);
// Check if the state exists in the result (i.e. if it is reachable)
if (resState < numResStates) {
stateRewards.get()[resState] = modelStateReward;
@ -244,16 +244,16 @@ namespace storm {
boost::optional<std::vector<ValueType>> stateActionRewards;
if (rewardModel.second.hasStateActionRewards()) {
stateActionRewards = std::vector<ValueType>(resultTransitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
uint_fast64_t modelState = 0;
uint_fast64_t modelRow = 0;
uint64_t modelState = 0;
uint64_t modelRow = 0;
for (auto const& modelStateActionReward : rewardModel.second.getStateActionRewardVector()) {
if (!storm::utility::isZero(modelStateActionReward)) {
while (modelRow >= model.getTransitionMatrix().getRowGroupIndices()[modelState + 1]) {
++modelState;
}
uint_fast64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState];
for (uint_fast64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
uint_fast64_t const& resState = getResultState(modelState, memoryState);
uint64_t rowOffset = modelRow - model.getTransitionMatrix().getRowGroupIndices()[modelState];
for (uint64_t memoryState = 0; memoryState < memoryStateCount; ++memoryState) {
uint64_t const& resState = getResultState(modelState, memoryState);
// Check if the state exists in the result (i.e. if it is reachable)
if (resState < numResStates) {
stateActionRewards.get()[resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset] = modelStateActionReward;
@ -266,19 +266,19 @@ namespace storm {
boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
if (rewardModel.second.hasTransitionRewards()) {
storm::storage::SparseMatrixBuilder<ValueType> builder(resultTransitionMatrix.getRowCount(), resultTransitionMatrix.getColumnCount());
uint_fast64_t stateIndex = 0;
uint64_t stateIndex = 0;
for (auto const& resState : toResultStateMapping) {
if (resState < numResStates) {
uint_fast64_t modelState = stateIndex / memoryStateCount;
uint_fast64_t memoryState = stateIndex % memoryStateCount;
uint_fast64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState);
for (uint_fast64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) {
uint_fast64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset;
uint_fast64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset;
uint64_t modelState = stateIndex / memoryStateCount;
uint64_t memoryState = stateIndex % memoryStateCount;
uint64_t rowGroupSize = resultTransitionMatrix.getRowGroupSize(resState);
for (uint64_t rowOffset = 0; rowOffset < rowGroupSize; ++rowOffset) {
uint64_t resRowIndex = resultTransitionMatrix.getRowGroupIndices()[resState] + rowOffset;
uint64_t modelRowIndex = model.getTransitionMatrix().getRowGroupIndices()[modelState] + rowOffset;
auto const& rewardMatrixRow = rewardModel.second.getTransitionRewardMatrix().getRow(modelRowIndex);
for (auto entryIt = rewardMatrixRow.begin(); entryIt != rewardMatrixRow.end(); ++entryIt) {
uint_fast64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin();
uint_fast64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
uint64_t transitionId = entryIt - rewardModel.second.getTransitionRewardMatrix().begin();
uint64_t const& successorMemoryState = memorySuccessors[transitionId * memoryStateCount + memoryState];
builder.addNextValue(resRowIndex, getResultState(entryIt->getColumn(), successorMemoryState), entryIt->getValue());
}
}
@ -300,19 +300,19 @@ namespace storm {
components.rateTransitions = true;
} else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
// We also need to translate the exit rates and the Markovian states
uint_fast64_t numResStates = components.transitionMatrix.getRowGroupCount();
uint_fast64_t memoryStateCount = memory.getNumberOfStates();
uint64_t numResStates = components.transitionMatrix.getRowGroupCount();
uint64_t memoryStateCount = memory.getNumberOfStates();
std::vector<ValueType> resultExitRates;
resultExitRates.reserve(components.transitionMatrix.getRowGroupCount());
storm::storage::BitVector resultMarkovianStates(numResStates, false);
auto const& modelExitRates = dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model).getExitRates();
auto const& modelMarkovianStates = dynamic_cast<storm::models::sparse::MarkovAutomaton<ValueType> const&>(model).getMarkovianStates();
uint_fast64_t stateIndex = 0;
uint64_t stateIndex = 0;
for (auto const& resState : toResultStateMapping) {
if (resState < numResStates) {
assert(resState == resultExitRates.size());
uint_fast64_t modelState = stateIndex / memoryStateCount;
uint64_t modelState = stateIndex / memoryStateCount;
resultExitRates.push_back(modelExitRates[modelState]);
if (modelMarkovianStates.get(modelState)) {
resultMarkovianStates.set(resState, true);

14
src/storm/storage/memorystructure/SparseModelMemoryProduct.h
View File

@ -33,33 +33,33 @@ namespace storm {
// Retrieves the state of the resulting model that represents the given memory and model state.
// An invalid index is returned, if the specifyied state does not exist (i.e., if it is not reachable).
uint_fast64_t const& getResultState(uint_fast64_t const& modelState, uint_fast64_t const& memoryState) const;
uint64_t const& getResultState(uint64_t const& modelState, uint64_t const& memoryState) const;
private:
// Computes for each pair of memory state and model transition index the successor memory state
// The resulting vector maps (modelTransition * memoryStateCount) + memoryState to the corresponding successor state of the memory structure
std::vector<uint_fast64_t> computeMemorySuccessors() const;
std::vector<uint64_t> computeMemorySuccessors() const;
// Computes the reachable states of the resulting model
storm::storage::BitVector computeReachableStates(std::vector<uint_fast64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates) const;
storm::storage::BitVector computeReachableStates(std::vector<uint64_t> const& memorySuccessors, storm::storage::BitVector const& initialStates) const;
// Methods that build the model components
// Matrix for deterministic models
storm::storage::SparseMatrix<ValueType> buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint_fast64_t> const& memorySuccessors) const;
storm::storage::SparseMatrix<ValueType> buildDeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint64_t> const& memorySuccessors) const;
// Matrix for nondeterministic models
storm::storage::SparseMatrix<ValueType> buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint_fast64_t> const& memorySuccessors) const;
storm::storage::SparseMatrix<ValueType> buildNondeterministicTransitionMatrix(storm::storage::BitVector const& reachableStates, std::vector<uint64_t> const& memorySuccessors) const;
// State labeling. Note: DOES NOT ADD A LABEL FOR THE INITIAL STATES
storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix) const;
// Reward models
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint_fast64_t> const& memorySuccessors) const;
std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> buildRewardModels(storm::storage::SparseMatrix<ValueType> const& resultTransitionMatrix, std::vector<uint64_t> const& memorySuccessors) const;
// Builds the resulting model
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildResult(storm::storage::SparseMatrix<ValueType>&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>>&& rewardModels) const;
// Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState)
std::vector<uint_fast64_t> toResultStateMapping;
std::vector<uint64_t> toResultStateMapping;
storm::models::sparse::Model<ValueType> const& model;

Write Preview
Loading…
Cancel
Save