diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 36a066da6..080e6bc0a 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -156,7 +156,7 @@ namespace storm { } template - std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative) { + std::vector SparseLTLHelper::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets) { const storm::automata::APSet& apSet = da.getAPSet(); std::vector apLabels; @@ -210,12 +210,12 @@ namespace storm { } if (acceptingStates.empty()) { - STORM_LOG_INFO("No acceptingStates states, skipping probability computation."); + STORM_LOG_INFO("No accepting states, skipping probability computation."); std::vector numericResult(this->_numberOfStates, storm::utility::zero()); return numericResult; } - STORM_LOG_INFO("Computing probabilities for reaching acceptingStates components..."); + STORM_LOG_INFO("Computing probabilities for reaching accepting components..."); storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true); storm::storage::BitVector soiProduct(product->getStatesOfInterest()); @@ -231,6 +231,7 @@ namespace storm { std::vector prodNumericResult; + if (Nondeterministic) { prodNumericResult = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, std::move(solveGoalProduct), @@ -238,7 +239,7 @@ namespace storm { product->getProductModel().getBackwardTransitions(), bvTrue, acceptingStates, - qualitative, + this->isQualitativeSet(), false // no schedulers (at the moment) ).values); @@ -249,7 +250,7 @@ namespace storm { product->getProductModel().getBackwardTransitions(), bvTrue, acceptingStates, - qualitative); + this->isQualitativeSet()); } std::vector numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult); @@ -281,7 +282,7 @@ namespace storm { << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition."); - std::vector numericResult = computeDAProductProbabilities(env, *da, apSatSets, this->isQualitativeSet()); + std::vector numericResult = computeDAProductProbabilities(env, *da, apSatSets); if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) { // compute 1-Pmax[!fomula] diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 29ab7a100..7774daf01 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -50,7 +50,7 @@ namespace storm { * @param a flag indicating whether qualitative model checking is performed * @return a value for each state */ - std::vector computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets, bool qualitative); + std::vector computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map& apSatSets); private: