Browse Source
Merge pull request 'Merge SMG LRA MC' (#4) from smg_lra_model_checking into main
Merge pull request 'Merge SMG LRA MC' (#4) from smg_lra_model_checking into main
Reviewed-on: http://git.pranger.xyz/TEMPEST/tempest-devel/pulls/4 WIP w.r.t. debug output, will be fixed in the futuremain
38 changed files with 1728 additions and 942 deletions
-
5CMakeLists.txt
-
164src/storm-parsers/parser/FormulaParserGrammar.cpp
-
68src/storm-parsers/parser/FormulaParserGrammar.h
-
4src/storm-parsers/parser/PrismParser.cpp
-
14src/storm/api/verification.h
-
5src/storm/builder/ExplicitModelBuilder.cpp
-
18src/storm/builder/ExplicitModelBuilder.h
-
20src/storm/environment/solver/MultiplierEnvironment.cpp
-
18src/storm/environment/solver/MultiplierEnvironment.h
-
52src/storm/generator/Choice.cpp
-
16src/storm/generator/Choice.h
-
34src/storm/logic/CloneVisitor.cpp
-
56src/storm/logic/FragmentChecker.cpp
-
224src/storm/logic/FragmentSpecification.cpp
-
38src/storm/logic/FragmentSpecification.h
-
6src/storm/logic/GameFormula.cpp
-
2src/storm/logic/GameFormula.h
-
36src/storm/logic/LiftableTransitionRewardsVisitor.cpp
-
2src/storm/modelchecker/AbstractModelChecker.cpp
-
4src/storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h
-
135src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
-
73src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h
-
120src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
-
9src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h
-
59src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
-
5src/storm/models/sparse/Smg.cpp
-
2src/storm/models/sparse/Smg.h
-
108src/storm/solver/GmmxxMultiplier.cpp
-
40src/storm/solver/Multiplier.cpp
-
56src/storm/solver/Multiplier.h
-
56src/storm/storage/Decomposition.cpp
-
281src/storm/storage/GameMaximalEndComponentDecomposition.cpp
-
109src/storm/storage/GameMaximalEndComponentDecomposition.h
-
66src/storm/storage/MaximalEndComponent.cpp
-
593src/storm/storage/SparseMatrix.cpp
-
164src/storm/storage/jani/JSONExporter.cpp
-
6src/storm/storage/prism/Program.h
-
2src/storm/utility/Engine.cpp
@ -1,23 +1,31 @@ |
|||
#pragma once |
|||
|
|||
#include <boost/optional.hpp> |
|||
|
|||
#include "storm/environment/solver/SolverEnvironment.h" |
|||
#include "storm/solver/SolverSelectionOptions.h" |
|||
|
|||
#include "storm/storage/BitVector.h" |
|||
|
|||
namespace storm { |
|||
|
|||
|
|||
class MultiplierEnvironment { |
|||
public: |
|||
|
|||
|
|||
MultiplierEnvironment(); |
|||
~MultiplierEnvironment(); |
|||
|
|||
|
|||
storm::solver::MultiplierType const& getType() const; |
|||
bool const& isTypeSetFromDefault() const; |
|||
void setType(storm::solver::MultiplierType value, bool isSetFromDefault = false); |
|||
|
|||
|
|||
void setOptimizationDirectionOverride(storm::storage::BitVector optimizationDirectionOverride); |
|||
boost::optional<storm::storage::BitVector> const& getOptimizationDirectionOverride() const; |
|||
|
|||
private: |
|||
storm::solver::MultiplierType type; |
|||
bool typeSetFromDefault; |
|||
|
|||
boost::optional<storm::storage::BitVector> optimizationDirectionOverride = boost::none; |
|||
}; |
|||
} |
|||
|
|||
@ -0,0 +1,135 @@ |
|||
#include "SparseNondeterministicGameInfiniteHorizonHelper.h"
|
|||
|
|||
#include "storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h"
|
|||
|
|||
#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"
|
|||
#include "storm/solver/Multiplier.h"
|
|||
|
|||
#include "storm/utility/solver.h"
|
|||
#include "storm/utility/vector.h"
|
|||
|
|||
#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
|
|||
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
|
|||
|
|||
#include "storm/exceptions/UnmetRequirementException.h"
|
|||
#include "storm/exceptions/InternalException.h"
|
|||
|
|||
namespace storm { |
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
template <typename ValueType> |
|||
SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<std::pair<std::string, uint_fast64_t>> const& player) : SparseInfiniteHorizonHelper<ValueType, true>(transitionMatrix), player(player) { |
|||
// Intentionally left empty.
|
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<uint64_t> const& SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::getProducedOptimalChoices() const { |
|||
STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); |
|||
STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); |
|||
return this->_producedOptimalChoices.get(); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<uint64_t>& SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::getProducedOptimalChoices() { |
|||
STORM_LOG_ASSERT(this->isProduceSchedulerSet(), "Trying to get the produced optimal choices although no scheduler was requested."); |
|||
STORM_LOG_ASSERT(this->_producedOptimalChoices.is_initialized(), "Trying to get the produced optimal choices but none were available. Was there a computation call before?"); |
|||
return this->_producedOptimalChoices.get(); |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
storm::storage::Scheduler<ValueType> SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::extractScheduler() const { |
|||
auto const& optimalChoices = getProducedOptimalChoices(); |
|||
storm::storage::Scheduler<ValueType> scheduler(optimalChoices.size()); |
|||
for (uint64_t state = 0; state < optimalChoices.size(); ++state) { |
|||
scheduler.setChoice(optimalChoices[state], state); |
|||
} |
|||
return scheduler; |
|||
} |
|||
|
|||
|
|||
template <typename ValueType> |
|||
void SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::createDecomposition() { |
|||
// TODO This needs to be changed to return the whole model as one component as long as there is no overwritten version of MaximalEndComponentDecomposition for SMGs.
|
|||
if (this->_longRunComponentDecomposition == nullptr) { |
|||
// The decomposition has not been provided or computed, yet.
|
|||
if (this->_backwardTransitions == nullptr) { |
|||
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::GameMaximalEndComponentDecomposition<ValueType>>(this->_transitionMatrix, *this->_backwardTransitions); |
|||
|
|||
this->_longRunComponentDecomposition = this->_computedLongRunComponentDecomposition.get(); |
|||
//STORM_LOG_DEBUG("\n" << this->_transitionMatrix);
|
|||
STORM_LOG_DEBUG("GMEC: " << *(this->_longRunComponentDecomposition)); |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter) { |
|||
auto underlyingSolverEnvironment = env; |
|||
std::vector<ValueType> componentLraValues; |
|||
createDecomposition(); |
|||
componentLraValues.reserve(this->_longRunComponentDecomposition->size()); |
|||
for (auto const& c : *(this->_longRunComponentDecomposition)) { |
|||
componentLraValues.push_back(computeLraForComponent(underlyingSolverEnvironment, stateValuesGetter, actionValuesGetter, c)); |
|||
} |
|||
return componentLraValues; |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
ValueType SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLraForComponent(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) { |
|||
// Allocate memory for the nondeterministic choices.
|
|||
if (this->isProduceSchedulerSet()) { |
|||
if (!this->_producedOptimalChoices.is_initialized()) { |
|||
this->_producedOptimalChoices.emplace(); |
|||
} |
|||
this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount()); |
|||
} |
|||
|
|||
storm::solver::LraMethod method = env.solver().lra().getNondetLraMethod(); |
|||
if (method == storm::solver::LraMethod::LinearProgramming) { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); |
|||
} else if (method == storm::solver::LraMethod::ValueIteration) { |
|||
return computeLraVi(env, stateRewardsGetter, actionRewardsGetter, component); |
|||
} else { |
|||
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique."); |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
ValueType SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLraVi(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& mec) { |
|||
|
|||
// Collect some parameters of the computation
|
|||
ValueType aperiodicFactor = storm::utility::convertNumber<ValueType>(env.solver().lra().getAperiodicFactor()); |
|||
std::vector<uint64_t>* optimalChoices = nullptr; |
|||
if (this->isProduceSchedulerSet()) { |
|||
optimalChoices = &this->_producedOptimalChoices.get(); |
|||
} |
|||
|
|||
// Now create a helper and perform the algorithm
|
|||
if (this->isContinuousTime()) { |
|||
STORM_LOG_THROW(false, storm::exceptions::InternalException, "We cannot handle continuous time games."); |
|||
} else { |
|||
storm::modelchecker::helper::internal::LraViHelper<ValueType, storm::storage::MaximalEndComponent, storm::modelchecker::helper::internal::LraViTransitionsType::GameNondetTsNoIs> viHelper(mec, this->_transitionMatrix, aperiodicFactor); |
|||
return viHelper.performValueIteration(env, stateRewardsGetter, actionRewardsGetter, nullptr, &this->getOptimizationDirection(), optimalChoices); |
|||
} |
|||
} |
|||
|
|||
template <typename ValueType> |
|||
std::vector<ValueType> SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& componentLraValues) { |
|||
STORM_LOG_THROW(false, storm::exceptions::InternalException, "We do not create compositions for LRA for SMGs, solving a stochastic shortest path problem is not available."); |
|||
} |
|||
|
|||
|
|||
template class SparseNondeterministicGameInfiniteHorizonHelper<double>; |
|||
template class SparseNondeterministicGameInfiniteHorizonHelper<storm::RationalNumber>; |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,73 @@ |
|||
#pragma once |
|||
|
|||
#include "storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace storage { |
|||
template <typename VT> class Scheduler; |
|||
} |
|||
|
|||
namespace modelchecker { |
|||
namespace helper { |
|||
|
|||
/*! |
|||
* Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system with different players choices. |
|||
* @tparam ValueType the type a value can have |
|||
*/ |
|||
template <typename ValueType> |
|||
class SparseNondeterministicGameInfiniteHorizonHelper : public SparseInfiniteHorizonHelper<ValueType, true> { |
|||
|
|||
public: |
|||
|
|||
/*! |
|||
* Function mapping from indices to values |
|||
*/ |
|||
typedef typename SparseInfiniteHorizonHelper<ValueType, true>::ValueGetter ValueGetter; |
|||
|
|||
/*! |
|||
* Initializes the helper for a discrete time model with different players (i.e. SMG) |
|||
*/ |
|||
SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<std::pair<std::string, uint_fast64_t>> const& player); |
|||
|
|||
/*! TODO |
|||
* Computes the long run average value given the provided state and action based rewards |
|||
* @param stateValuesGetter a function returning a value for a given state index |
|||
* @param actionValuesGetter a function returning a value for a given (global) choice index |
|||
* @return a value for each state |
|||
*/ |
|||
std::vector<ValueType> computeLongRunAverageValues(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter) override; |
|||
|
|||
/*! |
|||
* @pre before calling this, a computation call should have been performed during which scheduler production was enabled. |
|||
* @return the produced scheduler of the most recent call. |
|||
*/ |
|||
std::vector<uint64_t> const& getProducedOptimalChoices() const; |
|||
|
|||
/*! |
|||
* @pre before calling this, a computation call should have been performed during which scheduler production was enabled. |
|||
* @return the produced scheduler of the most recent call. |
|||
*/ |
|||
std::vector<uint64_t>& getProducedOptimalChoices(); |
|||
|
|||
/*! |
|||
* @pre before calling this, a computation call should have been performed during which scheduler production was enabled. |
|||
* @return a new scheduler containing optimal choices for each state that yield the long run average values of the most recent call. |
|||
*/ |
|||
storm::storage::Scheduler<ValueType> extractScheduler() const; |
|||
|
|||
ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& component); |
|||
|
|||
ValueType computeLraVi(Environment const& env, ValueGetter const& stateValuesGetter, ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& mec); |
|||
|
|||
void createDecomposition(); |
|||
std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues); |
|||
|
|||
private: |
|||
std::vector<std::pair<std::string, uint_fast64_t>> player; |
|||
}; |
|||
|
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -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_ */ |
|||
593
src/storm/storage/SparseMatrix.cpp
File diff suppressed because it is too large
View File
File diff suppressed because it is too large
View File
Write
Preview
Loading…
Cancel
Save
Reference in new issue