From b75c16297f91efe77d96f6a6fcc054c4931f7084 Mon Sep 17 00:00:00 2001
From: hannah <hannah.mertens@rwth-aachen.de>
Date: Tue, 15 Jun 2021 10:39:49 +0200
Subject: [PATCH] fixed some typos

---
 .../modelchecker/helper/ltl/SparseLTLHelper.cpp     | 13 +++++++------
 src/storm/modelchecker/helper/ltl/SparseLTLHelper.h |  2 +-
 2 files changed, 8 insertions(+), 7 deletions(-)

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<typename ValueType, bool Nondeterministic>
-            std::vector<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) {
+            std::vector<ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets) {
                 const storm::automata::APSet& apSet = da.getAPSet();
 
                 std::vector<storm::storage::BitVector> 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<ValueType> numericResult(this->_numberOfStates, storm::utility::zero<ValueType>());
                     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<ValueType> prodNumericResult;
 
+
                 if (Nondeterministic) {
                     prodNumericResult = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::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<ValueType> numericResult = product->projectToOriginalModel(this->_numberOfStates, prodNumericResult);
@@ -281,7 +282,7 @@ namespace storm {
                                        << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
 
 
-                std::vector<ValueType> numericResult = computeDAProductProbabilities(env, *da, apSatSets, this->isQualitativeSet());
+                std::vector<ValueType> 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<ValueType> computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative);
+                std::vector<ValueType> computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets);
 
 
             private: