From 539b3230eb46d8e9ab45bd23797b43311a6479df Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 29 Aug 2018 08:56:57 +0200 Subject: [PATCH] when exporting jani, eliminate reward accumulation kinds whenever they do not have any effect --- src/storm/storage/jani/JSONExporter.cpp | 46 ++++++++++++++++++------- src/storm/storage/jani/JSONExporter.h | 3 +- 2 files changed, 35 insertions(+), 14 deletions(-) diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index d0d1fb8e6..cc45468c0 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -11,6 +11,7 @@ #include "storm/exceptions/InvalidJaniException.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/InvalidPropertyException.h" #include "storm/storage/expressions/RationalLiteralExpression.h" #include "storm/storage/expressions/IntegerLiteralExpression.h" @@ -29,6 +30,7 @@ #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/Property.h" +#include "storm/storage/jani/traverser/AssignmentsFinder.h" namespace storm { namespace jani { @@ -153,6 +155,24 @@ namespace storm { return iDecl; } + modernjson::json FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const { + + storm::jani::Variable const& transientVar = model.getGlobalVariable(rewardModelName); + storm::jani::AssignmentsFinder::ResultType assignmentKinds; + STORM_LOG_THROW(model.hasGlobalVariable(rewardModelName), storm::exceptions::InvalidPropertyException, "Unable to find transient variable with name " << rewardModelName << "."); + if (transientVar.getInitExpression().containsVariables() || !storm::utility::isZero(transientVar.getInitExpression().evaluateAsRational())) { + assignmentKinds.hasLocationAssignment = true; + assignmentKinds.hasEdgeAssignment = true; + assignmentKinds.hasEdgeDestinationAssignment = true; + } + assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar); + + bool steps = rewardAccumulation.isStepsSet() && (assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment); + bool time = rewardAccumulation.isTimeSet() && !model.isDiscreteTimeModel() && assignmentKinds.hasLocationAssignment; + bool exit = rewardAccumulation.isExitSet() && assignmentKinds.hasLocationAssignment; + return constructRewardAccumulation(storm::logic::RewardAccumulation(steps, time, exit)); + } + modernjson::json FormulaToJaniJson::constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const { std::vector res; if (rewardAccumulation.isStepsSet()) { @@ -168,11 +188,11 @@ namespace storm { return res; } - modernjson::json FormulaToJaniJson::constructStandardRewardAccumulation() const { + modernjson::json FormulaToJaniJson::constructStandardRewardAccumulation(std::string const& rewardModelName) const { if (model.isDiscreteTimeModel()) { - return constructRewardAccumulation(storm::logic::RewardAccumulation(true, false, true)); + return constructRewardAccumulation(storm::logic::RewardAccumulation(true, false, true), rewardModelName); } else { - return constructRewardAccumulation(storm::logic::RewardAccumulation(true, true, false)); + return constructRewardAccumulation(storm::logic::RewardAccumulation(true, true, false), rewardModelName); } } @@ -241,9 +261,9 @@ namespace storm { modernjson::json rewbound; rewbound["exp"] = tbr.getRewardName(); if (tbr.hasRewardAccumulation()) { - rewbound["accumulate"] = constructRewardAccumulation(tbr.getRewardAccumulation()); + rewbound["accumulate"] = constructRewardAccumulation(tbr.getRewardAccumulation(), tbr.getRewardName()); } else { - rewbound["accumulate"] = constructStandardRewardAccumulation(); + rewbound["accumulate"] = constructStandardRewardAccumulation(tbr.getRewardName()); } rewbound["bounds"] = propertyInterval; rewardBounds.push_back(std::move(rewbound)); @@ -469,18 +489,18 @@ namespace storm { if (f.getSubformula().isEventuallyFormula()) { opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); if (f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) { - opDecl["left"]["accumulate"] = constructRewardAccumulation(f.getSubformula().asEventuallyFormula().getRewardAccumulation()); + opDecl["left"]["accumulate"] = constructRewardAccumulation(f.getSubformula().asEventuallyFormula().getRewardAccumulation(), rewardModelName); } else { - opDecl["left"]["accumulate"] = constructStandardRewardAccumulation(); + opDecl["left"]["accumulate"] = constructStandardRewardAccumulation(rewardModelName); } } else if (f.getSubformula().isCumulativeRewardFormula()) { // TODO: support for reward bounded formulas STORM_LOG_WARN_COND(!f.getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound(), "Export for reward bounded cumulative reward formulas currently unsupported."); opDecl["left"][instantName] = buildExpression(f.getSubformula().asCumulativeRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); if (f.getSubformula().asCumulativeRewardFormula().hasRewardAccumulation()) { - opDecl["left"]["accumulate"] = constructRewardAccumulation(f.getSubformula().asCumulativeRewardFormula().getRewardAccumulation()); + opDecl["left"]["accumulate"] = constructRewardAccumulation(f.getSubformula().asCumulativeRewardFormula().getRewardAccumulation(), rewardModelName); } else { - opDecl["left"]["accumulate"] = constructStandardRewardAccumulation(); + opDecl["left"]["accumulate"] = constructStandardRewardAccumulation(rewardModelName); } } else if (f.getSubformula().isInstantaneousRewardFormula()) { opDecl["left"][instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); @@ -499,18 +519,18 @@ namespace storm { if (f.getSubformula().isEventuallyFormula()) { opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); if (f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) { - opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asEventuallyFormula().getRewardAccumulation()); + opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asEventuallyFormula().getRewardAccumulation(), rewardModelName); } else { - opDecl["accumulate"] = constructStandardRewardAccumulation(); + opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName); } } else if (f.getSubformula().isCumulativeRewardFormula()) { // TODO: support for reward bounded formulas STORM_LOG_WARN_COND(!f.getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound(), "Export for reward bounded cumulative reward formulas currently unsupported."); opDecl[instantName] = buildExpression(f.getSubformula().asCumulativeRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); if (f.getSubformula().asCumulativeRewardFormula().hasRewardAccumulation()) { - opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asCumulativeRewardFormula().getRewardAccumulation()); + opDecl["accumulate"] = constructRewardAccumulation(f.getSubformula().asCumulativeRewardFormula().getRewardAccumulation(), rewardModelName); } else { - opDecl["accumulate"] = constructStandardRewardAccumulation(); + opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName); } } else if (f.getSubformula().isInstantaneousRewardFormula()) { opDecl[instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 63bc24826..1f1a49db8 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -70,7 +70,8 @@ namespace storm { modernjson::json constructPropertyInterval(boost::optional const& lower, boost::optional const& lowerExclusive, boost::optional const& upper, boost::optional const& upperExclusive) const; modernjson::json constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation) const; - modernjson::json constructStandardRewardAccumulation() const; + modernjson::json constructRewardAccumulation(storm::logic::RewardAccumulation const& rewardAccumulation, std::string const& rewardModelName) const; + modernjson::json constructStandardRewardAccumulation(std::string const& rewardModelName) const; storm::jani::Model const& model; mutable bool stateExitRewards;