Started to restructure LTL model checking algorithms

Conflicts:
	src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

src/storm/modelchecker/helper/SingleValueModelCheckerHelper.cpp

@@ -82,6 +82,16 @@ namespace storm {
             bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isProduceSchedulerSet() const {
                 return _produceScheduler;
             }
+
+            template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
+            void SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::setQualitative(bool value) {
+                _isQualitativeSet = value;
+            }
+
+            template <typename ValueType, storm::models::ModelRepresentation ModelRepresentation>
+            bool SingleValueModelCheckerHelper<ValueType, ModelRepresentation>::isQualitativeSet() const {
+                return _isQualitativeSet;
+            }
  
             template class SingleValueModelCheckerHelper<double, storm::models::ModelRepresentation::Sparse>;
             template class SingleValueModelCheckerHelper<storm::RationalNumber, storm::models::ModelRepresentation::Sparse>;

src/storm/modelchecker/helper/SingleValueModelCheckerHelper.h

@@ -100,11 +100,22 @@ namespace storm {
                  * @return whether an optimal scheduler shall be constructed during the computation
                  */
                 bool isProduceSchedulerSet() const;
+
+                /*!
+                * Sets whether the property needs to be checked qualitatively
+                */
+                void setQualitative(bool value);
+
+                /*!
+                 * @return whether the property needs to be checked qualitatively
+                 */
+                bool isQualitativeSet() const;
                 
             private:
                 boost::optional<storm::solver::OptimizationDirection> _optimizationDirection;
                 boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> _valueThreshold;
                 bool _produceScheduler;
+                bool _isQualitativeSet;
             };
         }
     }

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

@@ -0,0 +1,192 @@
+#include "SparseLTLHelper.h"
+
+#include "storm/transformer/DAProductBuilder.h"
+#include "storm/automata/LTL2DeterministicAutomaton.h"
+
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/Mdp.h"
+
+#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
+#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
+
+#include "storm/storage/StronglyConnectedComponentDecomposition.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/DebugSettings.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+
+            template <typename ValueType, typename Model, bool Nondeterministic>
+            SparseLTLHelper<ValueType, Model, Nondeterministic>::SparseLTLHelper(Model const& model, storm::storage::SparseMatrix<ValueType> const& transitionMatrix) : _model(model), _transitionMatrix(transitionMatrix) {
+                // Intentionally left empty.
+            }
+
+            template<typename ValueType, typename Model, bool Nondeterministic>
+            std::vector<ValueType> SparseLTLHelper<ValueType, Model, Nondeterministic>::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) {
+                STORM_LOG_THROW((!Nondeterministic) || goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP");
+
+
+                const storm::automata::APSet& apSet = da.getAPSet();
+
+                std::vector<storm::storage::BitVector> apLabels;
+                for (const std::string& ap : apSet.getAPs()) {
+                    auto it = apSatSets.find(ap);
+                    STORM_LOG_THROW(it != apSatSets.end(), storm::exceptions::InvalidOperationException, "Deterministic automaton has AP " << ap << ", does not appear in formula");
+
+                    apLabels.push_back(std::move(it->second));
+                }
+
+                storm::storage::BitVector statesOfInterest;
+                if (goal.hasRelevantValues()) {
+                    statesOfInterest = goal.relevantValues();
+                } else {
+                    // product from all model states
+                    statesOfInterest = storm::storage::BitVector(this->_model.getNumberOfStates(), true);
+                }
+
+
+                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);
+
+                auto product = productBuilder.build(this->_model, statesOfInterest);
+
+                STORM_LOG_INFO("Product "+ (Nondeterministic ? std::string("MDP-DA") : std::string("DTMC")) +" has " << product->getProductModel().getNumberOfStates() << " states and "
+                                                   << product->getProductModel().getNumberOfTransitions() << " transitions.");
+
+                if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
+                    STORM_LOG_TRACE("Writing model to model.dot");
+                    std::ofstream modelDot("model.dot");
+                    this->_model.writeDotToStream(modelDot);
+                    modelDot.close();
+
+                    STORM_LOG_TRACE("Writing product model to product.dot");
+                    std::ofstream productDot("product.dot");
+                    product->getProductModel().writeDotToStream(productDot);
+                    productDot.close();
+
+                    STORM_LOG_TRACE("Product model mapping:");
+                    std::stringstream str;
+                    product->printMapping(str);
+                    STORM_LOG_TRACE(str.str());
+                }
+
+
+                // DTMC: BCC
+                // MDP: computeSurelyAcceptingPmaxStates
+                storm::storage::BitVector accepting;
+                if (Nondeterministic) {
+                    STORM_LOG_INFO("Computing accepting end components...");
+                    accepting = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeSurelyAcceptingPmaxStates(*product->getAcceptance(), product->getProductModel().getTransitionMatrix(), product->getProductModel().getBackwardTransitions());
+                    if (accepting.empty()) {
+                        STORM_LOG_INFO("No accepting states, skipping probability computation.");
+                        std::vector<ValueType> numericResult(this->_model.getNumberOfStates(), storm::utility::zero<ValueType>());
+                        return numericResult;
+                    }
+
+                } else {
+                    STORM_LOG_INFO("Computing BSCCs and checking for acceptance...");
+
+                    storm::storage::StronglyConnectedComponentDecomposition<ValueType> bottomSccs(product->getProductModel().getTransitionMatrix(),
+                                                                                                  storage::StronglyConnectedComponentDecompositionOptions().onlyBottomSccs().dropNaiveSccs());
+                    accepting = storm::storage::BitVector(product->getProductModel().getNumberOfStates());
+                    std::size_t checkedBSCCs = 0, acceptingBSCCs = 0, acceptingBSCCStates = 0;
+                    for (auto& scc : bottomSccs) {
+                        checkedBSCCs++;
+                        if (product->getAcceptance()->isAccepting(scc)) {
+                            acceptingBSCCs++;
+                            for (auto& state : scc) {
+                                accepting.set(state);
+                                acceptingBSCCStates++;
+                            }
+                        }
+                    }
+
+                    STORM_LOG_INFO("BSCC analysis: " << acceptingBSCCs << " of " << checkedBSCCs << " BSCCs were accepting (" << acceptingBSCCStates << " states in accepting BSCCs).");
+
+                    if (acceptingBSCCs == 0) {
+                        STORM_LOG_INFO("No accepting BSCCs, skipping probability computation.");
+                        std::vector<ValueType> numericResult(this->_model.getNumberOfStates(), storm::utility::zero<ValueType>());
+                        return numericResult;
+                    }
+                }
+
+                STORM_LOG_INFO("Computing probabilities for reaching accepting BSCCs...");
+
+                storm::storage::BitVector bvTrue(product->getProductModel().getNumberOfStates(), true);
+
+                storm::solver::SolveGoal<ValueType> solveGoalProduct(goal);
+                storm::storage::BitVector soiProduct(product->getStatesOfInterest());
+                solveGoalProduct.setRelevantValues(std::move(soiProduct));
+
+                std::vector<ValueType> prodNumericResult;
+
+                if (Nondeterministic) {
+                    prodNumericResult
+                            = std::move(storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(env,
+                                                                                                                                std::move(solveGoalProduct),
+                                                                                                                                product->getProductModel().getTransitionMatrix(),
+                                                                                                                                product->getProductModel().getBackwardTransitions(),
+                                                                                                                                bvTrue,
+                                                                                                                                accepting,
+                                                                                                                                qualitative,
+                                                                                                                                false  // no schedulers (at the moment)
+                                                                                                                                ).values);
+
+                } else {
+                    prodNumericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeUntilProbabilities(env,
+                                                                                                                   std::move(solveGoalProduct),
+                                                                                                                   product->getProductModel().getTransitionMatrix(),
+                                                                                                                   product->getProductModel().getBackwardTransitions(),
+                                                                                                                   bvTrue,
+                                                                                                                   accepting,
+                                                                                                                   qualitative);
+                    }
+
+                std::vector<ValueType> numericResult = product->projectToOriginalModel(this->_model, prodNumericResult);
+                return numericResult;
+            }
+
+
+            template<typename ValueType, typename RewardModelType, bool Nondeterministic>
+            std::vector <ValueType> SparseLTLHelper<ValueType, RewardModelType, Nondeterministic>::computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal<ValueType>&& goal, storm::logic::Formula const& ltlFormula, std::map<std::string, storm::storage::BitVector>& apSatSets) {
+                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);
+
+                STORM_LOG_INFO("Deterministic automaton for LTL formula has "
+                                       << da->getNumberOfStates() << " states, "
+                                       << da->getAPSet().size() << " atomic propositions and "
+                                       << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
+
+
+                std::vector<ValueType> numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSatSets, this->isQualitativeSet());
+
+                /*
+                if(Nondeterministic && this->getOptimizationDirection()==OptimizationDirection::Minimize) {
+                    // compute 1-Pmax[!ltl]
+                    for (auto& value : numericResult) {
+                        value = storm::utility::one<ValueType>() - value;
+                    }
+                }
+                */
+
+                return numericResult;
+            }
+
+            template class SparseLTLHelper<double, storm::models::sparse::Dtmc<double>, false>;
+            template class SparseLTLHelper<double, storm::models::sparse::Mdp<double>, true>;
+
+#ifdef STORM_HAVE_CARL
+            template class SparseLTLHelper<storm::RationalNumber, storm::models::sparse::Dtmc<storm::RationalNumber>, false>;
+            template class SparseLTLHelper<storm::RationalNumber, storm::models::sparse::Mdp<storm::RationalNumber>, true>;
+            template class SparseLTLHelper<storm::RationalFunction,  storm::models::sparse::Dtmc<storm::RationalFunction>, false>;
+
+#endif
+
+        }
+    }
+}

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

@@ -0,0 +1,52 @@
+#include "storm/modelchecker/helper/SingleValueModelCheckerHelper.h"
+#include "storm/storage/SparseMatrix.h"
+#include "storm/solver/SolveGoal.h"
+
+
+namespace storm {
+
+    namespace automata {
+        // fwd
+        class DeterministicAutomaton;
+    }
+
+    namespace modelchecker {
+        namespace helper {
+
+            /*!
+             * Helper class for todo...
+             * @tparam ValueType the type a value can have
+             * @tparam Nondeterministic true if there is nondeterminism in the Model (MDP)
+             */
+            template<typename ValueType, typename Model,  bool Nondeterministic> // todo remove Model
+            class SparseLTLHelper: public SingleValueModelCheckerHelper<ValueType, storm::models::ModelRepresentation::Sparse> {
+
+            public:
+                /*!
+                 * Initializes the helper for a discrete time (i.e. DTMC, MDP)
+                 */
+                SparseLTLHelper(Model const& model, storm::storage::SparseMatrix<ValueType> const& transitionMatrix);
+
+
+                /*!
+                 * todo
+                 * @return
+                 */
+                std::vector<ValueType> computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative);
+
+
+                /*!
+                 * Computes the ltl probabilities ...todo
+                 * @return a value for each state
+                 */
+                std::vector<ValueType> computeLTLProbabilities(Environment const &env, storm::solver::SolveGoal<ValueType>&& goal, storm::logic::Formula const& f, std::map<std::string, storm::storage::BitVector>& apSatSets);  //todo was brauchen wir hier aps und ..?
+
+
+            private:
+                storm::storage::SparseMatrix<ValueType> const& _transitionMatrix;
+                Model const& _model; // todo remove ?
+
+            };
+        }
+    }
+}

src/storm/modelchecker/helper/utility/SetInformationFromCheckTask.h

@@ -25,6 +25,9 @@ namespace storm {
                 }
                 // Scheduler Production
 			    helper.setProduceScheduler(checkTask.isProduceSchedulersSet());
