From 986d1183aa91485f0d3aa592177b51aa289a48d4 Mon Sep 17 00:00:00 2001
From: Fabian Russold <fabian.russold@student.tugraz.at>
Date: Fri, 9 Aug 2024 11:04:18 +0200
Subject: [PATCH] bug fixes and optimizations
---
.../rpatl/SparseSmgRpatlModelChecker.cpp | 2 +
.../rpatl/helper/SparseSmgRpatlHelper.cpp | 16 ++--
.../helper/internal/SoundGameViHelper.cpp | 91 ++++++++++++-------
.../rpatl/helper/internal/SoundGameViHelper.h | 5 +-
src/storm/storage/MaximalEndComponent.cpp | 16 +++-
src/storm/storage/MaximalEndComponent.h | 11 +++
6 files changed, 96 insertions(+), 45 deletions(-)
diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
index cb110be26..30001ce75 100644
--- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
+++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
@@ -142,6 +142,7 @@ namespace storm {
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeUntilProbabilitiesSound(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint());
+ STORM_LOG_DEBUG(ret.values);
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
if(checkTask.isShieldingTask()) {
storm::storage::BitVector allStatesBv = storm::storage::BitVector(this->getModel().getTransitionMatrix().getRowGroupCount(), true);
@@ -151,6 +152,7 @@ namespace storm {
if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
}
+ //STORM_LOG_DEBUG(result);
return result;
}
diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
index 566120827..e3dc2d8ee 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
@@ -83,11 +83,13 @@ namespace storm {
storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates);
// assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f
assert(xU.size() == probGreater0.size());
- for (size_t i = 0; i < xL.size(); i++) // TODO Fabian: do this more efficient
- {
- if (probGreater0[i])
- xU[i] = 1;
- }
+ auto xU_begin = xU.begin();
+ std::for_each(xU.begin(), xU.end(), [&probGreater0, &xU_begin](ValueType &it)
+ {
+ if (probGreater0[&it - &(*xU_begin)])
+ it = 1;
+ });
+
STORM_LOG_DEBUG("xU " << xU);
std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
@@ -95,9 +97,9 @@ namespace storm {
std::vector<ValueType> constrainedChoiceValues;
viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues);
- return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(xU), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
- assert(false);
+ STORM_LOG_DEBUG(xU);
+ return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(xU), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
}
template<typename ValueType>
diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
index 5a7109cac..732127ce9 100644
--- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
@@ -84,62 +84,82 @@ namespace storm {
prepareSolversAndMultipliers(env);
}
_x1IsCurrent = !_x1IsCurrent;
+ std::vector<ValueType> choiceValuesL = std::vector<ValueType>(this->_transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
- std::vector<ValueType> choiceValues = xNewL();
- choiceValues.resize(this->_transitionMatrix.getRowCount());
-
- _multiplier->multiply(env, xOldL(), nullptr, choiceValues);
- reduceChoiceValues(choiceValues, &reducedMinimizerActions);
- xNewL() = choiceValues;
+ _multiplier->multiply(env, xOldL(), nullptr, choiceValuesL);
+ reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL());
// over_approximation
- _multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition);
+ std::vector<ValueType> choiceValuesU = std::vector<ValueType>(this->_transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
+
+ _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU);
+ reduceChoiceValues(choiceValuesU, nullptr, xNewU());
+
+ //_multiplier->multiplyAndReduce(env, dir, xOldU(), nullptr, xNewU(), nullptr, &_statesOfCoalition);
// restricting the none optimal minimizer choices
storage::SparseMatrix<ValueType> restrictedTransMatrix = this->_transitionMatrix.restrictRows(reducedMinimizerActions);
- _multiplierRestricted = storm::solver::MultiplierFactory<ValueType>().create(env, restrictedTransMatrix);
// STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix);
- // find_MSECs() & deflate()
+ // find_MSECs()
storm::storage::MaximalEndComponentDecomposition<ValueType> MSEC = storm::storage::MaximalEndComponentDecomposition<ValueType>(restrictedTransMatrix, _backwardTransitions);
- // STORM_LOG_DEBUG("MECD: \n" << MECD);
- deflate(MSEC,restrictedTransMatrix, xNewU());
+ // STORM_LOG_DEBUG("MECD: \n" << MSEC);
+
+ // reducing the choiceValuesU
+ size_t i = 0;
+ auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) {
+ bool ret = !(reducedMinimizerActions[i]);
+ i++;
+ return ret;
+ });
+ choiceValuesU.erase(new_end, choiceValuesU.end());
+
+ // deflating the MSECs
+ deflate(MSEC, restrictedTransMatrix, xNewU(), choiceValuesU);
}
template <typename ValueType>
- void SoundGameViHelper<ValueType>::deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MSEC, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU) {
+ void SoundGameViHelper<ValueType>::deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MSEC, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU, std::vector<ValueType> choiceValues) {
auto rowGroupIndices = restrictedMatrix.getRowGroupIndices();
+ auto choice_begin = choiceValues.begin();
// iterating over all MSECs
for (auto smec_it : MSEC) {
ValueType bestExit = 0;
+ if (smec_it.isErgodic(restrictedMatrix)) continue; // TODO Fabian: ?? isErgodic undefined ref
auto stateSet = smec_it.getStateSet();
for (uint state : stateSet) {
- uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
- if (!_minimizerStates[state]) { // check if current state is maximizer state
- for (uint choice = 0; choice < rowGroupSize; choice++) {
- if (!smec_it.containsChoice(state, choice + rowGroupIndices[state])) {
- ValueType choiceValue = 0;
- _multiplierRestricted->multiplyRow(choice + rowGroupIndices[state], xU, choiceValue);
- if (choiceValue > bestExit)
- bestExit = choiceValue;
- }
- }
- }
+ if (_minimizerStates[state]) continue;
+ uint rowGroupIndex = rowGroupIndices[state];
+ auto exitingCompare = [&state, &smec_it, &choice_begin](const ValueType &lhs, const ValueType &rhs)
+ {
+ bool lhsExiting = !smec_it.containsChoice(state, (&lhs - &(*choice_begin)));
+ bool rhsExiting = !smec_it.containsChoice(state, (&rhs - &(*choice_begin)));
+ if( lhsExiting && !rhsExiting) return false;
+ if(!lhsExiting && rhsExiting) return true;
+ if(!lhsExiting && !rhsExiting) return false;
+ return lhs < rhs;
+ };
+ uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndex;
+
+ auto choice_it = choice_begin + rowGroupIndex;
+ ValueType newBestExit = *std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare);
+ if (newBestExit > bestExit)
+ bestExit = newBestExit;
}
// deflating the states of the current MSEC
for (uint state : stateSet) {
- if (!_psiStates[state])
- xU[state] = std::min(xU[state], bestExit);
+ if (_psiStates[state]) continue;
+ xU[state] = std::min(xU[state], bestExit);
}
}
}
template <typename ValueType>
- void SoundGameViHelper<ValueType>::reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result)
+ void SoundGameViHelper<ValueType>::reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result, std::vector<ValueType>& x)
{
// result BitVec should be initialized with 1s outside the method
@@ -153,23 +173,26 @@ namespace storm {
// getting the optimal minimizer choice for the given state
optChoice = *std::min_element(choice_it, choice_it + rowGroupSize);
- for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
- if (*choice_it > optChoice) {
- result->set(rowGroupIndices[state] + choice, 0);
+ if (result != nullptr) {
+ for (uint choice = 0; choice < rowGroupSize; choice++, choice_it++) {
+ if (*choice_it > optChoice) {
+ result->set(rowGroupIndices[state] + choice, 0);
+ }
}
}
- // reducing the xNew() (choiceValues) vector for minimizer states
- choiceValues[state] = optChoice;
+ else
+ choice_it += rowGroupSize;
+ // reducing the xNew() vector for minimizer states
+ x[state] = optChoice;
}
else
{
optChoice = *std::max_element(choice_it, choice_it + rowGroupSize);
- // reducing the xNew() (choiceValues) vector for maximizer states
- choiceValues[state] = optChoice;
+ // reducing the xNew() vector for maximizer states
+ x[state] = optChoice;
choice_it += rowGroupSize;
}
}
- choiceValues.resize(this->_transitionMatrix.getRowGroupCount());
}
diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
index 5fecd8d87..f738958ca 100644
--- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
+++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
@@ -74,9 +74,9 @@ namespace storm {
*/
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
- void deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU);
+ void deflate(storm::storage::MaximalEndComponentDecomposition<ValueType> const MECD, storage::SparseMatrix<ValueType> const restrictedMatrix, std::vector<ValueType>& xU, std::vector<ValueType> choiceValues);
- void reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result);
+ void reduceChoiceValues(std::vector<ValueType>& choiceValues, storm::storage::BitVector* result, std::vector<ValueType>& x);
/*!
* Checks whether the curently computed value achieves the desired precision
@@ -117,7 +117,6 @@ namespace storm {
storm::storage::BitVector _psiStates;
std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U;
std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplier;
- std::unique_ptr<storm::solver::Multiplier<ValueType>> _multiplierRestricted;
OptimizationDirection _optimizationDirection;
bool _produceScheduler = false;
diff --git a/src/storm/storage/MaximalEndComponent.cpp b/src/storm/storage/MaximalEndComponent.cpp
index aa7453277..d4f51e089 100644
--- a/src/storm/storage/MaximalEndComponent.cpp
+++ b/src/storm/storage/MaximalEndComponent.cpp
@@ -4,7 +4,6 @@
namespace storm {
namespace storage {
-
std::ostream& operator<<(std::ostream& out, storm::storage::FlatSet<uint_fast64_t> const& block);
MaximalEndComponent::MaximalEndComponent() : stateToChoicesMapping() {
@@ -100,6 +99,18 @@ namespace storm {
return stateChoicePair->second.find(choice) != stateChoicePair->second.end();
}
+ template<typename ValueType>
+ bool MaximalEndComponent::isErgodic(storm::storage::SparseMatrix<ValueType> transitionMatrix) const {
+ auto rowGroupIndices = transitionMatrix.getRowGroupIndices();
+ for (auto state : this->getStateSet())
+ {
+ if (getChoicesForState(state).size() == (rowGroupIndices[state + 1] - rowGroupIndices[state])) continue;
+ return false;
+ }
+ return true;
+ }
+
+
MaximalEndComponent::set_type MaximalEndComponent::getStateSet() const {
set_type states;
states.reserve(stateToChoicesMapping.size());
@@ -136,5 +147,8 @@ namespace storm {
MaximalEndComponent::const_iterator MaximalEndComponent::end() const {
return stateToChoicesMapping.end();
}
+
+ template bool MaximalEndComponent::isErgodic<double>(storm::storage::SparseMatrix<double> transitionMatrix) const;
+ template bool MaximalEndComponent::isErgodic<storm::RationalNumber>(storm::storage::SparseMatrix<storm::RationalNumber> transitionMatrix) const;
}
}
diff --git a/src/storm/storage/MaximalEndComponent.h b/src/storm/storage/MaximalEndComponent.h
index a1d5b37c2..66c1d1c4a 100644
--- a/src/storm/storage/MaximalEndComponent.h
+++ b/src/storm/storage/MaximalEndComponent.h
@@ -5,6 +5,7 @@
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/BoostTypes.h"
+#include "storm/storage/SparseMatrix.h"
namespace storm {
namespace storage {
@@ -20,6 +21,7 @@ namespace storm {
typedef std::unordered_map<uint_fast64_t, set_type> map_type;
typedef map_type::iterator iterator;
typedef map_type::const_iterator const_iterator;
+
/*!
* Creates an empty MEC.
@@ -124,6 +126,15 @@ namespace storm {
* @return True if the given choice is contained in the MEC.
*/
bool containsChoice(uint_fast64_t state, uint_fast64_t choice) const;
+
+ /*!
+ * Retrieves wether the MEC is ergodic or not i.e. wether the MEC is exitable or not
+ *
+ * @param transitionMatrix the given transition matrix
+ * @return True if the MEC is ergodic
+ */
+ template<typename ValueType>
+ bool isErgodic(storm::storage::SparseMatrix<ValueType> transitionMatrix) const;
/*!
* Retrieves the set of states contained in the MEC.