added GameMECDecomposition for testing purposes

src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp

@@ -4,6 +4,7 @@
 
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/MaximalEndComponentDecomposition.h"
+#include "storm/storage/GameMaximalEndComponentDecomposition.h"
 #include "storm/storage/Scheduler.h"
 
 #include "storm/solver/MinMaxLinearEquationSolver.h"
@@ -61,7 +62,7 @@ namespace storm {
                         this->_computedBackwardTransitions = std::make_unique<storm::storage::SparseMatrix<ValueType>>(this->_transitionMatrix.transpose(true));
                         this->_backwardTransitions = this->_computedBackwardTransitions.get();
                     }
-                    this->_computedLongRunComponentDecomposition = std::make_unique<storm::storage::MaximalEndComponentDecomposition<ValueType>>(this->_transitionMatrix, *this->_backwardTransitions);
+                    this->_computedLongRunComponentDecomposition = std::make_unique<storm::storage::GameMaximalEndComponentDecomposition<ValueType>>(this->_transitionMatrix, *this->_backwardTransitions);
                     this->_longRunComponentDecomposition = this->_computedLongRunComponentDecomposition.get();
                 }
             }

src/storm/storage/GameMaximalEndComponentDecomposition.cpp

@@ -0,0 +1,281 @@
+#include <list>
+#include <queue>
+#include <numeric>
+
+#include "storm/models/sparse/StandardRewardModel.h"
+
+#include "storm/storage/GameMaximalEndComponentDecomposition.h"
+#include "storm/storage/StronglyConnectedComponentDecomposition.h"
+
+namespace storm {
+    namespace storage {
+
+        template<typename ValueType>
+        GameMaximalEndComponentDecomposition<ValueType>::GameMaximalEndComponentDecomposition() : Decomposition() {
+            // Intentionally left empty.
+        }
+
+        template<typename ValueType>
+        template<typename RewardModelType>
+        GameMaximalEndComponentDecomposition<ValueType>::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<ValueType, RewardModelType> const& model) {
+            singleMEC(model.getTransitionMatrix(), model.getBackwardTransitions());
+            //performGameMaximalEndComponentDecomposition(model.getTransitionMatrix(), model.getBackwardTransitions());
+        }
+
+        template<typename ValueType>
+        GameMaximalEndComponentDecomposition<ValueType>::GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
+            singleMEC(transitionMatrix, backwardTransitions);
+            //performGameMaximalEndComponentDecomposition(transitionMatrix, backwardTransitions);
+        }
+
+        template<typename ValueType>
+        GameMaximalEndComponentDecomposition<ValueType>::GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& states) {
+        }
+
+        template<typename ValueType>
+        GameMaximalEndComponentDecomposition<ValueType>::GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& states, storm::storage::BitVector const& choices) {
+        }
+
+        template<typename ValueType>
+        GameMaximalEndComponentDecomposition<ValueType>::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<ValueType> const& model, storm::storage::BitVector const& states) {
+        }
+
+        template<typename ValueType>
+        GameMaximalEndComponentDecomposition<ValueType>::GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition const& other) : Decomposition(other) {
+            // Intentionally left empty.
+        }
+
+        template<typename ValueType>
+        GameMaximalEndComponentDecomposition<ValueType>& GameMaximalEndComponentDecomposition<ValueType>::operator=(GameMaximalEndComponentDecomposition const& other) {
+            Decomposition::operator=(other);
+            return *this;
+        }
+
+        template<typename ValueType>
+        GameMaximalEndComponentDecomposition<ValueType>::GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition&& other) : Decomposition(std::move(other)) {
+            // Intentionally left empty.
+        }
+
+        template<typename ValueType>
+        GameMaximalEndComponentDecomposition<ValueType>& GameMaximalEndComponentDecomposition<ValueType>::operator=(GameMaximalEndComponentDecomposition&& other) {
+            Decomposition::operator=(std::move(other));
+            return *this;
+        }
+
+        template <typename ValueType>
+        void GameMaximalEndComponentDecomposition<ValueType>::performGameMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> backwardTransitions, storm::storage::BitVector const* states, storm::storage::BitVector const* choices) {
+            // Get some data for convenient access.
+            uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount();
+            std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
+
+            // Initialize the maximal end component list to be the full state space.
+            std::list<StateBlock> endComponentStateSets;
+            if (states) {
+                endComponentStateSets.emplace_back(states->begin(), states->end(), true);
+            } else {
+                std::vector<storm::storage::sparse::state_type> allStates;
+                allStates.resize(transitionMatrix.getRowGroupCount());
+                std::iota(allStates.begin(), allStates.end(), 0);
+                endComponentStateSets.emplace_back(allStates.begin(), allStates.end(), true);
+            }
+            storm::storage::BitVector statesToCheck(numberOfStates);
+            storm::storage::BitVector includedChoices;
+            if (choices) {
+                includedChoices = *choices;
+            } else if (states) {
+                includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount());
+                for (auto state : *states) {
+                    for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
+                        includedChoices.set(choice, true);
+                    }
+                }
+            } else {
+                includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount(), true);
+            }
+            storm::storage::BitVector currMecAsBitVector(transitionMatrix.getRowGroupCount());
+
+            for (std::list<StateBlock>::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) {
+                StateBlock const& mec = *mecIterator;
+                currMecAsBitVector.clear();
+                currMecAsBitVector.set(mec.begin(), mec.end(), true);
+                // Keep track of whether the MEC changed during this iteration.
+                bool mecChanged = false;
+
+                // Get an SCC decomposition of the current MEC candidate.
+
+                StronglyConnectedComponentDecomposition<ValueType> sccs(transitionMatrix, StronglyConnectedComponentDecompositionOptions().subsystem(&currMecAsBitVector).choices(&includedChoices).dropNaiveSccs());
+                for(auto const& sc: sccs) {
+                    STORM_LOG_DEBUG("SCC size: " << sc.size());
+                }
+
+                // We need to do another iteration in case we have either more than once SCC or the SCC is smaller than
+                // the MEC canditate itself.
+                mecChanged |= sccs.size() != 1 || (sccs.size() > 0 && sccs[0].size() < mec.size());
+
+                // Check for each of the SCCs whether all actions for each state do not leave the SCC. // TODO there is certainly a better way to do that...
+                for (auto& scc : sccs) {
+                    statesToCheck.set(scc.begin(), scc.end());
+
+                    while (!statesToCheck.empty()) {
+                        storm::storage::BitVector statesToRemove(numberOfStates);
+
+                        for (auto state : statesToCheck) {
+                            bool keepStateInMEC = true;
+
+                            for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
+
+                                // If the choice is not part of our subsystem, skip it.
+                                if (choices && !choices->get(choice)) {
+                                    continue;
+                                }
+
+                                // If the choice is not included any more, skip it.
+                                //if (!includedChoices.get(choice)) {
+                                //    continue;
+                                //}
+
+                                bool choiceContainedInMEC = true;
+                                for (auto const& entry : transitionMatrix.getRow(choice)) {
+                                    if (storm::utility::isZero(entry.getValue())) {
+                                        continue;
+                                    }
+
+                                    if (!scc.containsState(entry.getColumn())) {
+                                        //includedChoices.set(choice, false);
+                                        choiceContainedInMEC = false;
+                                        break;
+                                    }
+                                }
+
+                                //TODO If there is at least one choice whose successor states are fully contained in the MEC, we can leave the state in the MEC.
+                                if (!choiceContainedInMEC) {
+                                    keepStateInMEC = false;
+                                    break;
+                                }
+                            }
+                            if (!keepStateInMEC) {
+                                statesToRemove.set(state, true);
+                            }
+
+                        }
+
+                        // Now erase the states that have no option to stay inside the MEC with all successors.
+                        mecChanged |= !statesToRemove.empty();
+                        for (uint_fast64_t state : statesToRemove) {
+                            scc.erase(state);
+                        }
+
+                        // Now check which states should be reconsidered, because successors of them were removed.
+                        statesToCheck.clear();
+                        for (auto state : statesToRemove) {
+                            for (auto const& entry : backwardTransitions.getRow(state)) {
+                                if (scc.containsState(entry.getColumn())) {
+                                    statesToCheck.set(entry.getColumn());
+                                }
+                            }
+                        }
+                    }
+                }
+
+                // If the MEC changed, we delete it from the list of MECs and append the possible new MEC candidates to
+                // the list instead.
+                if (mecChanged) {
+                    for (StronglyConnectedComponent& scc : sccs) {
+                        if (!scc.empty()) {
+                            endComponentStateSets.push_back(std::move(scc));
+                        }
+                    }
+
+                    std::list<StateBlock>::const_iterator eraseIterator(mecIterator);
+                    ++mecIterator;
+                    endComponentStateSets.erase(eraseIterator);
+                } else {
+                    // Otherwise, we proceed with the next MEC candidate.
+                    ++mecIterator;
+                }
+
+            } // End of loop over all MEC candidates.
+
+            // Now that we computed the underlying state sets of the MECs, we need to properly identify the choices
+            // contained in the MEC and store them as actual MECs.
+            this->blocks.reserve(endComponentStateSets.size());
+            for (auto const& mecStateSet : endComponentStateSets) {
+                MaximalEndComponent newMec;
+
+                for (auto state : mecStateSet) {
+                    MaximalEndComponent::set_type containedChoices;
+                    for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
+                        // Skip the choice if it is not part of our subsystem.
+                        if (choices && !choices->get(choice)) {
+                            continue;
+                        }
+
+                        if (includedChoices.get(choice)) {
+                            containedChoices.insert(choice);
+                        }
+                    }
+
+                    STORM_LOG_ASSERT(!containedChoices.empty(), "The contained choices of any state in an MEC must be non-empty.");
+                    newMec.addState(state, std::move(containedChoices));
+                }
+
+                this->blocks.emplace_back(std::move(newMec));
+            }
+
+            STORM_LOG_DEBUG("MEC decomposition found " << this->size() << " GMEC(s).");
+        }
+
+        template <typename ValueType>
+        void GameMaximalEndComponentDecomposition<ValueType>::singleMEC(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> backwardTransitions, storm::storage::BitVector const* states, storm::storage::BitVector const* choices) {
+            MaximalEndComponent singleMec;
+
+            std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
+
+            std::list<StateBlock> endComponentStateSets;
+            std::vector<storm::storage::sparse::state_type> allStates;
+            allStates.resize(transitionMatrix.getRowGroupCount());
+            std::iota(allStates.begin(), allStates.end(), 0);
+            endComponentStateSets.emplace_back(allStates.begin(), allStates.end(), true);
+
+            storm::storage::BitVector includedChoices = storm::storage::BitVector(transitionMatrix.getRowCount(), true);
+            this->blocks.reserve(endComponentStateSets.size());
+            for (auto const& mecStateSet : endComponentStateSets) {
+                MaximalEndComponent newMec;
+
+                for (auto state : mecStateSet) {
+                    MaximalEndComponent::set_type containedChoices;
+                    for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
+                        // Skip the choice if it is not part of our subsystem.
+                        if (choices && !choices->get(choice)) {
+                            continue;
+                        }
+
+                        if (includedChoices.get(choice)) {
+                            containedChoices.insert(choice);
+                        }
+                    }
+
+                    STORM_LOG_ASSERT(!containedChoices.empty(), "The contained choices of any state in an MEC must be non-empty.");
+                    newMec.addState(state, std::move(containedChoices));
+                }
+
+                this->blocks.emplace_back(std::move(newMec));
+            }
+
+            STORM_LOG_DEBUG("Whole state space is one single MEC");
+
+        }
+
+        // Explicitly instantiate the MEC decomposition.
+        template class GameMaximalEndComponentDecomposition<double>;
+        template GameMaximalEndComponentDecomposition<double>::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<double> const& model);
+
+#ifdef STORM_HAVE_CARL
+        template class GameMaximalEndComponentDecomposition<storm::RationalNumber>;
+        template GameMaximalEndComponentDecomposition<storm::RationalNumber>::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model);
+
+        template class GameMaximalEndComponentDecomposition<storm::RationalFunction>;
+        template GameMaximalEndComponentDecomposition<storm::RationalFunction>::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<storm::RationalFunction> const& model);
+#endif
+    }
+}

