compute SatSets via LTLHelper

src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -100,40 +100,27 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<SparseCtmcModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
             storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
 
+            STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula);
             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;
-            // TODO simplify APs
-            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);
-            }
 
             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)
+            // 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
+            // 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
+            // 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 ltl probability computations in embedded DTMC...");
 
+            // TODO ?
             if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
                 STORM_LOG_TRACE("Writing model to model.dot");
                 std::ofstream modelDot("model.dot");
@@ -141,11 +128,16 @@ namespace storm {
                 modelDot.close();
             }
 
-            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(embeddedDtmc.getTransitionMatrix(), this->getModel().getNumberOfStates());
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(embeddedDtmc.getTransitionMatrix(), embeddedDtmc.getNumberOfStates());
             storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, embeddedDtmc);
+
+            // Compute Satisfaction sets for APs
+            auto formulaChecker = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) { return this->check(env, *formula); };
+            std::map<std::string, storm::storage::BitVector> apSets = helper.computeApSets(extracted, formulaChecker);
+
             std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
 
-            // we can directly return the numericResult vector as the state space of the CTMC and the embedded DTMC are exactly the same
+            // 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)));
         }
 

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -116,26 +116,10 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<SparseMarkovAutomatonModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
             storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
 
+            STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula);
             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;
-
-            // TODO simplify APs
-            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);
-            }
-
             const SparseMarkovAutomatonModelType& ma = this->getModel();
             typedef typename storm::models::sparse::Mdp<typename SparseMarkovAutomatonModelType::ValueType> SparseMdpModelType;
 
@@ -161,6 +145,11 @@ namespace storm {
 
             storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(embeddedMdp.getTransitionMatrix(), this->getModel().getNumberOfStates());
             storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, embeddedMdp);
+
+            // Compute Satisfaction sets for APs
+            auto formulaChecker = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) { return this->check(env, *formula); };
+            std::map<std::string, storm::storage::BitVector> apSets = helper.computeApSets(extracted, formulaChecker);
+
             std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
 
             // We can directly return the numericResult vector as the state space of the CTMC and the embedded MDP are exactly the same

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

@@ -1,3 +1,5 @@
+#include <modelchecker/results/ExplicitQualitativeCheckResult.h>
+#include <logic/ExtractMaximalStateFormulasVisitor.h>
 #include "SparseLTLHelper.h"
 
 #include "storm/transformer/DAProductBuilder.h"
