channged data structure for extracted formulas

src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp

@@ -7,11 +7,11 @@
 namespace storm {
     namespace logic {
 
-        ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(FormulaLabelMapping& extractedFormulas) : extractedFormulas(extractedFormulas), nestingLevel(0) {
+        ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(ApToFormulaMap& extractedFormulas, std::map<std::string, std::string>& cachedFormulas) : extractedFormulas(extractedFormulas), cachedFormulas(cachedFormulas), nestingLevel(0) {
         }
 
-        std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, FormulaLabelMapping& extractedFormulas) {
-            ExtractMaximalStateFormulasVisitor visitor(extractedFormulas);
+        std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, ApToFormulaMap& extractedFormulas, std::map<std::string, std::string>& cachedFormulas) {
+            ExtractMaximalStateFormulasVisitor visitor(extractedFormulas, cachedFormulas);
             boost::any result = f.accept(visitor, boost::any());
             return boost::any_cast<std::shared_ptr<Formula>>(result);
         }
@@ -152,16 +152,20 @@ namespace storm {
         std::shared_ptr<Formula> ExtractMaximalStateFormulasVisitor::extract(std::shared_ptr<Formula> f) const {
             // TODO can be optimized
             std::string label;
-            auto it = extractedFormulas.find(f->toString());
-            if (it != extractedFormulas.end()){
+
+            // Find equivalent formula in cache
+            auto it = cachedFormulas.find(f->toString());
+            if (it != cachedFormulas.end()){
                 // Reuse label of equivalent formula
-                label = it->second.first;
+                label = it->second;
             } else {
                 // Create new label
                 label = "p" + std::to_string(extractedFormulas.size());
+                extractedFormulas[label] = f;
+                // Update cache
+                cachedFormulas[f->toString()] = label;
             }
 
-            extractedFormulas[f->toString()] = LabelFormulaPair(label, f);
             return std::make_shared<storm::logic::AtomicLabelFormula>(label);
         }
 

src/storm/logic/ExtractMaximalStateFormulasVisitor.h

@@ -9,12 +9,9 @@ namespace storm {
 
         class ExtractMaximalStateFormulasVisitor : public CloneVisitor {
         public:
-            typedef std::pair<std::string, std::shared_ptr<Formula const>> LabelFormulaPair;
+            typedef std::map<std::string, std::shared_ptr<Formula const>> ApToFormulaMap;
 
-            // Maintain a mapping from formula-strings to formula-label pairs in order to use the same label for the equivalent formulas (as strings)
-            typedef std::map<std::string, LabelFormulaPair> FormulaLabelMapping;
-
-            static std::shared_ptr<Formula> extract(PathFormula const& f, FormulaLabelMapping& extractedFormulas);
+            static std::shared_ptr<Formula> extract(PathFormula const& f, ApToFormulaMap& extractedFormulas, std::map<std::string, std::string>& cachedFormulas);
 
             virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@@ -31,13 +28,15 @@ namespace storm {
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
 
         private:
-            ExtractMaximalStateFormulasVisitor(FormulaLabelMapping& extractedFormulas);
+            ExtractMaximalStateFormulasVisitor(ApToFormulaMap& extractedFormulas, std::map<std::string, std::string>& cachedFormulas);
 
             std::shared_ptr<Formula> extract(std::shared_ptr<Formula> f) const;
             void incrementNestingLevel() const;
             void decrementNestingLevel() const;
 
-            FormulaLabelMapping& extractedFormulas;
+            ApToFormulaMap& extractedFormulas;
+            // A mapping from formula-strings to labels in order to use the same label for the equivalent formulas (as strings)
+            std::map<std::string, std::string>& cachedFormulas;
             std::size_t nestingLevel;
         };
 

src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -101,10 +101,10 @@ namespace storm {
             storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
 
             STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula);
-
-            // Maintain a mapping from formula-strings to pairs in order to reuse labels of equivalent (compared as strings) formulas
-            std::map<std::string, storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair> extracted;
-            std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted);
+            storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted;
+            // Maintain a mapping from formula-strings to labels in order to reuse labels of equivalent (compared as strings) formulas
+            std::map<std::string, std::string> cached;
+            std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached);
 
 
             const SparseCtmcModelType& ctmc = this->getModel();

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -117,15 +117,14 @@ namespace storm {
             storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
 
             STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula);
-
-            // Maintain a mapping from formula-strings to pairs in order to reuse labels of equivalent (compared as strings) formulas
-            std::map<std::string, storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair> extracted;
-            std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted);
+            storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted;
+            // Maintain a mapping from formula-strings to labels in order to reuse labels of equivalent (compared as strings) formulas
+            std::map<std::string, std::string> cached;
+            std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached);
 
             const SparseMarkovAutomatonModelType& ma = this->getModel();
             typedef typename storm::models::sparse::Mdp<typename SparseMarkovAutomatonModelType::ValueType> SparseMdpModelType;
 
-            // TODO correct?
             STORM_LOG_INFO("Computing embedded MDP...");
             storm::storage::SparseMatrix<ValueType> probabilityMatrix = ma.getTransitionMatrix();
             // Copy of the state labelings of the MDP

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

@@ -309,19 +309,18 @@ namespace storm {
             }
 
             template<typename ValueType, bool Nondeterministic>
-            std::map<std::string, storm::storage::BitVector> SparseLTLHelper<ValueType, Nondeterministic>::computeApSets(std::map<std::string, 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> SparseLTLHelper<ValueType, Nondeterministic>::computeApSets(std::map<std::string, std::shared_ptr<storm::logic::Formula const>> 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& it: extracted) {
-                    storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair pair = it.second;
-                    STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << pair.first << "\" <=> " << *pair.second << "...");
+                for (auto& p: extracted) {
+                    STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "...");
 
-                    std::unique_ptr<CheckResult> subResultPointer = formulaChecker(pair.second);
+                    std::unique_ptr<CheckResult> subResultPointer = formulaChecker(p.second);
 
                     ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
                     auto sat = subResult.getTruthValuesVector();
 
-                    apSets[pair.first] = std::move(sat);
-                    STORM_LOG_INFO(" Atomic proposition \"" << pair.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states.");
+                    apSets[p.first] = std::move(sat);
+                    STORM_LOG_INFO(" Atomic proposition \"" << p.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states.");
                 }
                 return apSets;
             }

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

@@ -49,7 +49,7 @@ namespace storm {
                  * @param
                  * @return
                  */
-                std::map<std::string, storm::storage::BitVector> computeApSets(std::map<std::string, 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> computeApSets(std::map<std::string, std::shared_ptr<storm::logic::Formula const>> const& extracted, std::function<std::unique_ptr<CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula)> formulaChecker);
 
 
             private:

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -132,6 +132,7 @@ namespace storm {
                     << da->getAPSet().size() << " atomic propositions and "
                     << *da->getAcceptance()->getAcceptanceExpression() << " as acceptance condition.");
 
+            // TODO move computation of apSets to SparseLTLHelper (extracted: AP to formula - std::map<std::string, std::shared_ptr<Formula const>>)
             std::map<std::string, storm::storage::BitVector> apSets;
             for (std::string const& ap : apSet.getAPs()) {
                 std::shared_ptr<storm::logic::Formula const> expression = pathFormula.getAPMapping().at(ap);
@@ -148,6 +149,15 @@ namespace storm {
 
             // TODO HOA call LTL helper
             std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeDAProductProbabilities(env, dtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet());
+            // storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(dtmc.getTransitionMatrix(), this->getModel().getNumberOfStates());
+            // storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, dtmc);
+
+            // Compute Satisfaction sets for APs (see above)
+            // auto formulaChecker = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) {return this->check(*formula); };
+            // std::map<std::string, storm::storage::BitVector> apSets = helper.computeApSets(extracted, formulaChecker);
+
+            // std::vector<ValueType> numericResult = helper.computeDAProductProbabilities(env, *da, apSatSets);
+
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
 
@@ -156,10 +166,10 @@ namespace storm {
             storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
 
             STORM_LOG_INFO("Extracting maximal state formulas for path formula: " << pathFormula);
-
-            // Maintain a mapping from formula-strings to pairs in order to reuse labels of equivalent (compared as strings) formulas
-            std::map<std::string, storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair> extracted;
-            std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted);
+            storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted;
+            // Maintain a mapping from formula-strings to labels in order to reuse labels of equivalent (compared as strings) formulas
+            std::map<std::string, std::string> cached;
+            std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached);
 
             const SparseDtmcModelType& dtmc = this->getModel();
 

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -185,10 +185,10 @@ 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);
-
-            // Maintain a mapping from formula-strings to pairs in order to reuse labels of equivalent (compared as strings) formulas
-            std::map<std::string, storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair> extracted;
-            std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted);
+            storm::logic::ExtractMaximalStateFormulasVisitor::ApToFormulaMap extracted;
+            // Maintain a mapping from formula-strings to labels in order to reuse labels of equivalent (compared as strings) formulas
+            std::map<std::string, std::string> cached;
+            std::shared_ptr<storm::logic::Formula> ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached);
 
             const SparseMdpModelType& mdp = this->getModel();
             // TODO ?