sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

smg lra debug commit 

this should be dropped in the future
main
Stefan Pranger 4 years ago
parent
432fef0a45
commit
c6c5c5cc13
8 changed files with 447 additions and 424 deletions
Unified View
  1. 1
      src/storm/builder/ExplicitModelBuilder.cpp
  2. 3
      src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
  3. 71
      src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
  4. 4
      src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
  5. 77
      src/storm/solver/GmmxxMultiplier.cpp
  6. 56
      src/storm/storage/Decomposition.cpp
  7. 66
      src/storm/storage/MaximalEndComponent.cpp
  8. 593
      src/storm/storage/SparseMatrix.cpp

1
src/storm/builder/ExplicitModelBuilder.cpp
View File

@ -161,6 +161,7 @@ namespace storm {
while (!statesToExplore.empty()) { while (!statesToExplore.empty()) {
// Get the first state in the queue. // Get the first state in the queue.
CompressedState currentState = statesToExplore.front().first; CompressedState currentState = statesToExplore.front().first;
STORM_LOG_DEBUG("Exploring (" << currentRowGroup << ") : " << toString(currentState, this->generator->getVariableInformation()));
StateType currentIndex = statesToExplore.front().second; StateType currentIndex = statesToExplore.front().second;
statesToExplore.pop_front(); statesToExplore.pop_front();

3
src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
View File

@ -63,7 +63,10 @@ namespace storm {
this->_backwardTransitions = this->_computedBackwardTransitions.get(); this->_backwardTransitions = this->_computedBackwardTransitions.get();
} }
this->_computedLongRunComponentDecomposition = std::make_unique<storm::storage::GameMaximalEndComponentDecomposition<ValueType>>(this->_transitionMatrix, *this->_backwardTransitions); this->_computedLongRunComponentDecomposition = std::make_unique<storm::storage::GameMaximalEndComponentDecomposition<ValueType>>(this->_transitionMatrix, *this->_backwardTransitions);
this->_longRunComponentDecomposition = this->_computedLongRunComponentDecomposition.get(); this->_longRunComponentDecomposition = this->_computedLongRunComponentDecomposition.get();
//STORM_LOG_DEBUG("\n" << this->_transitionMatrix);
STORM_LOG_DEBUG("GMEC: " << *(this->_longRunComponentDecomposition));
} }
} }

71
src/storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.cpp
View File

@ -24,11 +24,11 @@ namespace storm {
namespace modelchecker { namespace modelchecker {
namespace helper { namespace helper {
namespace internal { namespace internal {
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
LraViHelper<ValueType, ComponentType, TransitionsType>::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector<ValueType> const* exitRates) : _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs), _Tsx1IsCurrent(false) { LraViHelper<ValueType, ComponentType, TransitionsType>::LraViHelper(ComponentType const& component, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, ValueType const& aperiodicFactor, storm::storage::BitVector const* timedStates, std::vector<ValueType> const* exitRates) : _transitionMatrix(transitionMatrix), _timedStates(timedStates), _hasInstantStates(TransitionsType == LraViTransitionsType::DetTsNondetIs || TransitionsType == LraViTransitionsType::DetTsDetIs), _Tsx1IsCurrent(false) {
setComponent(component); setComponent(component);
// Run through the component and collect some data: // Run through the component and collect some data:
// We create two submodels, one consisting of the timed states of the component and one consisting of the instant states of the component. // We create two submodels, one consisting of the timed states of the component and one consisting of the instant states of the component.
// For this, we create a state index map that point from state indices of the input model to indices of the corresponding submodel of that state. // For this, we create a state index map that point from state indices of the input model to indices of the corresponding submodel of that state.
@ -141,8 +141,9 @@ namespace storm {
_IsTransitions = isTransitionsBuilder.build(); _IsTransitions = isTransitionsBuilder.build();
_IsToTsTransitions = isToTsTransitionsBuilder.build(); _IsToTsTransitions = isToTsTransitionsBuilder.build();
} }
STORM_LOG_DEBUG(uniformizationFactor << " - " << _uniformizationRate);
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
void LraViHelper<ValueType, ComponentType, TransitionsType>::setComponent(ComponentType component) { void LraViHelper<ValueType, ComponentType, TransitionsType>::setComponent(ComponentType component) {
_component.clear(); _component.clear();
@ -156,7 +157,7 @@ namespace storm {
} }
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
ValueType LraViHelper<ValueType, ComponentType, TransitionsType>::performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector<ValueType> const* exitRates, storm::solver::OptimizationDirection const* dir, std::vector<uint64_t>* choices) { ValueType LraViHelper<ValueType, ComponentType, TransitionsType>::performValueIteration(Environment const& env, ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector<ValueType> const* exitRates, storm::solver::OptimizationDirection const* dir, std::vector<uint64_t>* choices) {
initializeNewValues(stateValueGetter, actionValueGetter, exitRates); initializeNewValues(stateValueGetter, actionValueGetter, exitRates);
@ -166,7 +167,7 @@ namespace storm {
if (env.solver().lra().isMaximalIterationCountSet()) { if (env.solver().lra().isMaximalIterationCountSet()) {
maxIter = env.solver().lra().getMaximalIterationCount(); maxIter = env.solver().lra().getMaximalIterationCount();
} }
// start the iterations // start the iterations
ValueType result = storm::utility::zero<ValueType>(); ValueType result = storm::utility::zero<ValueType>();
uint64_t iter = 0; uint64_t iter = 0;
@ -198,7 +199,7 @@ namespace storm {
// If there will be a next iteration, we have to prepare it. // If there will be a next iteration, we have to prepare it.
prepareNextIteration(env); prepareNextIteration(env);
} }
if (maxIter.is_initialized() && iter == maxIter.get()) { if (maxIter.is_initialized() && iter == maxIter.get()) {
STORM_LOG_WARN("LRA computation did not converge within " << iter << " iterations."); STORM_LOG_WARN("LRA computation did not converge within " << iter << " iterations.");
@ -207,15 +208,23 @@ namespace storm {
} else { } else {
STORM_LOG_TRACE("LRA computation converged after " << iter << " iterations."); STORM_LOG_TRACE("LRA computation converged after " << iter << " iterations.");
} }
if (choices) { if (choices) {
// We will be doing one more iteration step and track scheduler choices this time. // We will be doing one more iteration step and track scheduler choices this time.
prepareNextIteration(env); prepareNextIteration(env);
performIterationStep(env, dir, choices); performIterationStep(env, dir, choices);
} }
std::cout << "result (" << iter << " steps):" << std::endl;
for(int i = 0; i < xNew().size() ; i++ ) {
std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl;
//if(i == 50) {std::cout << "only showing top 50 lines"; break; }
for(int i = 0; i < xNew().size() ; i++ ) {
std::cout << std::setprecision(4) << i << "\t: " << xNew().at(i) << "\t" << xNew().at(i) * _uniformizationRate << "\t" << std::setprecision(16) << xOld().at(i) *_uniformizationRate << std::endl;
//if(i == 50) {std::cout << "only showing top 50 lines"; break; }
}
return result; return result;
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
void LraViHelper<ValueType, ComponentType, TransitionsType>::initializeNewValues(ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector<ValueType> const* exitRates) { void LraViHelper<ValueType, ComponentType, TransitionsType>::initializeNewValues(ValueGetter const& stateValueGetter, ValueGetter const& actionValueGetter, std::vector<ValueType> const* exitRates) {
// clear potential old values and reserve enough space for new values // clear potential old values and reserve enough space for new values
@ -225,7 +234,7 @@ namespace storm {
_IsChoiceValues.clear(); _IsChoiceValues.clear();
_IsChoiceValues.reserve(_IsTransitions.getRowCount()); _IsChoiceValues.reserve(_IsTransitions.getRowCount());
} }
// Set the new choice-based values // Set the new choice-based values
ValueType actionRewardScalingFactor = storm::utility::one<ValueType>() / _uniformizationRate; ValueType actionRewardScalingFactor = storm::utility::one<ValueType>() / _uniformizationRate;
for (auto const& element : _component) { for (auto const& element : _component) {
@ -250,14 +259,14 @@ namespace storm {
// Set-up new iteration vectors for timed states // Set-up new iteration vectors for timed states
_Tsx1.assign(_TsTransitions.getRowGroupCount(), storm::utility::zero<ValueType>()); _Tsx1.assign(_TsTransitions.getRowGroupCount(), storm::utility::zero<ValueType>());
_Tsx2 = _Tsx1; _Tsx2 = _Tsx1;
if (_hasInstantStates) { if (_hasInstantStates) {
// Set-up vectors for storing intermediate results for instant states. // Set-up vectors for storing intermediate results for instant states.
_Isx.resize(_IsTransitions.getRowGroupCount(), storm::utility::zero<ValueType>()); _Isx.resize(_IsTransitions.getRowGroupCount(), storm::utility::zero<ValueType>());
_Isb = _IsChoiceValues; _Isb = _IsChoiceValues;
} }
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
void LraViHelper<ValueType, ComponentType, TransitionsType>::prepareSolversAndMultipliers(const Environment& env, storm::solver::OptimizationDirection const* dir) { void LraViHelper<ValueType, ComponentType, TransitionsType>::prepareSolversAndMultipliers(const Environment& env, storm::solver::OptimizationDirection const* dir) {
_TsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _TsTransitions); _TsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _TsTransitions);
@ -315,7 +324,7 @@ namespace storm {
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "The solver requirement " << req.getEnabledRequirementsAsString() << " has not been cleared."); STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "The solver requirement " << req.getEnabledRequirementsAsString() << " has not been cleared.");
} }
} }
// Set up multipliers for transitions connecting timed and instant states // Set up multipliers for transitions connecting timed and instant states
_TsToIsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _TsToIsTransitions); _TsToIsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _TsToIsTransitions);
_IsToTsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _IsToTsTransitions); _IsToTsMultiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _IsToTsTransitions);
@ -324,7 +333,7 @@ namespace storm {
_TsMultiplier->setOptimizationDirectionOverride(env.solver().multiplier().getOptimizationDirectionOverride().get()); _TsMultiplier->setOptimizationDirectionOverride(env.solver().multiplier().getOptimizationDirectionOverride().get());
} }
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
void LraViHelper<ValueType, ComponentType, TransitionsType>::setInputModelChoices(std::vector<uint64_t>& choices, std::vector<uint64_t> const& localMecChoices, bool setChoiceZeroToTimedStates, bool setChoiceZeroToInstantStates) const { void LraViHelper<ValueType, ComponentType, TransitionsType>::setInputModelChoices(std::vector<uint64_t>& choices, std::vector<uint64_t> const& localMecChoices, bool setChoiceZeroToTimedStates, bool setChoiceZeroToInstantStates) const {
// Transform the local choices (within this mec) to choice indices for the input model // Transform the local choices (within this mec) to choice indices for the input model
@ -347,7 +356,7 @@ namespace storm {
} }
STORM_LOG_ASSERT(localState == localMecChoices.size(), "Did not traverse all component states."); STORM_LOG_ASSERT(localState == localMecChoices.size(), "Did not traverse all component states.");
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
void LraViHelper<ValueType, ComponentType, TransitionsType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir, std::vector<uint64_t>* choices) { void LraViHelper<ValueType, ComponentType, TransitionsType>::performIterationStep(Environment const& env, storm::solver::OptimizationDirection const* dir, std::vector<uint64_t>* choices) {
STORM_LOG_ASSERT(!((nondetTs() || nondetIs()) && dir == nullptr), "No optimization direction provided for model with nondeterminism"); STORM_LOG_ASSERT(!((nondetTs() || nondetIs()) && dir == nullptr), "No optimization direction provided for model with nondeterminism");
@ -355,13 +364,13 @@ namespace storm {
if (!_TsMultiplier) { if (!_TsMultiplier) {
prepareSolversAndMultipliers(env, dir); prepareSolversAndMultipliers(env, dir);
} }
// Compute new x values for the timed states // Compute new x values for the timed states
// Flip what is new and what is old // Flip what is new and what is old
_Tsx1IsCurrent = !_Tsx1IsCurrent; _Tsx1IsCurrent = !_Tsx1IsCurrent;
// At this point, xOld() points to what has been computed in the most recent call of performIterationStep (initially, this is the 0-vector). // At this point, xOld() points to what has been computed in the most recent call of performIterationStep (initially, this is the 0-vector).
// The result of this ongoing computation will be stored in xNew() // The result of this ongoing computation will be stored in xNew()
// Compute the values obtained by a single uniformization step between timed states only // Compute the values obtained by a single uniformization step between timed states only
if (nondetTs() && !gameNondetTs()) { if (nondetTs() && !gameNondetTs()) {
if (choices == nullptr) { if (choices == nullptr) {
@ -425,7 +434,7 @@ namespace storm {
_TsToIsMultiplier->multiply(env, _Isx, &xNew(), xNew()); _TsToIsMultiplier->multiply(env, _Isx, &xNew(), xNew());
} }
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
typename LraViHelper<ValueType, ComponentType, TransitionsType>::ConvergenceCheckResult LraViHelper<ValueType, ComponentType, TransitionsType>::checkConvergence(bool relative, ValueType precision) const { typename LraViHelper<ValueType, ComponentType, TransitionsType>::ConvergenceCheckResult LraViHelper<ValueType, ComponentType, TransitionsType>::checkConvergence(bool relative, ValueType precision) const {
STORM_LOG_ASSERT(_TsMultiplier, "tried to check for convergence without doing an iteration first."); STORM_LOG_ASSERT(_TsMultiplier, "tried to check for convergence without doing an iteration first.");
@ -433,7 +442,7 @@ namespace storm {
// We need to 'revert' this scaling when computing the absolute precision. // We need to 'revert' this scaling when computing the absolute precision.
// However, for relative precision, the scaling cancels out. // However, for relative precision, the scaling cancels out.
ValueType threshold = relative ? precision : ValueType(precision / _uniformizationRate); ValueType threshold = relative ? precision : ValueType(precision / _uniformizationRate);
ConvergenceCheckResult res = { true, storm::utility::one<ValueType>() }; ConvergenceCheckResult res = { true, storm::utility::one<ValueType>() };
// Now check whether the currently produced results are precise enough // Now check whether the currently produced results are precise enough
STORM_LOG_ASSERT(threshold > storm::utility::zero<ValueType>(), "Did not expect a non-positive threshold."); STORM_LOG_ASSERT(threshold > storm::utility::zero<ValueType>(), "Did not expect a non-positive threshold.");
@ -460,15 +469,15 @@ namespace storm {
break; break;
} }
} }
// Compute the average of the maximal and the minimal difference. // Compute the average of the maximal and the minimal difference.
ValueType avgDiff = (maxDiff + minDiff) / (storm::utility::convertNumber<ValueType>(2.0)); ValueType avgDiff = (maxDiff + minDiff) / (storm::utility::convertNumber<ValueType>(2.0));
// "Undo" the scaling of the values // "Undo" the scaling of the values
res.currentValue = avgDiff * _uniformizationRate; res.currentValue = avgDiff * _uniformizationRate;
return res; return res;
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
void LraViHelper<ValueType, ComponentType, TransitionsType>::prepareNextIteration(Environment const& env) { void LraViHelper<ValueType, ComponentType, TransitionsType>::prepareNextIteration(Environment const& env) {
// To avoid large (and numerically unstable) x-values, we substract a reference value. // To avoid large (and numerically unstable) x-values, we substract a reference value.
@ -480,39 +489,39 @@ namespace storm {
_IsToTsMultiplier->multiply(env, xNew(), &_IsChoiceValues, _Isb); _IsToTsMultiplier->multiply(env, xNew(), &_IsChoiceValues, _Isb);
} }
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
bool LraViHelper<ValueType, ComponentType, TransitionsType>::isTimedState(uint64_t const& inputModelStateIndex) const { bool LraViHelper<ValueType, ComponentType, TransitionsType>::isTimedState(uint64_t const& inputModelStateIndex) const {
STORM_LOG_ASSERT(!_hasInstantStates || _timedStates != nullptr, "Model has instant states but no partition into timed and instant states is given."); STORM_LOG_ASSERT(!_hasInstantStates || _timedStates != nullptr, "Model has instant states but no partition into timed and instant states is given.");
STORM_LOG_ASSERT(!_hasInstantStates || inputModelStateIndex < _timedStates->size(), "Unable to determine whether state " << inputModelStateIndex << " is timed."); STORM_LOG_ASSERT(!_hasInstantStates || inputModelStateIndex < _timedStates->size(), "Unable to determine whether state " << inputModelStateIndex << " is timed.");
return !_hasInstantStates || _timedStates->get(inputModelStateIndex); return !_hasInstantStates || _timedStates->get(inputModelStateIndex);
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
std::vector<ValueType>& LraViHelper<ValueType, ComponentType, TransitionsType>::xNew() { std::vector<ValueType>& LraViHelper<ValueType, ComponentType, TransitionsType>::xNew() {
return _Tsx1IsCurrent ? _Tsx1 : _Tsx2; return _Tsx1IsCurrent ? _Tsx1 : _Tsx2;
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
std::vector<ValueType> const& LraViHelper<ValueType, ComponentType, TransitionsType>::xNew() const { std::vector<ValueType> const& LraViHelper<ValueType, ComponentType, TransitionsType>::xNew() const {
return _Tsx1IsCurrent ? _Tsx1 : _Tsx2; return _Tsx1IsCurrent ? _Tsx1 : _Tsx2;
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
std::vector<ValueType>& LraViHelper<ValueType, ComponentType, TransitionsType>::xOld() { std::vector<ValueType>& LraViHelper<ValueType, ComponentType, TransitionsType>::xOld() {
return _Tsx1IsCurrent ? _Tsx2 : _Tsx1; return _Tsx1IsCurrent ? _Tsx2 : _Tsx1;
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
std::vector<ValueType> const& LraViHelper<ValueType, ComponentType, TransitionsType>::xOld() const { std::vector<ValueType> const& LraViHelper<ValueType, ComponentType, TransitionsType>::xOld() const {
return _Tsx1IsCurrent ? _Tsx2 : _Tsx1; return _Tsx1IsCurrent ? _Tsx2 : _Tsx1;
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
bool LraViHelper<ValueType, ComponentType, TransitionsType>::nondetTs() const { bool LraViHelper<ValueType, ComponentType, TransitionsType>::nondetTs() const {
return TransitionsType == LraViTransitionsType::NondetTsNoIs || gameNondetTs(); return TransitionsType == LraViTransitionsType::NondetTsNoIs || gameNondetTs();
} }
template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType> template <typename ValueType, typename ComponentType, LraViTransitionsType TransitionsType>
bool LraViHelper<ValueType, ComponentType, TransitionsType>::nondetIs() const { bool LraViHelper<ValueType, ComponentType, TransitionsType>::nondetIs() const {
return TransitionsType == LraViTransitionsType::DetTsNondetIs; return TransitionsType == LraViTransitionsType::DetTsNondetIs;
@ -529,11 +538,11 @@ namespace storm {
template class LraViHelper<storm::RationalNumber, storm::storage::MaximalEndComponent, LraViTransitionsType::GameNondetTsNoIs>; template class LraViHelper<storm::RationalNumber, storm::storage::MaximalEndComponent, LraViTransitionsType::GameNondetTsNoIs>;
template class LraViHelper<double, storm::storage::MaximalEndComponent, LraViTransitionsType::DetTsNondetIs>; template class LraViHelper<double, storm::storage::MaximalEndComponent, LraViTransitionsType::DetTsNondetIs>;
template class LraViHelper<storm::RationalNumber, storm::storage::MaximalEndComponent, LraViTransitionsType::DetTsNondetIs>; template class LraViHelper<storm::RationalNumber, storm::storage::MaximalEndComponent, LraViTransitionsType::DetTsNondetIs>;
template class LraViHelper<double, storm::storage::StronglyConnectedComponent, LraViTransitionsType::DetTsNoIs>; template class LraViHelper<double, storm::storage::StronglyConnectedComponent, LraViTransitionsType::DetTsNoIs>;
template class LraViHelper<storm::RationalNumber, storm::storage::StronglyConnectedComponent, LraViTransitionsType::DetTsNoIs>; template class LraViHelper<storm::RationalNumber, storm::storage::StronglyConnectedComponent, LraViTransitionsType::DetTsNoIs>;
} }
} }
} }
} }

4
src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
View File

@ -65,6 +65,7 @@ namespace storm {
Environment solverEnv = env; Environment solverEnv = env;
coalitionIndicator(solverEnv, checkTask); coalitionIndicator(solverEnv, checkTask);
storm::logic::GameFormula const& gameFormula = checkTask.getFormula(); storm::logic::GameFormula const& gameFormula = checkTask.getFormula();
storm::logic::Formula const& subFormula = gameFormula.getSubformula(); storm::logic::Formula const& subFormula = gameFormula.getSubformula();
@ -143,6 +144,8 @@ namespace storm {
playerIds.push_back(boost::get<uint_fast64_t>(player) - 1); playerIds.push_back(boost::get<uint_fast64_t>(player) - 1);
} }
} }
//for(auto const& p : playerActionIndices) std::cout << p.first << " - " << p.second << ", "; std::cout << std::endl;
//for(auto const& p : playerIds) std::cout << p << ", "; std::cout << std::endl;
for(uint i = 0; i < playerActionIndices.size(); i++) { for(uint i = 0; i < playerActionIndices.size(); i++) {
if(std::find(playerIds.begin(), playerIds.end(), playerActionIndices.at(i).second) != playerIds.end()) { if(std::find(playerIds.begin(), playerIds.end(), playerActionIndices.at(i).second) != playerIds.end()) {
@ -151,6 +154,7 @@ namespace storm {
} }
coalitionIndicators.complement(); coalitionIndicators.complement();
//std::cout << "MINMAX OVERRIDE: " << coalitionIndicators << std::endl;
env.solver().multiplier().setOptimizationDirectionOverride(coalitionIndicators); env.solver().multiplier().setOptimizationDirectionOverride(coalitionIndicators);
} }

77
src/storm/solver/GmmxxMultiplier.cpp
View File

@ -16,25 +16,26 @@
namespace storm { namespace storm {
namespace solver { namespace solver {
template<typename ValueType> template<typename ValueType>
GmmxxMultiplier<ValueType>::GmmxxMultiplier(storm::storage::SparseMatrix<ValueType> const& matrix) : Multiplier<ValueType>(matrix) { GmmxxMultiplier<ValueType>::GmmxxMultiplier(storm::storage::SparseMatrix<ValueType> const& matrix) : Multiplier<ValueType>(matrix) {
// Intentionally left empty. // Intentionally left empty.
//STORM_LOG_DEBUG("\n" << matrix);
} }
template<typename ValueType> template<typename ValueType>
void GmmxxMultiplier<ValueType>::initialize() const { void GmmxxMultiplier<ValueType>::initialize() const {
if (gmmMatrix.nrows() == 0) { if (gmmMatrix.nrows() == 0) {
gmmMatrix = std::move(*storm::adapters::GmmxxAdapter<ValueType>().toGmmxxSparseMatrix(this->matrix)); gmmMatrix = std::move(*storm::adapters::GmmxxAdapter<ValueType>().toGmmxxSparseMatrix(this->matrix));
} }
} }
template<typename ValueType> template<typename ValueType>
void GmmxxMultiplier<ValueType>::clearCache() const { void GmmxxMultiplier<ValueType>::clearCache() const {
gmmMatrix = gmm::csr_matrix<ValueType>(); gmmMatrix = gmm::csr_matrix<ValueType>();
Multiplier<ValueType>::clearCache(); Multiplier<ValueType>::clearCache();
} }
template<typename ValueType> template<typename ValueType>
bool GmmxxMultiplier<ValueType>::parallelize(Environment const& env) const { bool GmmxxMultiplier<ValueType>::parallelize(Environment const& env) const {
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
@ -43,7 +44,7 @@ namespace storm {
return false; return false;
#endif #endif
} }
template<typename ValueType> template<typename ValueType>
void GmmxxMultiplier<ValueType>::multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const { void GmmxxMultiplier<ValueType>::multiply(Environment const& env, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result) const {
initialize(); initialize();
@ -65,7 +66,7 @@ namespace storm {
std::swap(result, *this->cachedVector); std::swap(result, *this->cachedVector);
} }
} }
template<typename ValueType> template<typename ValueType>
void GmmxxMultiplier<ValueType>::multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, bool backwards) const { void GmmxxMultiplier<ValueType>::multiplyGaussSeidel(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> const* b, bool backwards) const {
initialize(); initialize();
@ -84,7 +85,7 @@ namespace storm {
} }
} }
} }
template<typename ValueType> template<typename ValueType>
void GmmxxMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const { void GmmxxMultiplier<ValueType>::multiplyAndReduce(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint_fast64_t>* choices) const {
initialize(); initialize();
@ -106,13 +107,13 @@ namespace storm {
std::swap(result, *this->cachedVector); std::swap(result, *this->cachedVector);
} }
} }
template<typename ValueType> template<typename ValueType>
void GmmxxMultiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const { void GmmxxMultiplier<ValueType>::multiplyAndReduceGaussSeidel(Environment const& env, OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType>& x, std::vector<ValueType> const* b, std::vector<uint_fast64_t>* choices, bool backwards) const {
initialize(); initialize();
multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, backwards); multAddReduceHelper(dir, rowGroupIndices, x, b, x, choices, backwards);
} }
template<typename ValueType> template<typename ValueType>
void GmmxxMultiplier<ValueType>::multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const { void GmmxxMultiplier<ValueType>::multiplyRow(uint64_t const& rowIndex, std::vector<ValueType> const& x, ValueType& value) const {
initialize(); initialize();
@ -148,14 +149,14 @@ namespace storm {
} }
} }
} }
template<typename ValueType> template<typename ValueType>
template<typename Compare, bool backwards> template<typename Compare, bool backwards>
void GmmxxMultiplier<ValueType>::multAddReduceHelper(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const { void GmmxxMultiplier<ValueType>::multAddReduceHelper(std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
Compare compare; Compare compare;
typedef std::vector<ValueType> VectorType; typedef std::vector<ValueType> VectorType;
typedef gmm::csr_matrix<ValueType> MatrixType; typedef gmm::csr_matrix<ValueType> MatrixType;
typename gmm::linalg_traits<VectorType>::const_iterator add_it, add_ite; typename gmm::linalg_traits<VectorType>::const_iterator add_it, add_ite;
if (b) { if (b) {
add_it = backwards ? gmm::vect_end(*b) - 1 : gmm::vect_begin(*b); add_it = backwards ? gmm::vect_end(*b) - 1 : gmm::vect_begin(*b);
@ -181,6 +182,7 @@ namespace storm {
uint64_t currentRowGroup = backwards ? rowGroupIndices.size() - 1 : 0; uint64_t currentRowGroup = backwards ? rowGroupIndices.size() - 1 : 0;
auto row_group_it = backwards ? rowGroupIndices.end() - 2 : rowGroupIndices.begin(); auto row_group_it = backwards ? rowGroupIndices.end() - 2 : rowGroupIndices.begin();
auto row_group_ite = backwards ? rowGroupIndices.begin() - 1 : rowGroupIndices.end() - 1; auto row_group_ite = backwards ? rowGroupIndices.begin() - 1 : rowGroupIndices.end() - 1;
//if(choices) STORM_LOG_DEBUG(" ");
while (row_group_it != row_group_ite) { while (row_group_it != row_group_ite) {
ValueType currentValue = storm::utility::zero<ValueType>(); ValueType currentValue = storm::utility::zero<ValueType>();
@ -199,7 +201,7 @@ namespace storm {
oldSelectedChoiceValue = currentValue; oldSelectedChoiceValue = currentValue;
} }
} }
// move row-based iterators to the next row // move row-based iterators to the next row
if (backwards) { if (backwards) {
--itr; --itr;
@ -213,6 +215,10 @@ namespace storm {
// Process the (rowGroupSize-1) remaining rows within the current row Group // Process the (rowGroupSize-1) remaining rows within the current row Group
uint64_t rowGroupSize = *(row_group_it + 1) - *row_group_it; uint64_t rowGroupSize = *(row_group_it + 1) - *row_group_it;
uint choiceforprintout = 0;
//std::cout << currentRowGroup << ": " << currentValue << ", ";
//STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x) << " + " << *add_it << "; ");
//STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x) << " + " << *add_it << "; ");
for (uint64_t i = 1; i < rowGroupSize; ++i) { for (uint64_t i = 1; i < rowGroupSize; ++i) {
ValueType newValue = b ? *add_it : storm::utility::zero<ValueType>(); ValueType newValue = b ? *add_it : storm::utility::zero<ValueType>();
newValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x); newValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x);
@ -220,12 +226,13 @@ namespace storm {
if (choices && currentRow == *choice_it + *row_group_it) { if (choices && currentRow == *choice_it + *row_group_it) {
oldSelectedChoiceValue = newValue; oldSelectedChoiceValue = newValue;
} }
//std::cout << newValue << ", ";
if(this->isOverridden(currentRowGroup) ? !compare(newValue, currentValue) : compare(newValue, currentValue)) { //STORM_LOG_DEBUG(std::setprecision(3) << vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x) << " + " << *add_it << "; ");
currentValue = newValue; currentValue = newValue;
if (choices) { if (choices) {
selectedChoice = currentRow - *row_group_it; selectedChoice = currentRow - *row_group_it;
} }
choiceforprintout = currentRow - *row_group_it;
} }
// move row-based iterators to the next row // move row-based iterators to the next row
if (backwards) { if (backwards) {
@ -238,7 +245,8 @@ namespace storm {
++add_it; ++add_it;
} }
} }
//STORM_LOG_DEBUG("\t= " << currentValue << "\tchoice: " << choiceforprintout);
//std::cout << std::fixed << std::setprecision(2) << " | v(" << currentRowGroup << ")=" << currentValue << " c: " << choiceforprintout << " |\n" ;
// Finally write value to target vector. // Finally write value to target vector.
*target_it = currentValue; *target_it = currentValue;
if(choices) { if(choices) {
@ -261,6 +269,7 @@ namespace storm {
++currentRowGroup; ++currentRowGroup;
} }
} }
//std::cout << std::endl;
} }
template<> template<>
@ -286,7 +295,7 @@ namespace storm {
multAdd(x, b, result); multAdd(x, b, result);
#endif #endif
} }
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
template<typename ValueType, typename Compare> template<typename ValueType, typename Compare>
class TbbMultAddReduceFunctor { class TbbMultAddReduceFunctor {
@ -294,14 +303,14 @@ namespace storm {
TbbMultAddReduceFunctor(std::vector<uint64_t> const& rowGroupIndices, gmm::csr_matrix<ValueType> const& matrix, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices) { TbbMultAddReduceFunctor(std::vector<uint64_t> const& rowGroupIndices, gmm::csr_matrix<ValueType> const& matrix, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) : rowGroupIndices(rowGroupIndices), matrix(matrix), x(x), b(b), result(result), choices(choices) {
// Intentionally left empty. // Intentionally left empty.
} }
void operator()(tbb::blocked_range<unsigned long> const& range) const { void operator()(tbb::blocked_range<unsigned long> const& range) const {
typedef std::vector<ValueType> VectorType; typedef std::vector<ValueType> VectorType;
typedef gmm::csr_matrix<ValueType> MatrixType; typedef gmm::csr_matrix<ValueType> MatrixType;
auto groupIt = rowGroupIndices.begin() + range.begin(); auto groupIt = rowGroupIndices.begin() + range.begin();
auto groupIte = rowGroupIndices.begin() + range.end(); auto groupIte = rowGroupIndices.begin() + range.end();
auto itr = mat_row_const_begin(matrix) + *groupIt; auto itr = mat_row_const_begin(matrix) + *groupIt;
typename std::vector<ValueType>::const_iterator bIt; typename std::vector<ValueType>::const_iterator bIt;
if (b) { if (b) {
@ -311,40 +320,40 @@ namespace storm {
if (choices) { if (choices) {
choiceIt = choices->begin() + range.begin(); choiceIt = choices->begin() + range.begin();
} }
auto resultIt = result.begin() + range.begin(); auto resultIt = result.begin() + range.begin();
// Variables for correctly tracking choices (only update if new choice is strictly better). // Variables for correctly tracking choices (only update if new choice is strictly better).
ValueType oldSelectedChoiceValue; ValueType oldSelectedChoiceValue;
uint64_t selectedChoice; uint64_t selectedChoice;
uint64_t currentRow = *groupIt; uint64_t currentRow = *groupIt;
for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) { for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) {
ValueType currentValue = storm::utility::zero<ValueType>(); ValueType currentValue = storm::utility::zero<ValueType>();
// Only multiply and reduce if the row group is not empty. // Only multiply and reduce if the row group is not empty.
if (*groupIt != *(groupIt + 1)) { if (*groupIt != *(groupIt + 1)) {
if (b) { if (b) {
currentValue = *bIt; currentValue = *bIt;
++bIt; ++bIt;
} }
currentValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x); currentValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x);
if (choices) { if (choices) {
selectedChoice = currentRow - *groupIt; selectedChoice = currentRow - *groupIt;
if (*choiceIt == selectedChoice) { if (*choiceIt == selectedChoice) {
oldSelectedChoiceValue = currentValue; oldSelectedChoiceValue = currentValue;
} }
} }
++itr; ++itr;
++currentRow; ++currentRow;
for (auto itre = mat_row_const_begin(matrix) + *(groupIt + 1); itr != itre; ++itr, ++bIt, ++currentRow) { for (auto itre = mat_row_const_begin(matrix) + *(groupIt + 1); itr != itre; ++itr, ++bIt, ++currentRow) {
ValueType newValue = b ? *bIt : storm::utility::zero<ValueType>(); ValueType newValue = b ? *bIt : storm::utility::zero<ValueType>();
newValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x); newValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x);
if (compare(newValue, currentValue)) { if (compare(newValue, currentValue)) {
currentValue = newValue; currentValue = newValue;
if (choices) { if (choices) {
@ -353,7 +362,7 @@ namespace storm {
} }
} }
} }
// Finally write value to target vector. // Finally write value to target vector.
*resultIt = currentValue; *resultIt = currentValue;
if (choices && compare(currentValue, oldSelectedChoiceValue)) { if (choices && compare(currentValue, oldSelectedChoiceValue)) {
@ -361,7 +370,7 @@ namespace storm {
} }
} }
} }
private: private:
Compare compare; Compare compare;
std::vector<uint64_t> const& rowGroupIndices; std::vector<uint64_t> const& rowGroupIndices;
@ -372,7 +381,7 @@ namespace storm {
std::vector<uint64_t>* choices; std::vector<uint64_t>* choices;
}; };
#endif #endif
template<typename ValueType> template<typename ValueType>
void GmmxxMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const { void GmmxxMultiplier<ValueType>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<ValueType> const& x, std::vector<ValueType> const* b, std::vector<ValueType>& result, std::vector<uint64_t>* choices) const {
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
@ -386,18 +395,18 @@ namespace storm {
multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices); multAddReduceHelper(dir, rowGroupIndices, x, b, result, choices);
#endif #endif
} }
template<> template<>
void GmmxxMultiplier<storm::RationalFunction>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& x, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint64_t>* choices) const { void GmmxxMultiplier<storm::RationalFunction>::multAddReduceParallel(storm::solver::OptimizationDirection const& dir, std::vector<uint64_t> const& rowGroupIndices, std::vector<storm::RationalFunction> const& x, std::vector<storm::RationalFunction> const* b, std::vector<storm::RationalFunction>& result, std::vector<uint64_t>* choices) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This operation is not supported.");
} }
template class GmmxxMultiplier<double>; template class GmmxxMultiplier<double>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class GmmxxMultiplier<storm::RationalNumber>; template class GmmxxMultiplier<storm::RationalNumber>;
template class GmmxxMultiplier<storm::RationalFunction>; template class GmmxxMultiplier<storm::RationalFunction>;
#endif #endif
} }
} }

56
src/storm/storage/Decomposition.cpp
View File

@ -8,84 +8,84 @@
namespace storm { namespace storm {
namespace storage { namespace storage {
template <typename BlockType> template <typename BlockType>
Decomposition<BlockType>::Decomposition() : blocks() { Decomposition<BlockType>::Decomposition() : blocks() {
// Intentionally left empty. // Intentionally left empty.
} }
template <typename BlockType> template <typename BlockType>
Decomposition<BlockType>::Decomposition(Decomposition const& other) : blocks(other.blocks) { Decomposition<BlockType>::Decomposition(Decomposition const& other) : blocks(other.blocks) {
// Intentionally left empty. // Intentionally left empty.
} }
template <typename BlockType> template <typename BlockType>
Decomposition<BlockType>& Decomposition<BlockType>::operator=(Decomposition const& other) { Decomposition<BlockType>& Decomposition<BlockType>::operator=(Decomposition const& other) {
this->blocks = other.blocks; this->blocks = other.blocks;
return *this; return *this;
} }
template <typename BlockType> template <typename BlockType>
Decomposition<BlockType>::Decomposition(Decomposition&& other) : blocks(std::move(other.blocks)) { Decomposition<BlockType>::Decomposition(Decomposition&& other) : blocks(std::move(other.blocks)) {
// Intentionally left empty. // Intentionally left empty.
} }
template <typename BlockType> template <typename BlockType>
Decomposition<BlockType>& Decomposition<BlockType>::operator=(Decomposition&& other) { Decomposition<BlockType>& Decomposition<BlockType>::operator=(Decomposition&& other) {
this->blocks = std::move(other.blocks); this->blocks = std::move(other.blocks);
return *this; return *this;
} }
template <typename BlockType> template <typename BlockType>
std::size_t Decomposition<BlockType>::size() const { std::size_t Decomposition<BlockType>::size() const {
return blocks.size(); return blocks.size();
} }
template <typename BlockType> template <typename BlockType>
bool Decomposition<BlockType>::empty() const { bool Decomposition<BlockType>::empty() const {
return blocks.empty(); return blocks.empty();
} }
template <typename BlockType> template <typename BlockType>
typename Decomposition<BlockType>::iterator Decomposition<BlockType>::begin() { typename Decomposition<BlockType>::iterator Decomposition<BlockType>::begin() {
return blocks.begin(); return blocks.begin();
} }
template <typename BlockType> template <typename BlockType>
typename Decomposition<BlockType>::iterator Decomposition<BlockType>::end() { typename Decomposition<BlockType>::iterator Decomposition<BlockType>::end() {
return blocks.end(); return blocks.end();
} }
template <typename BlockType> template <typename BlockType>
typename Decomposition<BlockType>::const_iterator Decomposition<BlockType>::begin() const { typename Decomposition<BlockType>::const_iterator Decomposition<BlockType>::begin() const {
return blocks.begin(); return blocks.begin();
} }
template <typename BlockType> template <typename BlockType>
typename Decomposition<BlockType>::const_iterator Decomposition<BlockType>::end() const { typename Decomposition<BlockType>::const_iterator Decomposition<BlockType>::end() const {
return blocks.end(); return blocks.end();
} }
template <typename BlockType> template <typename BlockType>
BlockType const& Decomposition<BlockType>::getBlock(uint_fast64_t index) const { BlockType const& Decomposition<BlockType>::getBlock(uint_fast64_t index) const {
return blocks.at(index); return blocks.at(index);
} }
template <typename BlockType> template <typename BlockType>
BlockType& Decomposition<BlockType>::getBlock(uint_fast64_t index) { BlockType& Decomposition<BlockType>::getBlock(uint_fast64_t index) {
return blocks.at(index); return blocks.at(index);
} }
template <typename BlockType> template <typename BlockType>
BlockType const& Decomposition<BlockType>::operator[](uint_fast64_t index) const { BlockType const& Decomposition<BlockType>::operator[](uint_fast64_t index) const {
return blocks[index]; return blocks[index];
} }
template <typename BlockType> template <typename BlockType>
BlockType& Decomposition<BlockType>::operator[](uint_fast64_t index) { BlockType& Decomposition<BlockType>::operator[](uint_fast64_t index) {
return blocks[index]; return blocks[index];
} }
template <typename BlockType> template <typename BlockType>
template <typename ValueType> template <typename ValueType>
storm::storage::SparseMatrix<ValueType> Decomposition<BlockType>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<ValueType> const& matrix) const { storm::storage::SparseMatrix<ValueType> Decomposition<BlockType>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<ValueType> const& matrix) const {
@ -97,49 +97,49 @@ namespace storm {
stateToBlockMap[state] = i; stateToBlockMap[state] = i;
} }
} }
// The resulting sparse matrix will have as many rows/columns as there are blocks in the partition. // The resulting sparse matrix will have as many rows/columns as there are blocks in the partition.
storm::storage::SparseMatrixBuilder<ValueType> dependencyGraphBuilder(this->size(), this->size()); storm::storage::SparseMatrixBuilder<ValueType> dependencyGraphBuilder(this->size(), this->size());
for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < this->size(); ++currentBlockIndex) { for (uint_fast64_t currentBlockIndex = 0; currentBlockIndex < this->size(); ++currentBlockIndex) {
// Get the next block. // Get the next block.
block_type const& block = this->getBlock(currentBlockIndex); block_type const& block = this->getBlock(currentBlockIndex);
// Now, we determine the blocks which are reachable (in one step) from the current block. // Now, we determine the blocks which are reachable (in one step) from the current block.
storm::storage::FlatSet<uint_fast64_t> allTargetBlocks; storm::storage::FlatSet<uint_fast64_t> allTargetBlocks;
for (auto state : block) { for (auto state : block) {
for (auto const& transitionEntry : matrix.getRowGroup(state)) { for (auto const& transitionEntry : matrix.getRowGroup(state)) {
uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.getColumn()]; uint_fast64_t targetBlock = stateToBlockMap[transitionEntry.getColumn()];
// We only need to consider transitions that are actually leaving the SCC. // We only need to consider transitions that are actually leaving the SCC.
if (targetBlock != currentBlockIndex) { if (targetBlock != currentBlockIndex) {
allTargetBlocks.insert(targetBlock); allTargetBlocks.insert(targetBlock);
} }
} }
} }
// Now we can just enumerate all the target blocks and insert the corresponding transitions. // Now we can just enumerate all the target blocks and insert the corresponding transitions.
for (auto const& targetBlock : allTargetBlocks) { for (auto const& targetBlock : allTargetBlocks) {
dependencyGraphBuilder.addNextValue(currentBlockIndex, targetBlock, storm::utility::one<ValueType>()); dependencyGraphBuilder.addNextValue(currentBlockIndex, targetBlock, storm::utility::one<ValueType>());
} }
} }
return dependencyGraphBuilder.build(); return dependencyGraphBuilder.build();
} }
template <typename BlockType> template <typename BlockType>
std::ostream& operator<<(std::ostream& out, Decomposition<BlockType> const& decomposition) { std::ostream& operator<<(std::ostream& out, Decomposition<BlockType> const& decomposition) {
out << "["; out << "[ ";
if (decomposition.size() > 0) { if (decomposition.size() > 0) {
for (uint_fast64_t blockIndex = 0; blockIndex < decomposition.size() - 1; ++blockIndex) { for (uint_fast64_t blockIndex = 0; blockIndex < decomposition.size() - 1; ++blockIndex) {
out << decomposition.blocks[blockIndex] << ", "; out << decomposition.blocks[blockIndex] << ", " << std::endl;
} }
out << decomposition.blocks.back(); out << decomposition.blocks.back();
} }
out << "]"; out << " ]";
return out; return out;
} }
template storm::storage::SparseMatrix<double> Decomposition<StateBlock>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<double> const& matrix) const; template storm::storage::SparseMatrix<double> Decomposition<StateBlock>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<double> const& matrix) const;
template storm::storage::SparseMatrix<float> Decomposition<StateBlock>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<float> const& matrix) const; template storm::storage::SparseMatrix<float> Decomposition<StateBlock>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<float> const& matrix) const;
template class Decomposition<StateBlock>; template class Decomposition<StateBlock>;
@ -149,7 +149,7 @@ namespace storm {
template storm::storage::SparseMatrix<float> Decomposition<StronglyConnectedComponent>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<float> const& matrix) const; template storm::storage::SparseMatrix<float> Decomposition<StronglyConnectedComponent>::extractPartitionDependencyGraph(storm::storage::SparseMatrix<float> const& matrix) const;
template class Decomposition<StronglyConnectedComponent>; template class Decomposition<StronglyConnectedComponent>;
template std::ostream& operator<<(std::ostream& out, Decomposition<StronglyConnectedComponent> const& decomposition); template std::ostream& operator<<(std::ostream& out, Decomposition<StronglyConnectedComponent> const& decomposition);
template class Decomposition<MaximalEndComponent>; template class Decomposition<MaximalEndComponent>;
template std::ostream& operator<<(std::ostream& out, Decomposition<MaximalEndComponent> const& decomposition); template std::ostream& operator<<(std::ostream& out, Decomposition<MaximalEndComponent> const& decomposition);
} // namespace storage } // namespace storage

66
src/storm/storage/MaximalEndComponent.cpp
View File

@ -3,125 +3,125 @@
namespace storm { namespace storm {
namespace storage { namespace storage {
std::ostream& operator<<(std::ostream& out, storm::storage::FlatSet<uint_fast64_t> const& block); std::ostream& operator<<(std::ostream& out, storm::storage::FlatSet<uint_fast64_t> const& block);
MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() { MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() {
// Intentionally left empty. // Intentionally left empty.
} }
MaximalEndComponent::MaximalEndComponent(MaximalEndComponent const& other) : stateToChoicesMapping(other.stateToChoicesMapping) { MaximalEndComponent::MaximalEndComponent(MaximalEndComponent const& other) : stateToChoicesMapping(other.stateToChoicesMapping) {
// Intentionally left empty. // Intentionally left empty.
} }
MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent const& other) { MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent const& other) {
stateToChoicesMapping = other.stateToChoicesMapping; stateToChoicesMapping = other.stateToChoicesMapping;
return *this; return *this;
} }
MaximalEndComponent::MaximalEndComponent(MaximalEndComponent&& other) : stateToChoicesMapping(std::move(other.stateToChoicesMapping)) { MaximalEndComponent::MaximalEndComponent(MaximalEndComponent&& other) : stateToChoicesMapping(std::move(other.stateToChoicesMapping)) {
// Intentionally left empty. // Intentionally left empty.
} }
MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent&& other) { MaximalEndComponent& MaximalEndComponent::operator=(MaximalEndComponent&& other) {
stateToChoicesMapping = std::move(other.stateToChoicesMapping); stateToChoicesMapping = std::move(other.stateToChoicesMapping);
return *this; return *this;
} }
void MaximalEndComponent::addState(uint_fast64_t state, set_type const& choices) { void MaximalEndComponent::addState(uint_fast64_t state, set_type const& choices) {
stateToChoicesMapping[state] = choices; stateToChoicesMapping[state] = choices;
} }
void MaximalEndComponent::addState(uint_fast64_t state, set_type&& choices) { void MaximalEndComponent::addState(uint_fast64_t state, set_type&& choices) {
stateToChoicesMapping.emplace(state, std::move(choices)); stateToChoicesMapping.emplace(state, std::move(choices));
} }
std::size_t MaximalEndComponent::size() const { std::size_t MaximalEndComponent::size() const {
return stateToChoicesMapping.size(); return stateToChoicesMapping.size();
} }
MaximalEndComponent::set_type const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const { MaximalEndComponent::set_type const& MaximalEndComponent::getChoicesForState(uint_fast64_t state) const {
auto stateChoicePair = stateToChoicesMapping.find(state); auto stateChoicePair = stateToChoicesMapping.find(state);
if (stateChoicePair == stateToChoicesMapping.end()) { if (stateChoicePair == stateToChoicesMapping.end()) {
throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC."; throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC.";
} }
return stateChoicePair->second; return stateChoicePair->second;
} }
MaximalEndComponent::set_type& MaximalEndComponent::getChoicesForState(uint_fast64_t state) { MaximalEndComponent::set_type& MaximalEndComponent::getChoicesForState(uint_fast64_t state) {
auto stateChoicePair = stateToChoicesMapping.find(state); auto stateChoicePair = stateToChoicesMapping.find(state);
if (stateChoicePair == stateToChoicesMapping.end()) { if (stateChoicePair == stateToChoicesMapping.end()) {
throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC."; throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::getChoicesForState: cannot retrieve choices for state not contained in MEC.";
} }
return stateChoicePair->second; return stateChoicePair->second;
} }
bool MaximalEndComponent::containsState(uint_fast64_t state) const { bool MaximalEndComponent::containsState(uint_fast64_t state) const {
auto stateChoicePair = stateToChoicesMapping.find(state); auto stateChoicePair = stateToChoicesMapping.find(state);
if (stateChoicePair == stateToChoicesMapping.end()) { if (stateChoicePair == stateToChoicesMapping.end()) {
return false; return false;
} }
return true; return true;
} }
void MaximalEndComponent::removeState(uint_fast64_t state) { void MaximalEndComponent::removeState(uint_fast64_t state) {
auto stateChoicePair = stateToChoicesMapping.find(state); auto stateChoicePair = stateToChoicesMapping.find(state);
if (stateChoicePair == stateToChoicesMapping.end()) { if (stateChoicePair == stateToChoicesMapping.end()) {
throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::removeState: cannot remove state not contained in MEC."; throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::removeState: cannot remove state not contained in MEC.";
} }
stateToChoicesMapping.erase(stateChoicePair); stateToChoicesMapping.erase(stateChoicePair);
} }
bool MaximalEndComponent::containsChoice(uint_fast64_t state, uint_fast64_t choice) const { bool MaximalEndComponent::containsChoice(uint_fast64_t state, uint_fast64_t choice) const {
auto stateChoicePair = stateToChoicesMapping.find(state); auto stateChoicePair = stateToChoicesMapping.find(state);
if (stateChoicePair == stateToChoicesMapping.end()) { if (stateChoicePair == stateToChoicesMapping.end()) {
throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::containsChoice: cannot obtain choices for state not contained in MEC."; throw storm::exceptions::InvalidStateException() << "Invalid call to MaximalEndComponent::containsChoice: cannot obtain choices for state not contained in MEC.";
} }
return stateChoicePair->second.find(choice) != stateChoicePair->second.end(); return stateChoicePair->second.find(choice) != stateChoicePair->second.end();
} }
MaximalEndComponent::set_type MaximalEndComponent::getStateSet() const { MaximalEndComponent::set_type MaximalEndComponent::getStateSet() const {
set_type states; set_type states;
states.reserve(stateToChoicesMapping.size()); states.reserve(stateToChoicesMapping.size());
for (auto const& stateChoicesPair : stateToChoicesMapping) { for (auto const& stateChoicesPair : stateToChoicesMapping) {
states.insert(stateChoicesPair.first); states.insert(stateChoicesPair.first);
} }
return states; return states;
} }
std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component) { std::ostream& operator<<(std::ostream& out, MaximalEndComponent const& component) {
out << "{"; out << "{";
for (auto const& stateChoicesPair : component.stateToChoicesMapping) { for (auto const& stateChoicesPair : component.stateToChoicesMapping) {
out << "{" << stateChoicesPair.first << ", " << stateChoicesPair.second << "}"; out << "(" << stateChoicesPair.first << ", " << stateChoicesPair.second << ")";
} }
out << "}"; out << "}";
return out; return out;
} }
MaximalEndComponent::iterator MaximalEndComponent::begin() { MaximalEndComponent::iterator MaximalEndComponent::begin() {
return stateToChoicesMapping.begin(); return stateToChoicesMapping.begin();
} }
MaximalEndComponent::iterator MaximalEndComponent::end() { MaximalEndComponent::iterator MaximalEndComponent::end() {
return stateToChoicesMapping.end(); return stateToChoicesMapping.end();
} }
MaximalEndComponent::const_iterator MaximalEndComponent::begin() const { MaximalEndComponent::const_iterator MaximalEndComponent::begin() const {
return stateToChoicesMapping.begin(); return stateToChoicesMapping.begin();
} }
MaximalEndComponent::const_iterator MaximalEndComponent::end() const { MaximalEndComponent::const_iterator MaximalEndComponent::end() const {
return stateToChoicesMapping.end(); return stateToChoicesMapping.end();
} }

593
src/storm/storage/SparseMatrix.cpp
File diff suppressed because it is too large
View File

Write Preview
|||||||
100:0
Loading…
Cancel
Save