diff --git a/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp b/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp index 30d4d683a..6652c868b 100644 --- a/src/storm/logic/ExtractMaximalStateFormulasVisitor.cpp +++ b/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& cachedFormulas) : extractedFormulas(extractedFormulas), cachedFormulas(cachedFormulas), nestingLevel(0) { } - std::shared_ptr ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, FormulaLabelMapping& extractedFormulas) { - ExtractMaximalStateFormulasVisitor visitor(extractedFormulas); + std::shared_ptr ExtractMaximalStateFormulasVisitor::extract(PathFormula const& f, ApToFormulaMap& extractedFormulas, std::map& cachedFormulas) { + ExtractMaximalStateFormulasVisitor visitor(extractedFormulas, cachedFormulas); boost::any result = f.accept(visitor, boost::any()); return boost::any_cast>(result); } @@ -152,16 +152,20 @@ namespace storm { std::shared_ptr ExtractMaximalStateFormulasVisitor::extract(std::shared_ptr 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(label); } diff --git a/src/storm/logic/ExtractMaximalStateFormulasVisitor.h b/src/storm/logic/ExtractMaximalStateFormulasVisitor.h index de1cf8cda..d1a188c3d 100644 --- a/src/storm/logic/ExtractMaximalStateFormulasVisitor.h +++ b/src/storm/logic/ExtractMaximalStateFormulasVisitor.h @@ -9,12 +9,9 @@ namespace storm { class ExtractMaximalStateFormulasVisitor : public CloneVisitor { public: - typedef std::pair> LabelFormulaPair; + typedef std::map> 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 FormulaLabelMapping; - - static std::shared_ptr extract(PathFormula const& f, FormulaLabelMapping& extractedFormulas); + static std::shared_ptr extract(PathFormula const& f, ApToFormulaMap& extractedFormulas, std::map& 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& cachedFormulas); std::shared_ptr extract(std::shared_ptr 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& cachedFormulas; std::size_t nestingLevel; }; diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index be1910735..28824477f 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/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 extracted; - std::shared_ptr 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 cached; + std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached); const SparseCtmcModelType& ctmc = this->getModel(); diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 35239a154..6de3d079d 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/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 extracted; - std::shared_ptr 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 cached; + std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached); const SparseMarkovAutomatonModelType& ma = this->getModel(); typedef typename storm::models::sparse::Mdp SparseMdpModelType; - // TODO correct? STORM_LOG_INFO("Computing embedded MDP..."); storm::storage::SparseMatrix probabilityMatrix = ma.getTransitionMatrix(); // Copy of the state labelings of the MDP diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp index 89ab5737d..12c1f030c 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.cpp @@ -309,19 +309,18 @@ namespace storm { } template - std::map SparseLTLHelper::computeApSets(std::map 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& 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 subResultPointer = formulaChecker(pair.second); + std::unique_ptr 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; } diff --git a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h index a90f43370..71760e717 100644 --- a/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h +++ b/src/storm/modelchecker/helper/ltl/SparseLTLHelper.h @@ -49,7 +49,7 @@ namespace storm { * @param * @return */ - std::map computeApSets(std::map 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 ff41d1a73..7aa519bc6 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/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::map apSets; for (std::string const& ap : apSet.getAPs()) { std::shared_ptr expression = pathFormula.getAPMapping().at(ap); @@ -148,6 +149,15 @@ namespace storm { // TODO HOA call LTL helper std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeDAProductProbabilities(env, dtmc, std::move(goal), *da, apSets, checkTask.isQualitativeSet()); + // storm::modelchecker::helper::SparseLTLHelper 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 const& formula) {return this->check(*formula); }; + // std::map apSets = helper.computeApSets(extracted, formulaChecker); + + // std::vector numericResult = helper.computeDAProductProbabilities(env, *da, apSatSets); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(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 extracted; - std::shared_ptr 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 cached; + std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached); const SparseDtmcModelType& dtmc = this->getModel(); diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index d567100fb..934517663 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/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 extracted; - std::shared_ptr 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 cached; + std::shared_ptr ltlFormula = storm::logic::ExtractMaximalStateFormulasVisitor::extract(pathFormula, extracted, cached); const SparseMdpModelType& mdp = this->getModel(); // TODO ?