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

debug: Sound Game VI now fully debugged (fixed Find_MSEC), WIP: produce scheduler

main
Fabian Russold 1 year ago
committed by sp
parent
621e9f6794
commit
8f187f46f1
4 changed files with 63 additions and 84 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
  2. 50
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
  3. 90
      src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
  4. 6
      src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h

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

@ -154,7 +154,6 @@ namespace storm {
if (checkTask.isProduceSchedulersSet() && ret.scheduler) { if (checkTask.isProduceSchedulersSet() && ret.scheduler) {
result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler)); result->asExplicitQuantitativeCheckResult<ValueType>().setScheduler(std::move(ret.scheduler));
} }
//STORM_LOG_DEBUG(result);
return result; return result;
} }

50
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
View File

@ -61,29 +61,30 @@ namespace storm {
template<typename ValueType> 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) { 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::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; 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); storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
// Initialize the x vector and solution vector result. // 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(); 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; 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>()); 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 // 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(); auto xU_begin = xU.begin();
@ -92,33 +93,32 @@ namespace storm {
if (probGreater0[&it - &(*xU_begin)]) if (probGreater0[&it - &(*xU_begin)])
it = 1; 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]); bool ret = !(relevantStates[i]);
i++; i++;
return ret; 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> 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()); storm::storage::BitVector clippedStatesOfCoalition(relevantStates.getNumberOfSetBits());
clippedStatesOfCoalition.setClippedStatesOfCoalition(relevantStates, statesOfCoalition); 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); 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)); return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
} }

90
src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.cpp
View File

