SubsystemBuilder: Fix deadlocks with a selfloop (if requested)

src/storm/models/sparse/StandardRewardModel.cpp

@@ -339,6 +339,24 @@ namespace storm {
             void StandardRewardModel<ValueType>::setStateActionRewardValue(uint_fast64_t row, ValueType const& value) {
                 this->optionalStateActionRewardVector.get()[row] = value;
             }
+
+            template<typename ValueType>
+            template<typename MatrixValueType>
+            void StandardRewardModel<ValueType>::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<MatrixValueType> const& transitions) {
+                if (hasStateRewards()) {
+                    getStateRewardVector()[state] = storm::utility::zero<ValueType>();
+                }
+                if (hasStateActionRewards()) {
+                    for (uint_fast64_t choice = transitions.getRowGroupIndices()[state]; choice < transitions.getRowGroupIndices()[state + 1]; ++choice) {
+                        getStateActionRewardVector()[choice] = storm::utility::zero<ValueType>();
+                    }
+                }
+                if (hasTransitionRewards()) {
+                    for (auto& entry : getTransitionRewardMatrix().getRowGroup(state)) {
+                        entry.setValue(storm::utility::zero<ValueType>());
+                    }
+                }
+            }
             
             template<typename ValueType>
             bool StandardRewardModel<ValueType>::empty() const {
@@ -412,7 +430,7 @@ namespace storm {
             template storm::storage::BitVector StandardRewardModel<double>::getChoicesWithZeroReward(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
             template storm::storage::BitVector StandardRewardModel<double>::getChoicesWithFilter(storm::storage::SparseMatrix<double> const& transitionMatrix, std::function<bool(double const&)> const& filter) const;
             template double StandardRewardModel<double>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<double> const& transitionMatrix, double const& stateRewardWeight, double const& actionRewardWeight) const;
-
+            template void StandardRewardModel<double>::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<double> const& transitionMatrix);
             template void StandardRewardModel<double>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards, std::vector<double> const* weights);
             template void StandardRewardModel<double>::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue);
             template void StandardRewardModel<double>::setStateReward(uint_fast64_t state, double const & newValue);
@@ -440,6 +458,7 @@ namespace storm {
             template storm::storage::BitVector StandardRewardModel<storm::RationalNumber>::getChoicesWithFilter(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::function<bool(storm::RationalNumber const&)> const& filter) const;
             template storm::RationalNumber StandardRewardModel<storm::RationalNumber>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const;
             template void StandardRewardModel<storm::RationalNumber>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, bool reduceToStateRewards, std::vector<storm::RationalNumber> const* weights);
+            template void StandardRewardModel<storm::RationalNumber>::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix);
             template void StandardRewardModel<storm::RationalNumber>::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue);
             template void StandardRewardModel<storm::RationalNumber>::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue);
             template class StandardRewardModel<storm::RationalNumber>;
@@ -452,7 +471,7 @@ namespace storm {
             template storm::storage::BitVector StandardRewardModel<storm::RationalFunction>::getStatesWithFilter(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::function<bool(storm::RationalFunction const&)> const& filter) const;
             template storm::storage::BitVector StandardRewardModel<storm::RationalFunction>::getChoicesWithZeroReward(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix) const;
             template storm::storage::BitVector StandardRewardModel<storm::RationalFunction>::getChoicesWithFilter(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, std::function<bool(storm::RationalFunction const&)> const& filter) const;
-
+            template void StandardRewardModel<storm::RationalFunction>::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix);
             template std::vector<storm::RationalFunction> StandardRewardModel<storm::RationalFunction>::getTotalActionRewardVector(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix,  std::vector<storm::RationalFunction> const& stateRewardWeights) const;
             template storm::RationalFunction StandardRewardModel<storm::RationalFunction>::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const;
             template void StandardRewardModel<storm::RationalFunction>::reduceToStateBasedRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, bool reduceToStateRewards, std::vector<storm::RationalFunction> const* weights);
@@ -471,6 +490,7 @@ namespace storm {
             template void StandardRewardModel<storm::Interval>::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue);
             template void StandardRewardModel<storm::Interval>::setStateReward(uint_fast64_t state, double const & newValue);
             template void StandardRewardModel<storm::Interval>::setStateReward(uint_fast64_t state, storm::Interval const & newValue);
