documentation and renaming of some methods

Conflicts:
	src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -89,6 +89,60 @@ namespace storm {
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
 
+        template<typename SparseCtmcModelType>
+        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
+            storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
+
+            std::vector<storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair> extracted;
+            std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted);
+
+            STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula);
+
+            std::map<std::string, storm::storage::BitVector> apSets;
+
+            for (auto& p : extracted) {
+                STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "...");
+
+                std::unique_ptr<CheckResult> subResultPointer = this->check(env, *p.second);
+                ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+                auto sat = subResult.getTruthValuesVector();
+
+                STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states.");
+
+                apSets[p.first] = std::move(sat);
+            }
+
+            STORM_LOG_INFO("Resulting LTL path formula: " << *ltlFormula);
+            STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString());
+
+            std::shared_ptr<storm::automata::DeterministicAutomaton> da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula, false);
+
+            STORM_LOG_INFO("Deterministic automaton for LTL formula has "
+                    << da->getNumberOfStates() << " states, "
+                    << da->getAPSet().size() << " atomic propositions and "
+                    << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
+
+            const SparseCtmcModelType& ctmc = this->getModel();
+            typedef typename storm::models::sparse::Dtmc<typename SparseCtmcModelType::ValueType> SparseDtmcModelType;
+
+            STORM_LOG_INFO("Computing embedded DTMC...");
+            // compute probability matrix (embedded DTMC)
+            storm::storage::SparseMatrix<ValueType> probabilityMatrix = storm::modelchecker::helper::SparseCtmcCslHelper::computeProbabilityMatrix(ctmc.getTransitionMatrix(), ctmc.getExitRateVector());
+            // copy of the state labelings of the CTMC
+            storm::models::sparse::StateLabeling labeling(ctmc.getStateLabeling());
+
+            // the embedded DTMC, used for building the product and computing the probabilities in the product
+            SparseDtmcModelType embeddedDtmc(std::move(probabilityMatrix), std::move(labeling));
+            storm::solver::SolveGoal<ValueType> goal(embeddedDtmc, checkTask);
+
+
+            STORM_LOG_INFO("Performing DA product and probability computations in embedded DTMC...");
+            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeDAProductProbabilities(env, embeddedDtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet());
+            // we can directly return the numericResult vector as the state space of the CTMC and the embedded DTMC are exactly the same
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+        }
+
+
         template <typename SparseCtmcModelType>
         std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask<storm::logic::InstantaneousRewardFormula, ValueType> const& checkTask) {
             storm::logic::InstantaneousRewardFormula const& rewardPathFormula = checkTask.getFormula();

src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp

@@ -23,9 +23,8 @@ namespace storm {
             }
 
 
-            // todo only for MDP and change name!
             template <typename ValueType, bool Nondeterministic>
-            storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::computeSurelyAcceptingPmaxStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
+            storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
                 STORM_LOG_INFO("Computing accepting states for acceptance condition " << *acceptance.getAcceptanceExpression());
                 if (acceptance.getAcceptanceExpression()->isTRUE()) {
                     STORM_LOG_INFO(" TRUE -> all states accepting (assumes no deadlock in the model)");
@@ -135,9 +134,8 @@ namespace storm {
                 return acceptingStates;
             }
 
-            // todo only for dtmc and change name!
             template <typename ValueType, bool Nondeterministic>
-            storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::computeAcceptingComponentStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix) {
+            storm::storage::BitVector SparseLTLHelper<ValueType, Nondeterministic>::computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix) {
                 storm::storage::StronglyConnectedComponentDecomposition<ValueType> bottomSccs(transitionMatrix, storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs());
                 //storm::storage::BitVector acceptingStates = storm::storage::BitVector(product->getProductModel().getNumberOfStates());
                 storm::storage::BitVector acceptingStates(transitionMatrix.getRowGroupCount(), false);
@@ -179,7 +177,6 @@ namespace storm {
                 }
 
 
-                // todo change text
                 STORM_LOG_INFO("Building "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC-DA")) +"product with deterministic automaton, starting from " << statesOfInterest.getNumberOfSetBits() << " model states...");
                 storm::transformer::DAProductBuilder productBuilder(da, apLabels);
 
@@ -200,19 +197,15 @@ namespace storm {
                     STORM_LOG_TRACE(str.str());
                 }
 
-                // DTMC: BCC
-                // MDP: computeSurelyAcceptingPmaxStates
+                // Compute accepting states
                 storm::storage::BitVector acceptingStates;
                 if (Nondeterministic) {
-                    STORM_LOG_INFO("Computing accepting end components...");
-                    // todo compute accepting states, same as below
-                    acceptingStates = computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions());
-
+                    STORM_LOG_INFO("Computing MECs and checking for acceptance...");
+                    acceptingStates = computeAcceptingECs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions());
 
                 } else {
                     STORM_LOG_INFO("Computing BSCCs and checking for acceptance...");
-                    // todo compute accepting states, (no btm)
-                    acceptingStates = computeAcceptingComponentStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix());
+                    acceptingStates = computeAcceptingBCCs(*product->getAcceptance(), product->getProductModel().getTransitionMatrix());
 
                 }
 
@@ -227,7 +220,7 @@ namespace storm {
                 storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true);
                 storm::storage::BitVector soiProduct(product->getStatesOfInterest());
 