@ -20,7 +20,6 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
void SoundGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) { void SoundGameViHelper<ValueType>::prepareSolversAndMultipliers(const Environment& env) {
STORM_LOG_DEBUG("\n" << _transitionMatrix);
_multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix); _multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, _transitionMatrix);
_x1IsCurrent = false; _x1IsCurrent = false;
_minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition; _minimizerStates = _optimizationDirection == OptimizationDirection::Maximize ? _statesOfCoalition : ~_statesOfCoalition;
@ -39,13 +38,11 @@ namespace storm {
//_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>()); //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
_x1L = xL; _x1L = xL;
_x2L = _x1L; _x2L = _x1L;
_x1Test = _x1L;
_x2Test = _x1L;
_x1U = xU; _x1U = xU;
_x2U = _x1U; _x2U = _x1U;
if (this->isProduceSchedulerSet()) {
if (this->isProduceSchedulerSet()) { // TODO Fabian scheduler !!!
if (!this->_producedOptimalChoices.is_initialized()) { if (!this->_producedOptimalChoices.is_initialized()) {
this->_producedOptimalChoices.emplace(); this->_producedOptimalChoices.emplace();
} }
@ -53,12 +50,19 @@ namespace storm {
} }
uint64_t iter = 0; 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) { while (iter < maxIter) {
performIterationStep(env, dir); performIterationStep(env, dir);
if (checkConvergence(precision)) { 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; break;
} }
if (storm::utility::resources::isTerminate()) { if (storm::utility::resources::isTerminate()) {
@ -69,13 +73,10 @@ namespace storm {
xL = xNewL(); xL = xNewL();
xU = xNewU(); 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. // We will be doing one more iteration step and track scheduler choices this time.
performIterationStep(env, dir, &_producedOptimalChoices.get()); performIterationStep(env, dir, &_producedOptimalChoices.get());
}
} */
} }
template <typename ValueType> template <typename ValueType>
@ -92,21 +93,25 @@ namespace storm {
_multiplier->multiply(env, xOldL(), nullptr, choiceValuesL); _multiplier->multiply(env, xOldL(), nullptr, choiceValuesL);
reduceChoiceValues(choiceValuesL, &reducedMinimizerActions, xNewL()); 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 // over_approximation
std::vector<ValueType> choiceValuesU = std::vector<ValueType>(this->_transitionMatrix.getRowCount(), storm::utility::zero<ValueType>()); std::vector<ValueType> choiceValuesU = std::vector<ValueType>(this->_transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
_multiplier->multiply(env, xOldU(), nullptr, choiceValuesU); _multiplier->multiply(env, xOldU(), nullptr, choiceValuesU);
reduceChoiceValues(choiceValuesU, nullptr, xNewU()); 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 if (reducedMinimizerActions != _oldPolicy) { // new MECs only if Policy changed
start = std::chrono::steady_clock::now(); start = std::chrono::steady_clock::now();
@ -114,21 +119,10 @@ namespace storm {
// restricting the none optimal minimizer choices // restricting the none optimal minimizer choices
_restrictedTransitions = this->_transitionMatrix.restrictRows(reducedMinimizerActions); _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() // find_MSECs()
_MSECs = storm::storage::MaximalEndComponentDecomposition<ValueType>(_restrictedTransitions, _restrictedTransitions.transpose(true)); _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 // reducing the choiceValuesU
size_t i = 0; size_t i = 0;
auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) { auto new_end = std::remove_if(choiceValuesU.begin(), choiceValuesU.end(), [&reducedMinimizerActions, &i](const auto& item) {
@ -137,31 +131,28 @@ namespace storm {
return ret; return ret;
}); });
choiceValuesU.erase(new_end, choiceValuesU.end()); 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; _oldPolicy = reducedMinimizerActions;
// deflating the MSECs // deflating the MSECs
start = std::chrono::steady_clock::now();
deflate(_MSECs, _restrictedTransitions, xNewU(), choiceValuesU); 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> 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) { 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 rowGroupIndices = restrictedMatrix.getRowGroupIndices();
auto choice_begin = choiceValues.begin(); auto choice_begin = choiceValues.begin();
// iterating over all MSECs // iterating over all MSECs
for (auto smec_it : MSEC) { for (auto smec_it : MSEC) {
ValueType bestExit = 0; ValueType bestExit = 0;
if (smec_it.isErgodic(restrictedMatrix)) continue;
// if (smec_it.isErgodic(restrictedMatrix)) continue;
auto stateSet = smec_it.getStateSet(); auto stateSet = smec_it.getStateSet();
for (uint state : stateSet) { for (uint state : stateSet) {
if (_psiStates[state]) {
bestExit = 1;
break;
}
if (_minimizerStates[state]) continue; if (_minimizerStates[state]) continue;
uint rowGroupIndex = rowGroupIndices[state]; uint rowGroupIndex = rowGroupIndices[state];
auto exitingCompare = [&state, &smec_it, &choice_begin](const ValueType &lhs, const ValueType &rhs) 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; uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndex;
auto choice_it = choice_begin + 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) if (newBestExit > bestExit)
bestExit = newBestExit; bestExit = newBestExit;
} }
// deflating the states of the current MSEC // deflating the states of the current MSEC
for (uint state : stateSet) { for (uint state : stateSet) {
if (_psiStates[state]) continue;
xU[state] = std::min(xU[state], bestExit); xU[state] = std::min(xU[state], bestExit);
} }
} }
@ -361,16 +355,6 @@ namespace storm {
return _x1IsCurrent ? _x2U : _x1U; 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>; template class SoundGameViHelper<double>;
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template class SoundGameViHelper<storm::RationalNumber>; template class SoundGameViHelper<storm::RationalNumber>;

6
src/storm/modelchecker/rpatl/helper/internal/SoundGameViHelper.h
View File

@ -97,10 +97,6 @@ namespace storm {
std::vector<ValueType>& xOldU(); std::vector<ValueType>& xOldU();
std::vector<ValueType> const& xOldU() const; std::vector<ValueType> const& xOldU() const;
std::vector<ValueType>& xNewTest();
std::vector<ValueType>& xOldTest();
bool _x1IsCurrent; bool _x1IsCurrent;
storm::storage::BitVector _minimizerStates; storm::storage::BitVector _minimizerStates;
@ -123,7 +119,7 @@ namespace storm {
storm::storage::BitVector _oldPolicy; storm::storage::BitVector _oldPolicy;
storm::storage::BitVector _statesOfCoalition; storm::storage::BitVector _statesOfCoalition;
storm::storage::BitVector _psiStates; 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; OptimizationDirection _optimizationDirection;
storm::storage::MaximalEndComponentDecomposition<ValueType> _MSECs; storm::storage::MaximalEndComponentDecomposition<ValueType> _MSECs;

Write Preview
Loading…
Cancel
Save