+            template void StandardRewardModel<storm::Interval>::clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<double> const& transitionMatrix);
             template void StandardRewardModel<storm::Interval>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards, std::vector<double> const* weights);
             template class StandardRewardModel<storm::Interval>;
             template std::ostream& operator<<<storm::Interval>(std::ostream& out, StandardRewardModel<storm::Interval> const& rewardModel);

src/storm/models/sparse/StandardRewardModel.h

@@ -123,9 +123,13 @@ namespace storm {
                  */
                 template<typename T>
                 void setStateActionReward(uint_fast64_t choiceIndex, T const& newValue);
-
-                //ValueType maximalStateActionReward() const;
-
+                
+                /*!
+                 * Sets all available rewards at this state to zero.
+                 */
+                template<typename MatrixValueType>
+                void clearRewardAtState(uint_fast64_t state, storm::storage::SparseMatrix<MatrixValueType> const& transitions);
+                
                 /*!
                  * Retrieves an optional value that contains the state-action reward vector if there is one.
                  *

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<ValueType>());
-            ++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<ValueType>());
+                ++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<ValueType>());
+            columnValuePtr->setColumn(column);
+            for (++columnValuePtr; columnValuePtr != columnValuePtrEnd; ++columnValuePtr) {
+                if (!storm::utility::isZero(columnValuePtr->getValue())) {
+                    --this->nonzeroEntryCount;
+                }
                 columnValuePtr->setValue(storm::utility::zero<ValueType>());
             }
         }
@@ -1060,6 +1073,27 @@ namespace storm {
             return result;
         }
         
+        template<typename ValueType>
+        void SparseMatrix<ValueType>::dropZeroEntries() {
+            updateNonzeroEntryCount();
+            if (getNonzeroEntryCount() != getEntryCount()) {
+                SparseMatrixBuilder<ValueType> 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<ValueType> result = builder.build();
+                // Add a row grouping if necessary.
+                if (!hasTrivialRowGrouping()) {
+                    result.setRowGroupIndices(getRowGroupIndices());
+                }
+                *this = std::move(result);
+            }
+        }
+        
         template<typename ValueType>
         SparseMatrix<ValueType> SparseMatrix<ValueType>::selectRowsFromRowGroups(std::vector<index_type> const& rowGroupToRowIndexMapping, bool insertDiagonalEntries) const {
             // First, we need to count how many non-zero entries the resulting matrix will have and reserve space for

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

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> ChoiceOrigins::selectChoices(std::vector<uint_fast64_t> const& selectedChoices) const {
                 std::vector<uint_fast64_t> indexToIdentifierMapping;
                 indexToIdentifierMapping.reserve(selectedChoices.size());

src/storm/storage/sparse/ChoiceOrigins.h

@@ -68,6 +68,11 @@ namespace storm {
                  */
                 std::shared_ptr<ChoiceOrigins> 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<uint_fast64_t> const indexToIdentifier;
+                std::vector<uint_fast64_t> indexToIdentifier;
                 
                 // cached identifier infos might be empty if identifiers have not been generated yet.
                 mutable std::vector<std::string> identifierToInfo;

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<typename RewardModelType>
@@ -59,6 +61,7 @@ namespace storm {
         template <typename ValueType, typename RewardModelType>
         SubsystemBuilderReturnType<ValueType, RewardModelType> internalBuildSubsystem(storm::models::sparse::Model<ValueType, RewardModelType> const& originalModel, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, SubsystemBuilderOptions const& options ) {
 
+            auto const& groupIndices = originalModel.getTransitionMatrix().getRowGroupIndices();
             SubsystemBuilderReturnType<ValueType, RewardModelType> 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<uint64_t>::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<ValueType, RewardModelType> 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<ValueType, RewardModelType>(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;
         }

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<uint_fast64_t> 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<uint64_t>::max()
             std::vector<uint64_t> 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 <typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
         SubsystemBuilderReturnType<ValueType, RewardModelType> buildSubsystem(storm::models::sparse::Model<ValueType, RewardModelType> const& originalModel, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& subsystemActions, bool keepUnreachableStates = true, SubsystemBuilderOptions options = SubsystemBuilderOptions());
+        
+
     }
 }