+
+                // Qualitative flag
+                helper.setQualitative(checkTask.isQualitativeSet());
             }
             
             /*!
@@ -40,6 +43,10 @@ namespace storm {
 			    if (checkTask.isBoundSet()) {
 			        helper.setValueThreshold(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
 			    }
+
+			    // Qualitative flag
+			    helper.setQualitative(checkTask.isQualitativeSet());
+
             }
         }
     }

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -15,6 +15,7 @@
 #include "storm/modelchecker/csl/helper/SparseCtmcCslHelper.h"
 #include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h"
 #include "storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.h"
+#include "storm/modelchecker/helper/ltl/SparseLTLHelper.h"
 #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h"
 
 #include "storm/logic/FragmentSpecification.h"
@@ -161,7 +162,7 @@ namespace storm {
             STORM_LOG_INFO("Extracting maximal state formulas and computing satisfaction sets for path formula: " << pathFormula);
 
             std::map<std::string, storm::storage::BitVector> apSets;
-
+            // todo instead: std::map<std::string, storm::storage::BitVector> apSets =  storm::modelchecker::helper::computeApSets(env, checkTask);
             for (auto& p : extracted) {
                 STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "...");
 
@@ -174,20 +175,12 @@ namespace storm {
                 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);
-
-            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 SparseDtmcModelType& dtmc = this->getModel();
-            storm::solver::SolveGoal<ValueType> goal(dtmc, checkTask);
 
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeDAProductProbabilities(env, dtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet());
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, SparseDtmcModelType, false> helper(dtmc, dtmc.getTransitionMatrix());
+            storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc);
+            std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), *ltlFormula, apSets);
+
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
 
@@ -256,14 +249,13 @@ namespace storm {
 
         template<typename SparseDtmcModelType>
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask) {
-
             storm::logic::StateFormula const& stateFormula = checkTask.getFormula();
-			std::unique_ptr<CheckResult> subResultPointer = this->check(env, stateFormula);
-			ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+			      std::unique_ptr<CheckResult> subResultPointer = this->check(env, stateFormula);
+			      ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
 
-			storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper<ValueType> helper(this->getModel().getTransitionMatrix());
+			      storm::modelchecker::helper::SparseDeterministicInfiniteHorizonHelper<ValueType> helper(this->getModel().getTransitionMatrix());
             storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
-			auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector());
+			      auto values = helper.computeLongRunAverageProbabilities(env, subResult.getTruthValuesVector());
 
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(values)));
         }

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -23,6 +23,7 @@
 #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
 #include "storm/modelchecker/helper/infinitehorizon/SparseNondeterministicInfiniteHorizonHelper.h"
 #include "storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.h"
+#include "storm/modelchecker/helper/ltl/SparseLTLHelper.h"
 #include "storm/modelchecker/helper/utility/SetInformationFromCheckTask.h"
 
 #include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h"
@@ -189,7 +190,6 @@ namespace storm {
             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 << "...");
 
@@ -216,31 +216,25 @@ namespace storm {
                 subTask = checkTask.substituteFormula(*ltlFormula);
             }
 
-            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);
-
-            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 SparseMdpModelType& mdp = this->getModel();
             storm::solver::SolveGoal<ValueType> goal(mdp, subTask);
 
-            std::vector<ValueType> numericResult = computeDAProductProbabilities(env, std::move(goal), *da, apSets, checkTask.isQualitativeSet());
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, SparseMdpModelType, true> helper(mdp, mdp.getTransitionMatrix());
+            storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, subTask, mdp);
+            std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), subTask), *ltlFormula, apSets);
 
-            if (minimize) {
+            if(minimize) {
                 // compute 1-Pmax[!ltl]
                 for (auto& value : numericResult) {
                     value = storm::utility::one<ValueType>() - value;
                 }
             }
+
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
 
 
+        /*
         template<typename SparseMdpModelType>
         std::vector<typename SparseMdpPrctlModelChecker<SparseMdpModelType>::ValueType> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal<typename SparseMdpPrctlModelChecker<SparseMdpModelType>::ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) const {
             STORM_LOG_THROW(goal.hasDirection() && goal.direction() == OptimizationDirection::Maximize, storm::exceptions::InvalidPropertyException, "Can only compute maximizing probabilties for DA product with MDP");
@@ -318,6 +312,7 @@ namespace storm {
             std::vector<ValueType> numericResult = product->projectToOriginalModel(this->getModel(), prodNumericResult);
             return numericResult;
         }
+        */
 
 
         template<typename SparseMdpModelType>

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@@ -46,7 +46,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> checkQuantileFormula(Environment const& env, CheckTask<storm::logic::QuantileFormula, ValueType> const& checkTask) override;
             
         private:
-            std::vector<ValueType> computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) const;
+            //std::vector<ValueType> computeDAProductProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets, bool qualitative) const;
         };
     } // namespace modelchecker
 } // namespace storm