diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp index d48211af6..d4f52f65c 100644 --- a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp +++ b/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>(this->_transitionMatrix.transpose(true)); this->_backwardTransitions = this->_computedBackwardTransitions.get(); } - this->_computedLongRunComponentDecomposition = std::make_unique>(this->_transitionMatrix, *this->_backwardTransitions); + this->_computedLongRunComponentDecomposition = std::make_unique>(this->_transitionMatrix, *this->_backwardTransitions); this->_longRunComponentDecomposition = this->_computedLongRunComponentDecomposition.get(); } } diff --git a/src/storm/storage/GameMaximalEndComponentDecomposition.cpp b/src/storm/storage/GameMaximalEndComponentDecomposition.cpp new file mode 100644 index 000000000..f82933b6e --- /dev/null +++ b/src/storm/storage/GameMaximalEndComponentDecomposition.cpp @@ -0,0 +1,281 @@ +#include +#include +#include + +#include "storm/models/sparse/StandardRewardModel.h" + +#include "storm/storage/GameMaximalEndComponentDecomposition.h" +#include "storm/storage/StronglyConnectedComponentDecomposition.h" + +namespace storm { + namespace storage { + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition() : Decomposition() { + // Intentionally left empty. + } + + template + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model) { + singleMEC(model.getTransitionMatrix(), model.getBackwardTransitions()); + //performGameMaximalEndComponentDecomposition(model.getTransitionMatrix(), model.getBackwardTransitions()); + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions) { + singleMEC(transitionMatrix, backwardTransitions); + //performGameMaximalEndComponentDecomposition(transitionMatrix, backwardTransitions); + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& states) { + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& states, storm::storage::BitVector const& choices) { + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& states) { + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition const& other) : Decomposition(other) { + // Intentionally left empty. + } + + template + GameMaximalEndComponentDecomposition& GameMaximalEndComponentDecomposition::operator=(GameMaximalEndComponentDecomposition const& other) { + Decomposition::operator=(other); + return *this; + } + + template + GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(GameMaximalEndComponentDecomposition&& other) : Decomposition(std::move(other)) { + // Intentionally left empty. + } + + template + GameMaximalEndComponentDecomposition& GameMaximalEndComponentDecomposition::operator=(GameMaximalEndComponentDecomposition&& other) { + Decomposition::operator=(std::move(other)); + return *this; + } + + template + void GameMaximalEndComponentDecomposition::performGameMaximalEndComponentDecomposition(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix 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 const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + + // Initialize the maximal end component list to be the full state space. + std::list endComponentStateSets; + if (states) { + endComponentStateSets.emplace_back(states->begin(), states->end(), true); + } else { + std::vector 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::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 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::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 + void GameMaximalEndComponentDecomposition::singleMEC(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix backwardTransitions, storm::storage::BitVector const* states, storm::storage::BitVector const* choices) { + MaximalEndComponent singleMec; + + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + + std::list endComponentStateSets; + std::vector 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; + template GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); + +#ifdef STORM_HAVE_CARL + template class GameMaximalEndComponentDecomposition; + template GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); + + template class GameMaximalEndComponentDecomposition; + template GameMaximalEndComponentDecomposition::GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel const& model); +#endif + } +} diff --git a/src/storm/storage/GameMaximalEndComponentDecomposition.h b/src/storm/storage/GameMaximalEndComponentDecomposition.h new file mode 100644 index 000000000..36c590426 --- /dev/null +++ b/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 + class GameMaximalEndComponentDecomposition : public Decomposition { + public: + /* + * Creates an empty MEC decomposition. + */ + GameMaximalEndComponentDecomposition(); + + /* + * Creates an MEC decomposition of the given model. + * + * @param model The model to decompose into MECs. + */ + template > + GameMaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel 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 const& transitionMatrix, storm::storage::SparseMatrix 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 const& transitionMatrix, storm::storage::SparseMatrix 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 const& transitionMatrix, storm::storage::SparseMatrix 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 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 const& transitionMatrix, storm::storage::SparseMatrix backwardTransitions, storm::storage::BitVector const* states = nullptr, storm::storage::BitVector const* choices = nullptr); + void singleMEC(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix backwardTransitions, storm::storage::BitVector const* states = nullptr, storm::storage::BitVector const* choices = nullptr); + }; + } +} + +#endif /* STORM_STORAGE_GAMEMAXIMALENDCOMPONENTDECOMPOSITION_H_ */