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

optimization: WIP relevant states for game VI

main
Fabian Russold 5 months ago
committed by sp
parent
26094b08ce
commit
621e9f6794
1 changed files with 38 additions and 18 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 56
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

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

@ -22,8 +22,7 @@ namespace storm {
// Relevant states are those states which are phiStates and not PsiStates.
storm::storage::BitVector relevantStates = phiStates & ~psiStates;
// Initialize the x vector and solution vector result.
// Initialize the x vector and solution vector result.
std::vector<ValueType> x = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
@ -62,44 +61,65 @@ 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);
storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, goal.direction());
std::unique_ptr<storm::storage::Scheduler<ValueType>> scheduler;
storm::storage::BitVector relevantStates(psiStates.size(), true);
storm::storage::BitVector relevantStates = storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true); // TODO Fabian
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, relevantStates, relevantStates, false);
// Initialize the x vector and solution vector result.
// TODO Fabian: maybe relevant states (later)
std::vector<ValueType> xL = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> xL = std::vector<ValueType>(relevantStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
auto xL_begin = xL.begin();
std::for_each(xL.begin(), xL.end(), [&prob1, &xL_begin](ValueType &it)
{
if (prob1[&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
assert(xL.size() == psiStates.size());
for (size_t i = 0; i < xL.size(); i++)
{
if (psiStates[i])
xL[i] = 1;
}
STORM_LOG_DEBUG("xL " << xL);
std::vector<ValueType> xU = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
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());
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);
/*size_t i = 0;
auto new_end = 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()); */
std::vector<ValueType> result = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, psiStates);
// 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;
storm::modelchecker::helper::internal::SoundGameViHelper<ValueType> viHelper(transitionMatrix, backwardTransitions, b, statesOfCoalition, psiStates, 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>());
STORM_LOG_DEBUG(xU);
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(xU), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
return SMGSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(relevantStates), std::move(scheduler), std::move(constrainedChoiceValues));
}
template<typename ValueType>

Write Preview
Loading…
Cancel
Save