Browse Source

Added a comment why this computeBoundedGlobally check happens.

tempestpy_adaptions
Lukas Posch 3 years ago
committed by Stefan Pranger
parent
commit
fb84fc6af0
  1. 1
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

1
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

@ -218,6 +218,7 @@ namespace storm {
storm::utility::vector::setVectorValues(result, relevantStates, x); storm::utility::vector::setVectorValues(result, relevantStates, x);
} }
// In bounded-globally formulas we not only to reach a psiState on the path but also want to stay in a set of psiStates in the given step bounds.
if(!computeBoundedGlobally){ if(!computeBoundedGlobally){
storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>()); storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
} }

Loading…
Cancel
Save