From 03c80f3ae1845e8f8d2034d5033309c0a4c33281 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 4 Oct 2018 10:27:43 +0200 Subject: [PATCH] correct treatment of non-trivial reward expressions --- src/storm-parsers/parser/JaniParser.cpp | 24 ++++++++++--- .../RewardAccumulationEliminationVisitor.cpp | 36 +++++++++++++------ src/storm/storage/jani/JSONExporter.cpp | 2 +- 3 files changed, 45 insertions(+), 17 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index eba57d0dd..52677bfb0 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -205,7 +205,11 @@ namespace storm { STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { try { + nonTrivialRewardModelExpressions.clear(); auto prop = this->parseProperty(propertyEntry, scope.refine("property[" + std::to_string(properties.size()) + "]")); + for (auto const& nonTrivRewExpr : nonTrivialRewardModelExpressions) { + model.addNonTrivialRewardExpression(nonTrivRewExpr.first, nonTrivRewExpr.second); + } // Eliminate reward accumulations as much as possible rewAccEliminator.eliminateRewardAccumulations(prop); properties.push_back(prop); @@ -321,7 +325,10 @@ namespace storm { STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a reward-instant in " + scope.description); storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), scope.refine("Step instant")); - if(rewardAccumulation.isEmpty()) { + if (!rewExpr.isVariable()) { + nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + } + if (rewardAccumulation.isEmpty()) { return std::make_shared(std::make_shared(stepInstantExpr, storm::logic::TimeBoundType::Steps), rewardName, opInfo); } else { return std::make_shared(std::make_shared(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps), rewardAccumulation), rewardName, opInfo); @@ -329,7 +336,10 @@ namespace storm { } else if (propertyStructure.count("time-instant") > 0) { STORM_LOG_THROW(propertyStructure.count("reward-instants") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a time-instant and a reward-instant in " + scope.description); storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), scope.refine("time instant")); - if(rewardAccumulation.isEmpty()) { + if (!rewExpr.isVariable()) { + nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + } + if (rewardAccumulation.isEmpty()) { return std::make_shared(std::make_shared(timeInstantExpr, storm::logic::TimeBoundType::Time), rewardName, opInfo); } else { return std::make_shared(std::make_shared(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time), rewardAccumulation), rewardName, opInfo); @@ -349,6 +359,9 @@ namespace storm { storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), scope.refine("reward instant")); bounds.emplace_back(false, rewInstantExpr); } + if (!rewExpr.isVariable()) { + nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + } return std::make_shared(std::make_shared(bounds, boundReferences, rewardAccumulation), rewardName, opInfo); } else { time = !rewExpr.containsVariables() && storm::utility::isOne(rewExpr.evaluateAsRational()); @@ -363,12 +376,12 @@ namespace storm { assert(subformula->isTotalRewardFormula() || subformula->isTimePathFormula()); return std::make_shared(subformula, opInfo); } else { + if (!rewExpr.isVariable()) { + nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); + } return std::make_shared(subformula, rewardName, opInfo); } } - if (!time && !rewExpr.isVariable()) { - nonTrivialRewardModelExpressions.emplace(rewardName, rewExpr); - } } else if (opString == "Smin" || opString == "Smax") { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); } else if (opString == "U" || opString == "F") { @@ -1403,6 +1416,7 @@ namespace storm { STORM_LOG_THROW(edgeEntry.at("rate").count("exp") == 1, storm::exceptions::InvalidJaniException, "Rate in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a defing expression."); rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), scope.refine("rate expression in edge from '" + sourceLoc)); STORM_LOG_THROW(rateExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Rate '" << rateExpr << "' has not a numerical type"); + STORM_LOG_THROW(rateExpr.containsVariables() || rateExpr.evaluateAsRational() > storm::utility::zero(), storm::exceptions::InvalidJaniException, "Only positive rates are allowed but rate '" << rateExpr << " was found."); } // guard STORM_LOG_THROW(edgeEntry.count("guard") <= 1, storm::exceptions::InvalidJaniException, "Guard can be given at most once in edge from '" << sourceLoc << "' in automaton '" << name << "'"); diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp index 34f911da7..11b99dabe 100644 --- a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -3,6 +3,7 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/traverser/AssignmentsFinder.h" +#include "storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.h" #include "storm/utility/macros.h" #include "storm/exceptions/UnexpectedException.h" @@ -126,20 +127,33 @@ namespace storm { } 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; + STORM_LOG_THROW(rewardModelName.is_initialized(), storm::exceptions::InvalidPropertyException, "Unable to find transient variable for unique reward model."); + storm::expressions::Expression rewardExpression = model.getRewardModelExpression(rewardModelName.get()); + bool hasStateRewards = false; + bool hasActionOrTransitionRewards = false; + auto variablesInRewardExpression = rewardExpression.getVariables(); + std::map initialSubstitution; + for (auto const& v : variablesInRewardExpression) { + STORM_LOG_ASSERT(model.hasGlobalVariable(v.getName()), "Unable to find global variable " << v.getName() << " occurring in a reward expression."); + auto const& janiVar = model.getGlobalVariable(v.getName()); + if (janiVar.hasInitExpression()) { + initialSubstitution.emplace(v, janiVar.getInitExpression()); + } + auto assignmentKinds = storm::jani::AssignmentsFinder().find(model, v); + hasActionOrTransitionRewards = hasActionOrTransitionRewards || assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment; + hasStateRewards = hasStateRewards || assignmentKinds.hasLocationAssignment; + } + rewardExpression = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution); + if (rewardExpression.containsVariables() || !storm::utility::isZero(rewardExpression.evaluateAsRational())) { + hasStateRewards = true; + hasActionOrTransitionRewards = true; } - assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar); - if ((assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment) && !accumulation.isStepsSet()) { + + + if (hasActionOrTransitionRewards && !accumulation.isStepsSet()) { return false; } - if (assignmentKinds.hasLocationAssignment) { + if (hasStateRewards) { if (model.isDiscreteTimeModel()) { if (!accumulation.isExitSet()) { return false; diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index be2c74471..8259229fc 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -183,7 +183,7 @@ namespace storm { time = time || (!model.isDeterministicModel() && assignmentKinds.hasLocationAssignment); exit = exit || assignmentKinds.hasLocationAssignment; } - storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution); + rewardExpression = storm::jani::substituteJaniExpression(rewardExpression, initialSubstitution); if (rewardExpression.containsVariables() || !storm::utility::isZero(rewardExpression.evaluateAsRational())) { steps = true; time = true;