3 changed files with 392 additions and 1 deletions
-
3src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
-
281src/storm/storage/GameMaximalEndComponentDecomposition.cpp
-
109src/storm/storage/GameMaximalEndComponentDecomposition.h
@ -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
|
||||
|
} |
||||
|
} |
||||
@ -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_ */ |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue