diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
index 6cd0a5560..9239f0578 100644
--- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
+++ b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
@@ -154,7 +154,6 @@ 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 88f2bd1a2..31dc8cea7 100644
--- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
@@ -61,29 +61,30 @@ namespace storm {
template<typename ValueType>
SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilitiesSound(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
- STORM_LOG_DEBUG("statesOfCoalition: " << statesOfCoalition << std::endl);
- storm::storage::BitVector prob1 = storm::utility::graph::performProb1(backwardTransitions, phiStates, psiStates);
storm::storage::BitVector probGreater0 = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates);
- STORM_LOG_DEBUG("probGreater0: " << probGreater0 << std::endl);
-
-
-
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
- storm::storage::BitVector relevantStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); // TODO Fabian
+ storm::storage::BitVector relevantStates = phiStates;
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
// Initialize the x vector and solution vector result.
- std::vector<ValueType> xL = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
+ std::vector<ValueType> xL = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+ // assigning 1s to the xL vector for all Goal states
auto xL_begin = xL.begin();
- std::for_each(xL.begin(), xL.end(), [&prob1, &xL_begin](ValueType &it)
+ std::for_each(xL.begin(), xL.end(), [&psiStates, &xL_begin](ValueType &it)
{
- if (prob1[&it - &(*xL_begin)])
+ if (psiStates[&it - &(*xL_begin)])
it = 1;
});
- // std::transform(xL.begin(), xL.end(), psiStates.begin(), xL, [](double& a) { a *= 3; }) // TODO Fabian
- // assigning 1s to the xL vector for all Goal states
+ size_t i = 0;
+ auto new_end = std::remove_if(xL.begin(), xL.end(), [&relevantStates, &i](const auto& item) {
+ bool ret = !(relevantStates[i]);
+ i++;
+ return ret;
+ });
+ xL.erase(new_end, xL.end());
+ xL.resize(relevantStates.getNumberOfSetBits());
std::vector<ValueType> xU = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
// assigning 1s to the xU vector for all states except the states s where Prob(sEf) = 0 for all goal states f
auto xU_begin = xU.begin();
@@ -92,33 +93,32 @@ namespace storm {
if (probGreater0[&it - &(*xU_begin)])
it = 1;
});
- /*size_t i = 0;
- auto new_end = std::remove_if(xU.begin(), xU.end(), [&relevantStates, &i](const auto& item) {
+ i = 0;
+ auto new_end_U = std::remove_if(xU.begin(), xU.end(), [&relevantStates, &i](const auto& item) {
bool ret = !(relevantStates[i]);
i++;
return ret;
});
- xU.erase(new_end, xU.end());
- xU.resize(relevantStates.getNumberOfSetBits()); */
+ xU.erase(new_end_U, xU.end());
+ xU.resize(relevantStates.getNumberOfSetBits());
+
+ storm::storage::BitVector clippedPsiStates(relevantStates.getNumberOfSetBits());
+ clippedPsiStates.setClippedStatesOfCoalition(relevantStates, psiStates);
- std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
+ std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
- // STORM_LOG_DEBUG(transitionMatrix);
- STORM_LOG_DEBUG("b: " << b);
storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits());
clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition);
- // std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>()); // TODO Fabian: do I need this?
- std::vector<ValueType> constrainedChoiceValues;
+ std::vector<ValueType> constrainedChoiceValues = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
- storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, backwardTransitions, b, statesOfCoalition, psiStates, goal.direction());
+ storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(submatrix, submatrix.transpose(), b, clippedStatesOfCoalition, clippedPsiStates, goal.direction());
viHelper.performValueIteration(env, xL, xU, goal.direction(), constrainedChoiceValues);
- storm::utility::vector::setVectorValues(result, relevantStates, xU);
- storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
+ viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
+ storm::utility::vector::setVectorValues(result, relevantStates, xL);
- STORM_LOG_DEBUG(xU);
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
}
diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
index 41dc61b50..4cea25c18 100644
--- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
+++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
@@ -20,7 +20,6 @@ namespace storm {
template <typename ValueType>
void SoundGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
- STORM_LOG_DEBUG("\n" << _transitionMatrix);
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
_x1IsCurrent = false;
_minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition;
@@ -39,13 +38,11 @@ namespace storm {
//_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
_x1L = xL;
_x2L = _x1L;
- _x1Test = _x1L;
- _x2Test = _x1L;
_x1U = xU;
_x2U = _x1U;
- if (this->isProduceSchedulerSet()) {
+ if (this->isProduceSchedulerSet()) { // TODO Fabian scheduler !!!
if (!this->_producedOptimalChoices.is_initialized()) {
this->_producedOptimalChoices.emplace();
}
@@ -53,12 +50,19 @@ namespace storm {
}
uint64_t iter = 0;
- constrainedChoiceValues = std::vector<ValueType>(xL.size(), storm::utility::zero<ValueType>()); // ??
+ constrainedChoiceValues = std::vector<ValueType>(xL.size(), storm::utility::zero<ValueType>());
while (iter < maxIter) {
performIterationStep(env, dir);
if (checkConvergence(precision)) {
- //_multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues); // TODO Fabian: ???
+ // one last iteration for shield
+ _multiplier->multiply(env, xNewL(), nullptr, constrainedChoiceValues);
+ storm::storage::BitVector psiStates = _psiStates;
+ auto xL_begin = xNewL().begin();
+ std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it){
+ if (psiStates[&it - &(*xL_begin)])
+ it = 1;
+ });
break;
}
if (storm::utility::resources::isTerminate()) {
@@ -69,13 +73,10 @@ namespace storm {
xL = xNewL();
xU = xNewU();
- // for profiling
- STORM_PRINT(_timing[0] << ", " << _timing[1] << ", " << _timing[2] << ", " << _timing[3] << ", " << _timing[4] << std::endl);
-
- if (isProduceSchedulerSet()) {
+ /* if (isProduceSchedulerSet()) {
// We will be doing one more iteration step and track scheduler choices this time.
performIterationStep(env, dir, &_producedOptimalChoices.get());
- }
+ } */
}
template <typename ValueType>
@@ -92,21 +93,25 @@ namespace storm {
_multiplier->multiply(env, xOldL(), nullptr, choiceValuesL);
reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL());
-
-
- // just for debugging
- _multiplier->multiplyAndReduce(env, _optimizationDirection, xOldTest(), nullptr, xNewTest(), nullptr, &_statesOfCoalition);
+ storm::storage::BitVector psiStates = _psiStates;
+ auto xL_begin = xNewL().begin();
+ std::for_each(xNewL().begin(), xNewL().end(), [&psiStates, &xL_begin](ValueType &it)
+ {
+ if (psiStates[&it - &(*xL_begin)])
+ it = 1;
+ });
// over_approximation
std::vector<ValueType> choiceValuesU = std::vector<ValueType>(this->_transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
_multiplier->multiply(env, xOldU(), nullptr, choiceValuesU);
reduceChoiceValues(choiceValuesU, nullptr, xNewU());
-
- auto finish = std::chrono::steady_clock::now();
- double elapsed_seconds = std::chrono::duration_cast<
- std::chrono::duration<double>>(finish - start).count();
- _timing[0] += elapsed_seconds;
+ auto xU_begin = xNewU().begin();
+ std::for_each(xNewU().begin(), xNewU().end(), [&psiStates, &xU_begin](ValueType &it)
+ {
+ if (psiStates[&it - &(*xU_begin)])
+ it = 1;
+ });
if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed
start = std::chrono::steady_clock::now();
@@ -114,21 +119,10 @@ namespace storm {
// restricting the none optimal minimizer choices
_restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions);
- finish = std::chrono::steady_clock::now();
- elapsed_seconds = std::chrono::duration_cast<std::chrono::duration<double>>(finish - start).count();
- _timing[1] += elapsed_seconds;
-
- // STORM_LOG_DEBUG("restricted Transition: \n" << restrictedTransMatrix);
- start = std::chrono::steady_clock::now();
// find_MSECs()
_MSECs = storm::storage::MaximalEndComponentDecomposition<ValueType>(_restrictedTransitions, _restrictedTransitions.transpose(true));
-
- finish = std::chrono::steady_clock::now();
- elapsed_seconds = std::chrono::duration_cast<std::chrono::duration<double>>(finish - start).count();
- _timing[2] += elapsed_seconds;
}
- start = std::chrono::steady_clock::now();
// reducing the choiceValuesU
size_t i = 0;
auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) {
@@ -137,31 +131,28 @@ namespace storm {
return ret;
});
choiceValuesU.erase(new_end, choiceValuesU.end());
- finish = std::chrono::steady_clock::now();
- elapsed_seconds = std::chrono::duration_cast<
- std::chrono::duration<double>>(finish - start).count();
- _timing[3] += elapsed_seconds;
+
_oldPolicy = reducedMinimizerActions;
// deflating the MSECs
- start = std::chrono::steady_clock::now();
deflate(_MSECs, _restrictedTransitions, xNewU(), choiceValuesU);
- finish = std::chrono::steady_clock::now();
- elapsed_seconds = std::chrono::duration_cast<
- std::chrono::duration<double>>(finish - start).count();
- _timing[4] += elapsed_seconds;
}
template <typename ValueType>
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;
+ // if (smec_it.isErgodic(restrictedMatrix)) continue;
auto stateSet = smec_it.getStateSet();
for (uint state : stateSet) {
+ if (_psiStates[state]) {
+ bestExit = 1;
+ break;
+ }
if (_minimizerStates[state]) continue;
uint rowGroupIndex = rowGroupIndices[state];
auto exitingCompare = [&state, &smec_it, &choice_begin](const ValueType &lhs, const ValueType &rhs)
@@ -176,13 +167,16 @@ namespace storm {
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndex;
auto choice_it = choice_begin + rowGroupIndex;
- ValueType newBestExit = *std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare);
+ auto it = std::max_element(choice_it, choice_it + rowGroupSize, exitingCompare);
+ ValueType newBestExit = 0;
+ if (!smec_it.containsChoice(state, it - choice_begin)) {
+ newBestExit = *it;
+ }
if (newBestExit > bestExit)
bestExit = newBestExit;
}
// deflating the states of the current MSEC
for (uint state : stateSet) {
- if (_psiStates[state]) continue;
xU[state] = std::min(xU[state], bestExit);
}
}
@@ -361,16 +355,6 @@ namespace storm {
return _x1IsCurrent ? _x2U : _x1U;
}
- template <typename ValueType>
- std::vector<ValueType>& SoundGameViHelper<ValueType>::xOldTest() {
- return _x1IsCurrent ? _x2Test : _x1Test;
- }
-
- template <typename ValueType>
- std::vector<ValueType>& SoundGameViHelper<ValueType>::xNewTest() {
- return _x1IsCurrent ? _x1Test : _x2Test;
- }
-
template class SoundGameViHelper<double>;
#ifdef STORM_HAVE_CARL
template class SoundGameViHelper<storm::RationalNumber>;
diff --git a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
index ad78bee56..45d583b7b 100644
--- a/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
+++ b/src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
@@ -97,10 +97,6 @@ namespace storm {
std::vector<ValueType>& xOldU();
std::vector<ValueType> const& xOldU() const;
- std::vector<ValueType>& xNewTest();
-
- std::vector<ValueType>& xOldTest();
-
bool _x1IsCurrent;
storm::storage::BitVector _minimizerStates;
@@ -123,7 +119,7 @@ namespace storm {
storm::storage::BitVector _oldPolicy;
storm::storage::BitVector _statesOfCoalition;
storm::storage::BitVector _psiStates;
- std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U, _x1Test, _x2Test, _b;
+ std::vector<ValueType> _x, _x1L, _x2L, _x1U, _x2U, _b;
OptimizationDirection _optimizationDirection;
storm::storage::MaximalEndComponentDecomposition<ValueType> _MSECs;