@@ -259,7 +261,7 @@ namespace storm {
 
 
             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::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;
                 STORM_LOG_THROW((!Nondeterministic) || this->isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
                 if (Nondeterministic && this->getOptimizationDirection() == OptimizationDirection::Minimize) {
@@ -294,6 +296,23 @@ namespace storm {
                 return numericResult;
             }
 
+            template<typename ValueType, bool Nondeterministic>
+            std::map<std::string, storm::storage::BitVector> SparseLTLHelper<ValueType, Nondeterministic>::computeApSets(std::vector<storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair> const& extracted, std::function<std::unique_ptr<CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> formulaChecker){
+                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 = formulaChecker(p.second);
+
+                    ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+                    auto sat = subResult.getTruthValuesVector();
+
+                    apSets[p.first] = std::move(sat);
+                    STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states.");
+                }
+                return apSets;
+            }
+
             template class SparseLTLHelper<double, false>;
             template class SparseLTLHelper<double, true>;
 

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

@@ -4,6 +4,7 @@
 #include "storm/solver/SolveGoal.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
+#include "storm/logic/ExtractMaximalStateFormulasVisitor.h"
 
 
 namespace storm {
@@ -27,6 +28,7 @@ namespace storm {
                 using productModelType = typename std::conditional<Nondeterministic, storm::models::sparse::Mdp<ValueType>, storm::models::sparse::Dtmc<ValueType>>::type;
 
 
+
                 /*!
                  * Initializes the helper for a discrete time model (i.e. DTMC, MDP)
                  * @param the transition matrix of the model
@@ -43,6 +45,16 @@ namespace storm {
                  */
                 std::vector<ValueType> computeLTLProbabilities(Environment const &env, storm::logic::Formula const& formula, std::map<std::string, storm::storage::BitVector>& apSatSets);
 
+                /*!
+                 * todo computes Sat sets of AP
+                 * @param
+                 * @param
+                 * @return
+                 */
+                std::map<std::string, storm::storage::BitVector> computeApSets(std::vector<storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair> const& extracted, std::function<std::unique_ptr<CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> formulaChecker);
+
+
+            private:
                 /*!
                  * Computes the (maximizing) probabilities for the constructed DA product
                  * @param the DA to build the product with
@@ -53,8 +65,6 @@ namespace storm {
                 std::vector<ValueType> computeDAProductProbabilities(Environment const& env, storm::automata::DeterministicAutomaton const& da, std::map<std::string, storm::storage::BitVector>& apSatSets);
 
 
-            private:
-
                 /*!
                  * Compute a set S of states that admit a probability 1 strategy of satisfying the given acceptance condition (in DNF).
                  * More precisely, let

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -146,6 +146,7 @@ namespace storm {
             const SparseDtmcModelType& dtmc = this->getModel();
             storm::solver::SolveGoal<ValueType> goal(dtmc, checkTask);
 
+            // TODO HOA call LTL helper
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeDAProductProbabilities(env, dtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet());
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
@@ -154,24 +155,10 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
             storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
 
+            STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula);
             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);
-            // TODO simplify APs
-            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);
-            }
-
             const SparseDtmcModelType& dtmc = this->getModel();
 
             // TODO ?
@@ -184,6 +171,11 @@ namespace storm {
 
             storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates());
             storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc);
+
+            // Compute Satisfaction sets for APs
+            auto formulaChecker = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) { return this->check(env, *formula); };
+            std::map<std::string, storm::storage::BitVector> apSets = helper.computeApSets(extracted, formulaChecker);
+
             std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
 
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -184,56 +184,13 @@ namespace storm {
 
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
 
+            STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula);
             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;
-            std::map<std::string, std::string> substitution;
-
-            // TODO Maintain a mapping from APsets to labels in order to use the same label for the same formulas
-            std::map<storm::storage::BitVector, std::string> labels;
-
-            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.");
-
-
-                auto occ = labels.find(sat);
-                if(occ != labels.end()){
-                    // Reuse AP
-                    STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is equivalent to " << occ->second << ", substituting...");
-                    substitution[p.first] = occ->second;
-                    continue;
-                }
-                /*// equivalent to !pi
-                occ = labels.find(~sat);
-                if(occ != labels.end()){
-                    // Reuse negated AP
-                    STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is equivalent to !" << occ->second << ", substituting...");
-                    substitution[p.first] =  todo: ! occ->second;
-                    continue;
-                }
-                 */
-
-                labels[sat] = p.first;
-                apSets[p.first] = std::move(sat);
-                STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states.");
-            }
-
-            ltlFormula = ltlFormula->substitute(substitution);
-
             const SparseMdpModelType& mdp = this->getModel();
-
-            // TODO
+            // TODO ?
             if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
                 STORM_LOG_TRACE("Writing model to model.dot");
                 std::ofstream modelDot("model.dot");
@@ -241,8 +198,13 @@ namespace storm {
                 modelDot.close();
             }
 
-            storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(mdp.getTransitionMatrix(), this->getModel().getNumberOfStates());
+            storm::modelchecker::helper::SparseLTLHelper<ValueType, true> helper(mdp.getTransitionMatrix(), mdp.getNumberOfStates());
             storm::modelchecker::helper::setInformationFromCheckTaskNondeterministic(helper, checkTask, mdp);
+
+            // Compute Satisfaction sets for APs
+            auto formulaChecker = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) { return this->check(env, *formula); };
+            std::map<std::string, storm::storage::BitVector> apSets = helper.computeApSets(extracted, formulaChecker);
+
             std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, *ltlFormula, apSets);
 
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));