diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index e37de0562..190449ea6 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -339,6 +339,24 @@ namespace storm { void StandardRewardModel::setStateActionRewardValue(uint_fast64_t row, ValueType const& value) { this->optionalStateActionRewardVector.get()[row] = value; } + + template + template + void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitions) { + if (hasStateRewards()) { + getStateRewardVector()[state] = storm::utility::zero(); + } + if (hasStateActionRewards()) { + for (uint_fast64_t choice = transitions.getRowGroupIndices()[state]; choice < transitions.getRowGroupIndices()[state + 1]; ++choice) { + getStateActionRewardVector()[choice] = storm::utility::zero(); + } + } + if (hasTransitionRewards()) { + for (auto& entry : getTransitionRewardMatrix().getRowGroup(state)) { + entry.setValue(storm::utility::zero()); + } + } + } template bool StandardRewardModel::empty() const { @@ -412,7 +430,7 @@ namespace storm { template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template double StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, double const& stateRewardWeight, double const& actionRewardWeight) const; - + template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitionMatrix); template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); @@ -440,6 +458,7 @@ namespace storm { template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template storm::RationalNumber StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); + template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitionMatrix); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); template class StandardRewardModel; @@ -452,7 +471,7 @@ namespace storm { template storm::storage::BitVector StandardRewardModel::getStatesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithFilter(storm::storage::SparseMatrix const& transitionMatrix, std::function const& filter) const; - + template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitionMatrix); template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::RationalFunction StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const; template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); @@ -471,6 +490,7 @@ namespace storm { template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::Interval const & newValue); + template void StandardRewardModel::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitionMatrix); template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template class StandardRewardModel; template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index cdfce6038..ac725d06c 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -123,9 +123,13 @@ namespace storm { */ template void setStateActionReward(uint_fast64_t choiceIndex, T const& newValue); - - //ValueType maximalStateActionReward() const; - + + /*! + * Sets all available rewards at this state to zero. + */ + template + void clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix const& transitions); + /*! * Retrieves an optional value that contains the state-action reward vector if there is one. * diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index cdeaaf9a2..b3e8cd8c3 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -690,17 +690,30 @@ namespace storm { // If the row has no elements in it, we cannot make it absorbing, because we would need to move all elements // in the vector of nonzeros otherwise. if (columnValuePtr >= columnValuePtrEnd) { - throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::makeRowDirac: cannot make row " << row << " absorbing, but there is no entry in this row."; + throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::makeRowDirac: cannot make row " << row << " absorbing, because there is no entry in this row."; } + iterator lastColumnValuePtr = this->end(row) - 1; - // If there is at least one entry in this row, we can just set it to one, modify its column value to the + // If there is at least one entry in this row, we can set it to one, modify its column value to the // one given by the parameter and set all subsequent elements of this row to zero. - columnValuePtr->setColumn(column); - columnValuePtr->setValue(storm::utility::one()); - ++columnValuePtr; - for (; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) { + // However, we want to preserve that column indices within a row are ascending, so we pick an entry that is close to the desired column index + while (columnValuePtr->getColumn() < column && columnValuePtr != lastColumnValuePtr) { + if (!storm::utility::isZero(columnValuePtr->getValue())) { + --this->nonzeroEntryCount; + } + columnValuePtr->setValue(storm::utility::zero()); + ++columnValuePtr; + } + // At this point, we have found the first entry whose column is >= the desired column (or the last entry of the row, if no such column exist) + if (storm::utility::isZero(columnValuePtr->getValue())) { ++this->nonzeroEntryCount; - columnValuePtr->setColumn(0); + } + columnValuePtr->setValue(storm::utility::one()); + columnValuePtr->setColumn(column); + for (++columnValuePtr; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) { + if (!storm::utility::isZero(columnValuePtr->getValue())) { + --this->nonzeroEntryCount; + } columnValuePtr->setValue(storm::utility::zero()); } } @@ -1060,6 +1073,27 @@ namespace storm { return result; } + template + void SparseMatrix::dropZeroEntries() { + updateNonzeroEntryCount(); + if (getNonzeroEntryCount() != getEntryCount()) { + SparseMatrixBuilder builder(getRowCount(), getColumnCount(), getNonzeroEntryCount(), true); + for (index_type row = 0; row < getRowCount(); ++row) { + for (auto const& entry : getRow(row)) { + if (!storm::utility::isZero(entry.getValue())) { + builder.addNextValue(row, entry.getColumn(), entry.getValue()); + } + } + } + SparseMatrix result = builder.build(); + // Add a row grouping if necessary. + if (!hasTrivialRowGrouping()) { + result.setRowGroupIndices(getRowGroupIndices()); + } + *this = std::move(result); + } + } + template SparseMatrix SparseMatrix::selectRowsFromRowGroups(std::vector const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const { // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index dbdd4086d..125b3bd39 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -726,6 +726,11 @@ namespace storm { */ SparseMatrix filterEntries(storm::storage::BitVector const& rowFilter) const; + /*! + * Removes all zero entries from this. + */ + void dropZeroEntries(); + /** * Compares two rows. * @param i1 Index of first row diff --git a/src/storm/storage/sparse/ChoiceOrigins.cpp b/src/storm/storage/sparse/ChoiceOrigins.cpp index ac554af10..56c512f37 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.cpp +++ b/src/storm/storage/sparse/ChoiceOrigins.cpp @@ -73,6 +73,10 @@ namespace storm { return cloneWithNewIndexToIdentifierMapping(std::move(indexToIdentifierMapping)); } + void ChoiceOrigins::clearOriginOfChoice(uint_fast64_t choiceIndex) { + indexToIdentifier[choiceIndex] = getIdentifierForChoicesWithNoOrigin(); + } + std::shared_ptr ChoiceOrigins::selectChoices(std::vector const& selectedChoices) const { std::vector indexToIdentifierMapping; indexToIdentifierMapping.reserve(selectedChoices.size()); diff --git a/src/storm/storage/sparse/ChoiceOrigins.h b/src/storm/storage/sparse/ChoiceOrigins.h index 0645ca466..902fdd031 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.h +++ b/src/storm/storage/sparse/ChoiceOrigins.h @@ -68,6 +68,11 @@ namespace storm { */ std::shared_ptr selectChoices(storm::storage::BitVector const& selectedChoices) const; + /* + * Removes origin information of the given choice. + */ + void clearOriginOfChoice(uint_fast64_t choiceIndex); + /* * Derive new choice origins from this by selecting the given choices. * If an invalid choice index is selected, the corresponding choice will get the identifier for choices with no origin. @@ -90,7 +95,7 @@ namespace storm { */ virtual void computeIdentifierInfos() const = 0; - std::vector const indexToIdentifier; + std::vector indexToIdentifier; // cached identifier infos might be empty if identifiers have not been generated yet. mutable std::vector identifierToInfo; diff --git a/src/storm/transformer/SubsystemBuilder.cpp b/src/storm/transformer/SubsystemBuilder.cpp index daca08a5d..44449c5ce 100644 --- a/src/storm/transformer/SubsystemBuilder.cpp +++ b/src/storm/transformer/SubsystemBuilder.cpp @@ -16,6 +16,7 @@ #include "storm/utility/builder.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/UnexpectedException.h" namespace storm { @@ -37,6 +38,7 @@ namespace storm { } else { STORM_LOG_THROW(originalModel.isOfType(storm::models::ModelType::Dtmc) || originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Unexpected model type."); } + // Nothing to be done if the model has deadlock States } template @@ -59,6 +61,7 @@ namespace storm { template SubsystemBuilderReturnType internalBuildSubsystem(storm::models::sparse::Model const& originalModel, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, SubsystemBuilderOptions const& options ) { + auto const& groupIndices = originalModel.getTransitionMatrix().getRowGroupIndices(); SubsystemBuilderReturnType result; uint_fast64_t subsystemStateCount = subsystemStates.getNumberOfSetBits(); if (options.buildStateMapping) { @@ -67,21 +70,20 @@ namespace storm { if (options.buildActionMapping) { result.newToOldActionIndexMapping.reserve(subsystemActions.getNumberOfSetBits()); } - if (options.buildKeptActions) { - result.keptActions = storm::storage::BitVector(originalModel.getTransitionMatrix().getRowCount(), false); - + storm::storage::BitVector deadlockStates; + if (options.fixDeadlocks) { + deadlockStates.resize(subsystemStates.size(), false); } - + // Get the set of actions that stay in the subsystem. + // Also establish the mappings if requested. + storm::storage::BitVector keptActions(originalModel.getTransitionMatrix().getRowCount(), false); for (auto subsysState : subsystemStates) { if (options.buildStateMapping) { result.newToOldStateIndexMapping.push_back(subsysState); } - bool keepAtLeastOneAction = !options.checkTransitionsOutside; // For debug mode only. - bool atLeastOneActionSelected = false; // For debug mode only. - for (uint_fast64_t row = subsystemActions.getNextSetIndex(originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]); row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; row = subsystemActions.getNextSetIndex(row+1)) { + bool hasDeadlock = true; + for (uint_fast64_t row = subsystemActions.getNextSetIndex(groupIndices[subsysState]); row < groupIndices[subsysState+1]; row = subsystemActions.getNextSetIndex(row + 1)) { bool allRowEntriesStayInSubsys = true; - atLeastOneActionSelected = true; - if (options.checkTransitionsOutside) { for (auto const &entry : originalModel.getTransitionMatrix().getRow(row)) { if (!subsystemStates.get(entry.getColumn())) { @@ -91,42 +93,87 @@ namespace storm { } } if (allRowEntriesStayInSubsys) { - keepAtLeastOneAction = true; + if (options.buildActionMapping) { + result.newToOldActionIndexMapping.push_back(row); + } + keptActions.set(row, true); + hasDeadlock = false; } + } + if (hasDeadlock) { + STORM_LOG_THROW(options.fixDeadlocks, storm::exceptions::InvalidOperationException, "Expected that in each state, at least one action is selected. Got a deadlock state instead. (violated at " << subsysState << ")"); if (options.buildActionMapping) { - result.newToOldActionIndexMapping.push_back(row); - } - if (options.buildKeptActions) { - result.keptActions.set(row, allRowEntriesStayInSubsys); + result.newToOldActionIndexMapping.push_back(std::numeric_limits::max()); } + deadlockStates.set(subsysState); } - if (!atLeastOneActionSelected && options.fixDeadlocks) { - - } - STORM_LOG_ASSERT(atLeastOneActionSelected, "Expected that in each state, at least one action is selected. (violated at " << subsysState << ")"); - STORM_LOG_ASSERT(keepAtLeastOneAction, "Expected that in each state, at least one action is preserved at least one action is selected. (violated at " << subsysState << ")"); } - + // If we have deadlock states we keep an action in each rowgroup of a deadlock states. + bool hasDeadlockStates = !deadlockStates.empty(); + if (options.buildKeptActions) { + // store them now, before changing them. + result.keptActions = keptActions; + } + for (auto const& deadlockState : deadlockStates) { + keptActions.set(groupIndices[deadlockState], true); + } + // Transform the components of the model storm::storage::sparse::ModelComponents components; - components.transitionMatrix = originalModel.getTransitionMatrix().getSubmatrix(false, result.keptActions, subsystemStates); + if (hasDeadlockStates) { + // make deadlock choices a selfloop + components.transitionMatrix = originalModel.getTransitionMatrix(); + components.transitionMatrix.makeRowGroupsAbsorbing(deadlockStates); + components.transitionMatrix.dropZeroEntries(); + components.transitionMatrix = components.transitionMatrix.getSubmatrix(false, keptActions, subsystemStates); + } else { + components.transitionMatrix = originalModel.getTransitionMatrix().getSubmatrix(false, keptActions, subsystemStates); + } components.stateLabeling = originalModel.getStateLabeling().getSubLabeling(subsystemStates); for (auto const& rewardModel : originalModel.getRewardModels()){ - components.rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, subsystemStates, result.keptActions))); + components.rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, subsystemStates, keptActions))); } if (originalModel.hasChoiceLabeling()) { - components.choiceLabeling = originalModel.getChoiceLabeling().getSubLabeling(result.keptActions); + components.choiceLabeling = originalModel.getChoiceLabeling().getSubLabeling(keptActions); } if (originalModel.hasStateValuations()) { components.stateValuations = originalModel.getStateValuations().selectStates(subsystemStates); } if (originalModel.hasChoiceOrigins()) { - components.choiceOrigins = originalModel.getChoiceOrigins()->selectChoices(result.keptActions); + components.choiceOrigins = originalModel.getChoiceOrigins()->selectChoices(keptActions); + } + + if (hasDeadlockStates) { + auto subDeadlockStates = deadlockStates % subsystemStates; + assert(deadlockStates.getNumberOfSetBits() == subDeadlockStates.getNumberOfSetBits()); + // erase rewards, choice labels, choice origins + for (auto& rewModel : components.rewardModels) { + for (auto const& state : subDeadlockStates) { + rewModel.second.clearRewardAtState(state, components.transitionMatrix); + } + } + if (components.choiceLabeling) { + storm::storage::BitVector nonDeadlockChoices(components.transitionMatrix.getRowCount(), true); + for (auto const& state : subDeadlockStates) { + auto const& choice = components.transitionMatrix.getRowGroupIndices()[state]; + nonDeadlockChoices.set(choice, false); + } + for (auto const& label : components.choiceLabeling.get().getLabels()) { + components.choiceLabeling->setChoices(label, components.choiceLabeling->getChoices(label) & nonDeadlockChoices); + } + } + if (components.choiceOrigins) { + for (auto const& state : subDeadlockStates) { + auto const& choice = components.transitionMatrix.getRowGroupIndices()[state]; + components.choiceOrigins.get()->clearOriginOfChoice(choice); + } + } } transformModelSpecificComponents(originalModel, subsystemStates, components); result.model = storm::utility::builder::buildModelFromComponents(originalModel.getType(), std::move(components)); + STORM_LOG_DEBUG("Subsystem Builder is done. Resulting model has " << result.model->getNumberOfStates() << " states."); return result; } diff --git a/src/storm/transformer/SubsystemBuilder.h b/src/storm/transformer/SubsystemBuilder.h index 9f18bfb1a..cf7aefaaf 100644 --- a/src/storm/transformer/SubsystemBuilder.h +++ b/src/storm/transformer/SubsystemBuilder.h @@ -17,6 +17,7 @@ namespace storm { // Gives for each state in the resulting model the corresponding state in the original model. std::vector newToOldStateIndexMapping; // Gives for each action in the resulting model the corresponding action in the original model. + // If this action was introduced to fix a deadlock, it will get index std::numeric_limits::max() std::vector newToOldActionIndexMapping; // marks the actions of the original model that are still available in the subsystem storm::storage::BitVector keptActions; @@ -27,7 +28,7 @@ namespace storm { bool buildStateMapping = true; bool buildActionMapping = false; bool buildKeptActions = true; - bool fixDeadlocks = true; + bool fixDeadlocks = false; }; /* @@ -40,7 +41,9 @@ namespace storm { * * it originates from a state that is part of the subsystem AND * * it does not contain a transition leading to a state outside of the subsystem. * - * If this introduces a deadlock state (i.e., a state without an action) an exception is thrown. + * If this introduces a deadlock state (i.e., a state without an action) it is either + * * fixed by inserting a selfloop (if fixDeadlocks is true) or + * * an exception is thrown (otherwise). * * @param originalModel The original model. * @param subsystemStates The selected states. @@ -49,5 +52,7 @@ namespace storm { */ template > SubsystemBuilderReturnType buildSubsystem(storm::models::sparse::Model const& originalModel, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, bool keepUnreachableStates = true, SubsystemBuilderOptions options = SubsystemBuilderOptions()); + + } }