use same labels for equivalent maximal state formulas

src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp

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

src/storm/logic/ExtractMaximalStateFormulasVisitor.h

@@ -1,7 +1,7 @@
 #pragma once
 
 #include <vector>
-
+#include <map>
 #include "storm/logic/CloneVisitor.h"
 
 namespace storm {
@@ -11,7 +11,10 @@ namespace storm {
         public:
             typedef std::pair<std::string, std::shared_ptr<Formula const>> LabelFormulaPair;
 
-            static std::shared_ptr<Formula> extract(PathFormula const& f, std::vector<LabelFormulaPair>& extractedFormulas);
+            // 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);
 
             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;
@@ -28,13 +31,13 @@ namespace storm {
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
 
         private:
-            ExtractMaximalStateFormulasVisitor(std::vector<LabelFormulaPair>& extractedFormulas);
+            ExtractMaximalStateFormulasVisitor(FormulaLabelMapping& extractedFormulas);
 
             std::shared_ptr<Formula> extract(std::shared_ptr<Formula> f) const;
             void incrementNestingLevel() const;
             void decrementNestingLevel() const;
 
-            std::vector<LabelFormulaPair>& extractedFormulas;
+            FormulaLabelMapping& extractedFormulas;
             std::size_t nestingLevel;
         };
 

src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -101,7 +101,9 @@ namespace storm {
             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;
+
+            // 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);
 
 

src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp

@@ -117,7 +117,9 @@ namespace storm {
             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;
+
+            // 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);
 
             const SparseMarkovAutomatonModelType& ma = this->getModel();

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

@@ -297,18 +297,19 @@ namespace storm {
             }
 
             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> 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> apSets;
-                for (auto& p : extracted) {
-                    STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << p.first << "\" <=> " << *p.second << "...");
+                for (auto& it: extracted) {
+                    storm::logic::ExtractMaximalStateFormulasVisitor::LabelFormulaPair pair = it.second;
+                    STORM_LOG_INFO(" Computing satisfaction set for atomic proposition \"" << pair.first << "\" <=> " << *pair.second << "...");
 
-                    std::unique_ptr<CheckResult> subResultPointer = formulaChecker(p.second);
+                    std::unique_ptr<CheckResult> subResultPointer = formulaChecker(pair.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.");
+                    apSets[pair.first] = std::move(sat);
+                    STORM_LOG_INFO(" Atomic proposition \"" << pair.first << "\" is satisfied by " << sat.getNumberOfSetBits() << " states.");
                 }
                 return apSets;
             }

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

@@ -27,8 +27,6 @@ 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
@@ -51,7 +49,7 @@ namespace storm {
                  * @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);
+                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);
 
 
             private:

src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -156,7 +156,9 @@ namespace storm {
             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;
+
+            // 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);
 
             const SparseDtmcModelType& dtmc = this->getModel();

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -185,8 +185,9 @@ 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;
-            
+
+            // 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);
 
             const SparseMdpModelType& mdp = this->getModel();

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

@@ -10,8 +10,6 @@
 #include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h"
 #include "MDPModelCheckingHelperReturnType.h"
 
-#include "storm/automata/AcceptanceCondition.h"
-
 #include "storm/utility/solver.h"
 #include "storm/solver/SolveGoal.h"