From 1d5860de8d77be8a40c3dc7f854c3f06a5d0c53c Mon Sep 17 00:00:00 2001 From: hannah Date: Thu, 17 Jun 2021 18:52:40 +0200 Subject: [PATCH] use same labels for equivalent maximal state formulas --- .../ExtractMaximalStateFormulasVisitor.cpp | 18 +++++++++++++----- .../logic/ExtractMaximalStateFormulasVisitor.h | 11 +++++++---- .../csl/SparseCtmcCslModelChecker.cpp | 4 +++- .../SparseMarkovAutomatonCslModelChecker.cpp | 4 +++- .../helper/ltl/SparseLTLHelper.cpp | 13 +++++++------ .../modelchecker/helper/ltl/SparseLTLHelper.h | 4 +--- .../prctl/SparseDtmcPrctlModelChecker.cpp | 4 +++- .../prctl/SparseMdpPrctlModelChecker.cpp | 5 +++-- .../prctl/helper/SparseMdpPrctlHelper.h | 2 -- 9 files changed, 40 insertions(+), 25 deletions(-) diff --git a/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp b/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp index d6f465027..30d4d683a 100644 --- a/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp +++ b/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp @@ -7,10 +7,10 @@ namespace storm { namespace logic { - ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(std::vector& extractedFormulas) : extractedFormulas(extractedFormulas), nestingLevel(0) { + ExtractMaximalStateFormulasVisitor::ExtractMaximalStateFormulasVisitor(FormulaLabelMapping& extractedFormulas) : extractedFormulas(extractedFormulas), nestingLevel(0) { } - std::shared_ptr ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, std::vector& extractedFormulas) { + std::shared_ptr ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, FormulaLabelMapping& extractedFormulas) { ExtractMaximalStateFormulasVisitor visitor(extractedFormulas); boost::any result = f.accept(visitor, boost::any()); return boost::any_cast>(result); @@ -150,10 +150,18 @@ namespace storm { } std::shared_ptr ExtractMaximalStateFormulasVisitor::extract(std::shared_ptr f) const { - std::string label = "p" + std::to_string(extractedFormulas.size()); - - const_cast&>(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(label); } diff --git a/src/storm/logic/ExtractMaximalStateFormulasVisitor.h b/src/storm/logic/ExtractMaximalStateFormulasVisitor.h index e3bd1cea5..de1cf8cda 100644 --- a/src/storm/logic/ExtractMaximalStateFormulasVisitor.h +++ b/src/storm/logic/ExtractMaximalStateFormulasVisitor.h @@ -1,7 +1,7 @@ #pragma once #include - +#include #include "storm/logic/CloneVisitor.h" namespace storm { @@ -11,7 +11,10 @@ namespace storm { public: typedef std::pair> LabelFormulaPair; - static std::shared_ptr extract(PathFormula const& f, std::vector& 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 FormulaLabelMapping; + + static std::shared_ptr 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& extractedFormulas); + ExtractMaximalStateFormulasVisitor(FormulaLabelMapping& extractedFormulas); std::shared_ptr extract(std::shared_ptr f) const; void incrementNestingLevel() const; void decrementNestingLevel() const; - std::vector& extractedFormulas; + FormulaLabelMapping& extractedFormulas; std::size_t nestingLevel; }; diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 995c06856..be1910735 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/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 extracted; + + // Maintain a mapping from formula-strings to pairs in order to reuse labels of equivalent (compared as strings) formulas + std::map extracted; std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted); diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 90c13cf61..c35c05b43 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/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 extracted; + + // Maintain a mapping from formula-strings to pairs in order to reuse labels of equivalent (compared as strings) formulas + std::map extracted; std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted); const SparseMarkovAutomatonModelType& ma = this->getModel(); diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 925f0ec3b..ea6df66fc 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -297,18 +297,19 @@ namespace storm { } template - std::map SparseLTLHelper::computeApSets(std::vector const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker){ + std::map SparseLTLHelper::computeApSets(std::map const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker){ std::map 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 subResultPointer = formulaChecker(p.second); + std::unique_ptr 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; } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index 44e618644..a90f43370 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -27,8 +27,6 @@ namespace storm { */ using productModelType = typename std::conditional, storm::models::sparse::Dtmc>::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 computeApSets(std::vector const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker); + std::map computeApSets(std::map const& extracted, std::function(std::shared_ptr const& formula)> formulaChecker); private: diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 70f7cd475..ff41d1a73 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/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 extracted; + + // Maintain a mapping from formula-strings to pairs in order to reuse labels of equivalent (compared as strings) formulas + std::map extracted; std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted); const SparseDtmcModelType& dtmc = this->getModel(); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 500e893ea..d567100fb 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/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 extracted; - + + // Maintain a mapping from formula-strings to pairs in order to reuse labels of equivalent (compared as strings) formulas + std::map extracted; std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted); const SparseMdpModelType& mdp = this->getModel(); diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index ea38383f0..6515b9d83 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/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"