From 8050f8fc67926d61ddd9831789ac68e2f66b5a8a Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 29 Aug 2018 08:54:28 +0200 Subject: [PATCH] eliminate reward accumulations on jani level --- src/storm-cli-utilities/model-handling.h | 41 ++------- .../RewardAccumulationEliminationVisitor.cpp | 88 +++++++------------ .../RewardAccumulationEliminationVisitor.h | 12 +-- src/storm/logic/TimeBoundType.h | 1 - src/storm/storage/jani/EdgeContainer.h | 2 +- 5 files changed, 49 insertions(+), 95 deletions(-) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 257453e92..524d772be 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -23,7 +23,6 @@ #include "storm/models/ModelBase.h" #include "storm/exceptions/OptionParserException.h" -#include "storm/exceptions/UnexpectedException.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" @@ -126,6 +125,10 @@ namespace storm { } if (!output.properties.empty()) { output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions); + if (output.model.is_initialized() && output.model->isJaniModel()) { + storm::logic::RewardAccumulationEliminationVisitor v(output.model->asJaniModel()); + v.eliminateRewardAccumulations(output.properties); + } } // Check whether conversion for PRISM to JANI is requested or necessary. @@ -384,7 +387,6 @@ namespace storm { std::pair, bool> result = std::make_pair(model, false); if (model->isSparseModel()) { - STORM_LOG_THROW((std::is_same::value), storm::exceptions::UnexpectedException, "Build-Value Type and ExportValueType should be the same in the sparse engine."); result = preprocessSparseModel(result.first->as>(), input); } else { STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); @@ -399,29 +401,6 @@ namespace storm { return result; } - template - storm::jani::Property preprocessProperty(std::shared_ptr const& model, storm::jani::Property const& property) { - storm::logic::RewardAccumulationEliminationVisitor v(model->getRewardModels(), model->getType()); - auto formula = v.eliminateRewardAccumulations(*property.getFilter().getFormula()); - auto states = v.eliminateRewardAccumulations(*property.getFilter().getStatesFormula()); - storm::jani::FilterExpression fe(formula, property.getFilter().getFilterType(), states); - return storm::jani::Property(property.getName(), fe, property.getComment()); - } - - template - std::vector preprocessProperties(std::shared_ptr const& model, SymbolicInput const& input) { - std::vector resultProperties; - for (auto const& property : input.properties) { - if (model->isSparseModel()) { - resultProperties.push_back(preprocessProperty(model->as>(), property)); - } else { - STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); - resultProperties.push_back(preprocessProperty(model->as>(), property)); - } - } - return resultProperties; - } - void printComputingCounterexample(storm::jani::Property const& property) { STORM_PRINT("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl); } @@ -696,7 +675,7 @@ namespace storm { } template - std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput& input, storm::settings::modules::CoreSettings::Engine engine) { + std::shared_ptr buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) { auto ioSettings = storm::settings::getModule(); auto buildSettings = storm::settings::getModule(); std::shared_ptr model; @@ -716,9 +695,6 @@ namespace storm { model = preprocessingResult.first; model->printModelInformationToStream(std::cout); } - if (!input.properties.empty()) { - input.properties = preprocessProperties(model, input); - } exportModel(model, input); } return model; @@ -737,16 +713,15 @@ namespace storm { } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) { verifyWithExplorationEngine(input); } else { - SymbolicInput preprocessedInput = input; - std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(preprocessedInput, engine); + std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, engine); if (model) { if (coreSettings.isCounterexampleSet()) { auto ioSettings = storm::settings::getModule(); - generateCounterexamples(model, preprocessedInput); + generateCounterexamples(model, input); } else { auto ioSettings = storm::settings::getModule(); - verifyModel(model, preprocessedInput, coreSettings); + verifyModel(model, input, coreSettings); } } } diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 0cefa9a7d..710f959f1 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -1,39 +1,35 @@ #include "storm/logic/RewardAccumulationEliminationVisitor.h" #include "storm/logic/Formulas.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/traverser/AssignmentsFinder.h" #include "storm/utility/macros.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/exceptions/InvalidPropertyException.h" -#include "storm/storage/dd/DdManager.h" -#include "storm/storage/dd/Add.h" -#include "storm/storage/dd/Bdd.h" - -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/models/symbolic/StandardRewardModel.h" namespace storm { namespace logic { - template - RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(std::unordered_map const& rewardModels, storm::models::ModelType const& modelType) : rewardModels(rewardModels) { - if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::S2pg) { - isDiscreteTimeModel = true; - } else if (modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::MarkovAutomaton) { - isDiscreteTimeModel = false; - } else { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unhandled model type " << modelType << "."); - } + RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(storm::jani::Model const& model) : model(model) { + // Intentionally left empty } - template - std::shared_ptr RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const { + std::shared_ptr RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const { boost::any result = f.accept(*this, boost::any()); return boost::any_cast>(result); } - template - boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { + 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()); + } + } + + boost::any RewardAccumulationEliminationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { std::vector> lowerBounds, upperBounds; std::vector timeBoundReferences; for (uint64_t i = 0; i < f.getDimension(); ++i) { @@ -68,8 +64,7 @@ namespace storm { } } - template - boost::any RewardAccumulationEliminationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { + boost::any RewardAccumulationEliminationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { boost::optional rewAcc; STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); auto rewName = boost::any_cast>(data); @@ -91,14 +86,13 @@ namespace storm { return std::static_pointer_cast(std::make_shared(bounds, timeBoundReferences, rewAcc)); } - template - boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { + boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); if (f.hasRewardAccumulation()) { if (f.isTimePathFormula()) { - if (isDiscreteTimeModel && ((!f.getRewardAccumulation().isExitSet() && !f.getRewardAccumulation().isStepsSet()) || (f.getRewardAccumulation().isStepsSet() && f.getRewardAccumulation().isExitSet()))) { + if (model.isDiscreteTimeModel() && ((!f.getRewardAccumulation().isExitSet() && !f.getRewardAccumulation().isStepsSet()) || (f.getRewardAccumulation().isStepsSet() && f.getRewardAccumulation().isExitSet()))) { return std::static_pointer_cast(std::make_shared(subformula, f.getContext(), f.getRewardAccumulation())); - } else if (!isDiscreteTimeModel && (!f.getRewardAccumulation().isTimeSet() || f.getRewardAccumulation().isExitSet() || f.getRewardAccumulation().isStepsSet())) { + } else if (!model.isDiscreteTimeModel() && (!f.getRewardAccumulation().isTimeSet() || f.getRewardAccumulation().isExitSet() || f.getRewardAccumulation().isStepsSet())) { return std::static_pointer_cast(std::make_shared(subformula, f.getContext(), f.getRewardAccumulation())); } } else if (f.isRewardPathFormula()) { @@ -112,14 +106,12 @@ namespace storm { return std::static_pointer_cast(std::make_shared(subformula, f.getContext())); } - template - boost::any RewardAccumulationEliminationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { + boost::any RewardAccumulationEliminationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, f.getOptionalRewardModelName())); return std::static_pointer_cast(std::make_shared(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); } - template - boost::any RewardAccumulationEliminationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { + boost::any RewardAccumulationEliminationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator."); auto rewName = boost::any_cast>(data); if (f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) { @@ -129,23 +121,22 @@ namespace storm { } } - template - bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional rewardModelName) const { - auto rewModelIt = rewardModels.end(); - if (rewardModelName.is_initialized()){ - rewModelIt = rewardModels.find(rewardModelName.get()); - STORM_LOG_THROW(rewModelIt != rewardModels.end(), storm::exceptions::InvalidPropertyException, "Unable to find reward model with name " << rewardModelName.get()); - } else if (rewardModels.size() == 1) { - rewModelIt = rewardModels.begin(); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Multiple reward models were defined but no reward model name was given for at least one property."); + bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional rewardModelName) const { + STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with for unique reward model."); + storm::jani::AssignmentsFinder::ResultType assignmentKinds; + STORM_LOG_THROW(model.hasGlobalVariable(rewardModelName.get()), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with name " << rewardModelName.get() << "."); + storm::jani::Variable const& transientVar = model.getGlobalVariable(rewardModelName.get()); + if (transientVar.getInitExpression().containsVariables() || !storm::utility::isZero(transientVar.getInitExpression().evaluateAsRational())) { + assignmentKinds.hasLocationAssignment = true; + assignmentKinds.hasEdgeAssignment = true; + assignmentKinds.hasEdgeDestinationAssignment = true; } - RewardModelType const& rewardModel = rewModelIt->second; - if ((rewardModel.hasStateActionRewards() || rewardModel.hasTransitionRewards()) && !accumulation.isStepsSet()) { + assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar); + if ((assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment) && !accumulation.isStepsSet()) { return false; } - if (rewardModel.hasStateRewards()) { - if (isDiscreteTimeModel) { + if (assignmentKinds.hasLocationAssignment) { + if (model.isDiscreteTimeModel()) { if (!accumulation.isExitSet()) { return false; } @@ -158,16 +149,5 @@ namespace storm { } return true; } - - template class RewardAccumulationEliminationVisitor>; - template class RewardAccumulationEliminationVisitor>; - template class RewardAccumulationEliminationVisitor>; - template class RewardAccumulationEliminationVisitor>; - - template class RewardAccumulationEliminationVisitor>; - template class RewardAccumulationEliminationVisitor>; - template class RewardAccumulationEliminationVisitor>; - template class RewardAccumulationEliminationVisitor>; - } } diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.h b/src/storm/logic/RewardAccumulationEliminationVisitor.h index 80915b8e9..0b77901d9 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.h +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.h @@ -5,21 +5,22 @@ #include "storm/logic/CloneVisitor.h" #include "storm/logic/RewardAccumulation.h" -#include "storm/models/ModelType.h" - +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" namespace storm { namespace logic { - template class RewardAccumulationEliminationVisitor : public CloneVisitor { public: - RewardAccumulationEliminationVisitor(std::unordered_map const& rewardModels, storm::models::ModelType const& modelType); + RewardAccumulationEliminationVisitor(storm::jani::Model const& model); /*! * Eliminates any reward accumulations of the formula, where the presence of the reward accumulation does not change the result of the formula */ std::shared_ptr eliminateRewardAccumulations(Formula const& f) const; + + void eliminateRewardAccumulations(std::vector& properties) 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; @@ -31,8 +32,7 @@ namespace storm { private: bool canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional rewardModelName) const; - std::unordered_map const& rewardModels; - bool isDiscreteTimeModel; + storm::jani::Model const& model; }; } diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h index 23f850105..ec9a753b0 100644 --- a/src/storm/logic/TimeBoundType.h +++ b/src/storm/logic/TimeBoundType.h @@ -51,7 +51,6 @@ namespace storm { } bool hasRewardAccumulation() const { - assert(isRewardBound()); return rewardAccumulation.is_initialized(); } diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h index faa33a418..c2bdfe80c 100644 --- a/src/storm/storage/jani/EdgeContainer.h +++ b/src/storm/storage/jani/EdgeContainer.h @@ -95,7 +95,7 @@ namespace storm { void clearConcreteEdges(); std::vector const& getConcreteEdges() const; std::vector & getConcreteEdges(); - TemplateEdgeContainer const& getTemplateEdges const; + TemplateEdgeContainer const& getTemplateEdges() const; size_t size() const;