-                // Create goal for computeUntilProbabilities, compute maximizing probabilities for DA product with MDP
+                // Create goal for computeUntilProbabilities, always compute maximizing probabilities
                 storm::solver::SolveGoal<ValueType> solveGoalProduct;
                 if (this->isValueThresholdSet()) {
                     solveGoalProduct = storm::solver::SolveGoal<ValueType>(OptimizationDirection::Maximize, this->getValueThresholdComparisonType(), this->getValueThresholdValue(), std::move(soiProduct));
@@ -263,6 +256,7 @@ namespace storm {
                 return numericResult;
             }
 
+
             template<typename ValueType, bool Nondeterministic>
             std::vector <ValueType> SparseLTLHelper<ValueType, Nondeterministic>::computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map<std::string, storm::storage::BitVector>& apSatSets) {
                 std::shared_ptr<storm::logic::Formula const> ltlFormula;
@@ -279,7 +273,7 @@ namespace storm {
                 STORM_LOG_INFO("Resulting LTL path formula: " << ltlFormula->toString());
                 STORM_LOG_INFO(" in prefix format: " << ltlFormula->toPrefixString());
 
-                std::shared_ptr<storm::automata::DeterministicAutomaton> da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula);
+                std::shared_ptr<storm::automata::DeterministicAutomaton> da = storm::automata::LTL2DeterministicAutomaton::ltl2da(*ltlFormula, Nondeterministic);
 
                 STORM_LOG_INFO("Deterministic automaton for LTL formula has "
                                        << da->getNumberOfStates() << " states, "
@@ -287,7 +281,6 @@ namespace storm {
                                        << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
 
 
-                // compute Pmax for MDP
                 std::vector<ValueType> numericResult = computeDAProductProbabilities(env, *da, apSatSets, this->isQualitativeSet());
 
                 if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) {
@@ -297,7 +290,6 @@ namespace storm {
                     }
                 }
 
-
                 return numericResult;
             }
 

src/storm/modelchecker/helper/ltl/SparseLTLHelper.h

@@ -12,7 +12,7 @@ namespace storm {
         namespace helper {
 
             /*!
-             * Helper class for todo...
+             * Helper class for LTL model checking
              * @tparam ValueType the type a value can have
              * @tparam Nondeterministic true if there is nondeterminism in the Model (MDP)
              */
@@ -22,47 +22,59 @@ namespace storm {
             public:
 
                 /*!
-                 * The type of the product automaton model // todo
+                 * The type of the product automaton (DTMC or MDP) that is used during the computation.
                  */
                 using productModelType = typename std::conditional<Nondeterministic, storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Dtmc<ValueType>>::type;
 
 
                 /*!
-                 * Initializes the helper for a discrete time (i.e. DTMC, MDP)
+                 * Initializes the helper for a discrete time model (i.e. DTMC, MDP)
+                 * @param the transition matrix of the model
+                 * @param the number of states of the model
                  */
                 SparseLTLHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::size_t numberOfSates);
 
 
                 /*!
-                 * todo
-                 * Computes maximizing(!) probabilties for DA product with MDP
-                 * @return
+                 * Computes the LTL probabilities
+                 * @param the LTL formula
+                 * @param the atomic propositions and satisfaction sets
+                 * @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> computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map<std::string, storm::storage::BitVector>& apSatSets);
 
                 /*!
-                 * Computes the ltl probabilities ...todo
+                 * Computes the (maximizing) probabilities for the constructed DA product
+                 * @param the DA to build the product with
+                 * @param the atomic propositions and satisfaction sets
+                 * @param a flag indicating whether qualitative model checking is performed
                  * @return a value for each state
                  */
-                std::vector<ValueType> computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map<std::string, storm::storage::BitVector>& apSatSets);  //todo was brauchen wir hier aps und ..?
+                std::vector<ValueType> computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative);
 
 
             private:
 
-                /*! todo only relevant for MDP  -  enable_if_t ?
-                 * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance conditon.
+                /*!
+                 * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF).
                  * More precisely, let
                  *   accEC be the set of states that are contained in end components that satisfy the acceptance condition
                  *  and let
                  *   P1acc be the set of states that satisfy Pmax=1[ F accEC ].
                  * This function then computes a set that contains accEC and is contained by P1acc.
                  * However, if the acceptance condition consists of 'true', the whole state space can be returned.
+                 * @param the acceptance condition (in DNF)
+                 * @param the transition matrix of the model
+                 * @param the reversed transition relation
                  */
-                static storm::storage::BitVector computeSurelyAcceptingPmaxStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
+                static storm::storage::BitVector computeAcceptingECs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
 
-                //todo only for dtmc, different to mdp: no backward tm
-                static storm::storage::BitVector computeAcceptingComponentStates(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
+                /**
+                * Compute a set S of states that are contained in BSCCs that satisfy the given acceptance conditon.
+                * @tparam the acceptance condition
+                * @tparam the transition matrix of the model
+                */
+                static storm::storage::BitVector computeAcceptingBCCs(automata::AcceptanceCondition const& acceptance, storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
 
 
                 storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -176,7 +176,6 @@ namespace storm {
 
             const SparseDtmcModelType& dtmc = this->getModel();
 
-            // TODO
             if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
                 STORM_LOG_TRACE("Writing model to model.dot");
                 std::ofstream modelDot("model.dot");