src/storm/storage/GameMaximalEndComponentDecomposition.h

@@ -0,0 +1,109 @@
+#ifndef STORM_STORAGE_GAMEMAXIMALENDCOMPONENTDECOMPOSITION_H_
+#define STORM_STORAGE_GAMEMAXIMALENDCOMPONENTDECOMPOSITION_H_
+
+#include "storm/storage/Decomposition.h"
+#include "storm/storage/MaximalEndComponent.h"
+#include "storm/models/sparse/NondeterministicModel.h"
+
+namespace storm  {
+    namespace storage {
+
+        /*!
+         * This class represents the decomposition of a stochastic multiplayer game into its (irreducible) maximal end components.
+         */
+        template <typename ValueType>
+        class GameMaximalEndComponentDecomposition : public Decomposition<MaximalEndComponent> {
+        public:
+            /*
+             * Creates an empty MEC decomposition.
+             */
+            GameMaximalEndComponentDecomposition();
+
+            /*
+             * Creates an MEC decomposition of the given model.
+             *
+             * @param model The model to decompose into MECs.
+             */
+            template <typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
+            GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<ValueType, RewardModelType> const& model);
+
+            /*
+             * Creates an MEC decomposition of the given model (represented by a row-grouped matrix).
+             *
+             * @param transitionMatrix The transition relation of model to decompose into MECs.
+             * @param backwardTransition The reversed transition relation.
+             */
+            GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
+
+            /*
+             * Creates an MEC decomposition of the given subsystem of given model (represented by a row-grouped matrix).
+             *
+             * @param transitionMatrix The transition relation of model to decompose into MECs.
+             * @param backwardTransition The reversed transition relation.
+             * @param states The states of the subsystem to decompose.
+             */
+            GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& states);
+
+            /*
+             * Creates an MEC decomposition of the given subsystem of given model (represented by a row-grouped matrix).
+             *
+             * @param transitionMatrix The transition relation of model to decompose into MECs.
+             * @param backwardTransition The reversed transition relation.
+             * @param states The states of the subsystem to decompose.
+             * @param choices The choices of the subsystem to decompose.
+             */
+            GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& states, storm::storage::BitVector const& choices);
+
+            /*!
+             * Creates an MEC decomposition of the given subsystem in the given model.
+             *
+             * @param model The model whose subsystem to decompose into MECs.
+             * @param states The states of the subsystem to decompose.
+             */
+            GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<ValueType> const& model, storm::storage::BitVector const& states);
+
+            /*!
+             * Creates an MEC decomposition by copying the contents of the given MEC decomposition.
+             *
+             * @param other The MEC decomposition to copy.
+             */
+            GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition const& other);
+
+            /*!
+             * Assigns the contents of the given MEC decomposition to the current one by copying its contents.
+             *
+             * @param other The MEC decomposition from which to copy-assign.
+             */
+            GameMaximalEndComponentDecomposition& operator=(GameMaximalEndComponentDecomposition const& other);
+
+            /*!
+             * Creates an MEC decomposition by moving the contents of the given MEC decomposition.
+             *
+             * @param other The MEC decomposition to move.
+             */
+            GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition&& other);
+
+            /*!
+             * Assigns the contents of the given MEC decomposition to the current one by moving its contents.
+             *
+             * @param other The MEC decomposition from which to move-assign.
+             */
+            GameMaximalEndComponentDecomposition& operator=(GameMaximalEndComponentDecomposition&& other);
+
+        private:
+            /*!
+             * Performs the actual decomposition of the given subsystem in the given model into MECs. As a side-effect
+             * this stores the MECs found in the current decomposition.
+             *
+             * @param transitionMatrix The transition matrix representing the system whose subsystem to decompose into MECs.
+             * @param backwardTransitions The reversed transition relation.
+             * @param states The states of the subsystem to decompose.
+             * @param choices The choices of the subsystem to decompose.
+             */
+            void performGameMaximalEndComponentDecomposition(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> backwardTransitions, storm::storage::BitVector const* states = nullptr, storm::storage::BitVector const* choices = nullptr);
+            void singleMEC(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> backwardTransitions, storm::storage::BitVector const* states = nullptr, storm::storage::BitVector const* choices = nullptr);
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_GAMEMAXIMALENDCOMPONENTDECOMPOSITION_H_ */