Browse Source

fixed typo

tempestpy_adaptions
Lukas Posch 4 years ago
parent
commit
50087994f7
  1. 2
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

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

@ -72,7 +72,7 @@ namespace storm {
}
template<typename ValueType>
MDPSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::v(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
MDPSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeGloballyProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
// the idea is to implement the definition of globally as in the formula:
// G phi = not(F(not psi)) = not(true U (not psi))
// so the psiStates are flipped, then the true U part is calculated, at the end the result is flipped again

Loading…
Cancel
Save