From f89817da3bd0e153fdad6e2d00b6f26603a4a78b Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 18 Sep 2018 15:45:20 +0200 Subject: [PATCH] eliminating reward accumulations directly at parsing time --- src/storm-parsers/api/properties.cpp | 6 +++++- src/storm-parsers/parser/JaniParser.cpp | 6 ++++++ .../logic/RewardAccumulationEliminationVisitor.cpp | 12 ++++++++---- .../logic/RewardAccumulationEliminationVisitor.h | 1 + 4 files changed, 20 insertions(+), 5 deletions(-) diff --git a/src/storm-parsers/api/properties.cpp b/src/storm-parsers/api/properties.cpp index 425fee410..68b68e990 100644 --- a/src/storm-parsers/api/properties.cpp +++ b/src/storm-parsers/api/properties.cpp @@ -3,8 +3,9 @@ #include "storm-parsers/parser/FormulaParser.h" #include "storm/api/properties.h" - #include "storm/storage/SymbolicModelDescription.h" +#include "storm/logic/RewardAccumulationEliminationVisitor.h" + #include "storm/storage/prism/Program.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" @@ -48,6 +49,9 @@ namespace storm { std::vector parsePropertiesForJaniModel(std::string const &inputString, storm::jani::Model const &model, boost::optional > const &propertyFilter) { storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer()); auto formulas = parseProperties(formulaParser, inputString, propertyFilter); + // Eliminate reward accumulations if possible + storm::logic::RewardAccumulationEliminationVisitor v(model); + v.eliminateRewardAccumulations(formulas); return substituteConstantsInProperties(formulas, model.getConstantsSubstitution()); } diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 697f3bcbe..20b256a0b 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -177,6 +177,10 @@ namespace storm { STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given"); std::shared_ptr composition = parseComposition(parsedStructure.at("system")); model.setSystemComposition(composition); + model.finalize(); + + // Parse properties + storm::logic::RewardAccumulationEliminationVisitor rewAccEliminator(model); STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given"); std::map properties; if (parseProperties && parsedStructure.count("properties") == 1) { @@ -184,6 +188,8 @@ namespace storm { for(auto const& propertyEntry : parsedStructure.at("properties")) { try { auto prop = this->parseProperty(propertyEntry, scope.refine("property[" + std::to_string(properties.size()) + "]")); + // Eliminate reward accumulations as much as possible + rewAccEliminator.eliminateRewardAccumulations(prop); properties.emplace(prop.getName(), prop); } catch (storm::exceptions::NotSupportedException const& ex) { STORM_LOG_WARN("Cannot handle property: " << ex.what()); diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 710f959f1..2ee9150f7 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -22,13 +22,17 @@ namespace storm { void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(std::vector& properties) const { for (auto& p : properties) { - auto formula = eliminateRewardAccumulations(*p.getFilter().getFormula()); - auto states = eliminateRewardAccumulations(*p.getFilter().getStatesFormula()); - storm::jani::FilterExpression fe(formula, p.getFilter().getFilterType(), states); - p = storm::jani::Property(p.getName(), storm::jani::FilterExpression(formula, p.getFilter().getFilterType(), states), p.getComment()); + eliminateRewardAccumulations(p); } } + void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(storm::jani::Property& property) const { + auto formula = eliminateRewardAccumulations(*property.getFilter().getFormula()); + auto states = eliminateRewardAccumulations(*property.getFilter().getStatesFormula()); + storm::jani::FilterExpression fe(formula, property.getFilter().getFilterType(), states); + property = storm::jani::Property(property.getName(), storm::jani::FilterExpression(formula, property.getFilter().getFilterType(), states), property.getComment()); + } + boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.h b/src/storm/logic/RewardAccumulationEliminationVisitor.h index 0b77901d9..59dbc330d 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.h +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.h @@ -21,6 +21,7 @@ namespace storm { std::shared_ptr eliminateRewardAccumulations(Formula const& f) const; void eliminateRewardAccumulations(std::vector& properties) const; + void eliminateRewardAccumulations(storm::jani::Property& property) const; virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override; virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;