From 701f3832b163bc19771f7b0ba1dbee7d330953dc Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 28 Aug 2018 10:19:58 +0200 Subject: [PATCH] parsing reward accumulations --- src/storm-parsers/parser/JaniParser.cpp | 64 ++++++++++++------------- src/storm-parsers/parser/JaniParser.h | 4 +- src/storm/logic/EventuallyFormula.cpp | 1 + 3 files changed, 35 insertions(+), 34 deletions(-) diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 0fecbe87a..65cd53ad4 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -196,6 +196,24 @@ namespace storm { } + storm::logic::RewardAccumulation JaniParser::parseRewardAccumulation(json const& accStructure, std::string const& context) { + bool accTime = false; + bool accSteps = false; + bool accExit = false; + STORM_LOG_THROW(accStructure.is_array(), storm::exceptions::InvalidJaniException, "Accumulate should be an array"); + for (auto const& accEntry : accStructure) { + if (accEntry == "steps") { + accSteps = true; + } else if (accEntry == "time") { + accTime = true; + } else if (accEntry == "exit") { + accExit = true; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "One may only accumulate either 'steps' or 'time' or 'exit', got " << accEntry.dump() << " in " << context); + } + } + return storm::logic::RewardAccumulation(accSteps, accTime, accExit); + } std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext,std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::string const& context, boost::optional bound) { if (propertyStructure.is_boolean()) { @@ -238,28 +256,17 @@ namespace storm { opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.bound = bound; - bool accTime = false; - bool accSteps = false; + storm::logic::RewardAccumulation rewardAccumulation(false, false, false); if (propertyStructure.count("accumulate") > 0) { - STORM_LOG_THROW(propertyStructure.at("accumulate").is_array(), storm::exceptions::InvalidJaniException, "Accumulate should be an array"); - for(auto const& accEntry : propertyStructure.at("accumulate")) { - if (accEntry == "steps") { - accSteps = true; - } else if (accEntry == "time") { - accTime = true; - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "One may only accumulate either 'steps' or 'time', got " << accEntry.dump() << " in " << context); - } - } + rewardAccumulation = parseRewardAccumulation(propertyStructure.at("accumulate"), context); } - // TODO: handle accumulation parameters! if (propertyStructure.count("step-instant") > 0) { STORM_LOG_THROW(propertyStructure.count("time-instant") == 0, storm::exceptions::NotSupportedException, "Storm does not support to have a step-instant and a time-instant in " + context); 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 " + context); storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context, globalVars, constants); - if(!accTime && !accSteps) { + if(rewardAccumulation.isEmpty()) { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); return std::make_shared(std::make_shared(stepInstantExpr, storm::logic::TimeBoundType::Steps), rewardName, opInfo); @@ -269,7 +276,7 @@ namespace storm { } else { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); - return std::make_shared(std::make_shared(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)), rewardName, opInfo); + return std::make_shared(std::make_shared(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps), rewardAccumulation), rewardName, opInfo); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); } @@ -279,7 +286,7 @@ namespace storm { storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context, globalVars, constants); - if(!accTime && !accSteps) { + if(rewardAccumulation.isEmpty()) { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); return std::make_shared(std::make_shared(timeInstantExpr, storm::logic::TimeBoundType::Time), rewardName, opInfo); @@ -289,7 +296,7 @@ namespace storm { } else { if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); - return std::make_shared(std::make_shared(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)), rewardName, opInfo); + return std::make_shared(std::make_shared(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time), rewardAccumulation), rewardName, opInfo); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); } @@ -300,25 +307,14 @@ namespace storm { for (auto const& rewInst : propertyStructure.at("reward-instants")) { storm::expressions::Expression rewInstExpression = parseExpression(rewInst.at("exp"), "Reward expression in " + context, globalVars, constants); STORM_LOG_THROW(!rewInstExpression.isVariable(), storm::exceptions::NotSupportedException, "Reward bounded cumulative reward formulas should only argue over reward expressions."); - boundReferences.emplace_back(rewInstExpression.getVariables().begin()->getName()); - bool rewInstAccSteps(false), rewInstAccTime(false); - for (auto const& accEntry : rewInst.at("accumulate")) { - if (accEntry == "steps") { - rewInstAccSteps = true; - } else if (accEntry == "time") { - rewInstAccTime = true; - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "One may only accumulate either 'steps' or 'time', got " << accEntry.dump() << " in " << context); - } - } - STORM_LOG_THROW(rewInstAccSteps || rewInstAccTime, storm::exceptions::NotSupportedException, "Storm only allows to accumulate either over time or over steps in " + context); - // TODO: handle accumulation parameters + storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rewInst.at("accumulate"), context); + boundReferences.emplace_back(rewInstExpression.getVariables().begin()->getName(), boundRewardAccumulation); storm::expressions::Expression rewInstantExpr = parseExpression(rewInst.at("instant"), "reward instant in " + context, globalVars, constants); bounds.emplace_back(false, rewInstantExpr); } if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); - return std::make_shared(std::make_shared(bounds, boundReferences), rewardName, opInfo); + return std::make_shared(std::make_shared(bounds, boundReferences, rewardAccumulation), rewardName, opInfo); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); } @@ -326,9 +322,9 @@ namespace storm { std::shared_ptr subformula; if (propertyStructure.count("reach") > 0) { auto context = time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward; - subformula = std::make_shared(parseFormula(propertyStructure.at("reach"), context, globalVars, constants, "Reach-expression of operator " + opString), context); + subformula = std::make_shared(parseFormula(propertyStructure.at("reach"), context, globalVars, constants, "Reach-expression of operator " + opString), context, rewardAccumulation); } else { - subformula = std::make_shared(); + subformula = std::make_shared(rewardAccumulation); } if (rewExpr.isVariable()) { assert(!time); @@ -410,6 +406,8 @@ namespace storm { STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); storm::expressions::Expression rewExpr = parseExpression(rbStructure.at("exp"), "Reward expression in " + context, globalVars, constants); STORM_LOG_THROW(rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions."); + storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rbStructure.at("accumulate"), context); + tbReferences.emplace_back(rewExpr.getVariables().begin()->getName(), boundRewardAccumulation); std::string rewardName = rewExpr.getVariables().begin()->getName(); STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type."); if (pi.hasLowerBound()) { diff --git a/src/storm-parsers/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h index 1ac4a514f..f56984c25 100644 --- a/src/storm-parsers/parser/JaniParser.h +++ b/src/storm-parsers/parser/JaniParser.h @@ -2,6 +2,7 @@ #include "storm/storage/jani/Constant.h" #include "storm/logic/Formula.h" #include "storm/logic/Bound.h" +#include "storm/logic/RewardAccumulation.h" #include "storm/exceptions/FileIoException.h" #include "storm/storage/expressions/ExpressionManager.h" @@ -66,7 +67,8 @@ namespace storm { std::vector> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::string const& context); std::vector> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::string const& context); storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure, std::unordered_map> const& constants); - + storm::logic::RewardAccumulation parseRewardAccumulation(json const& accStructure, std::string const& context); + std::shared_ptr parseComposition(json const& compositionStructure); storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& globalVars, std::unordered_map> const& constants, std::unordered_map> const& localVars = {}); diff --git a/src/storm/logic/EventuallyFormula.cpp b/src/storm/logic/EventuallyFormula.cpp index 863b977fd..c8ed335e5 100644 --- a/src/storm/logic/EventuallyFormula.cpp +++ b/src/storm/logic/EventuallyFormula.cpp @@ -8,6 +8,7 @@ namespace storm { namespace logic { EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context, boost::optional rewardAccumulation) : UnaryPathFormula(subformula), context(context), rewardAccumulation(rewardAccumulation) { STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::Time, storm::exceptions::InvalidPropertyException, "Invalid context for formula."); + STORM_LOG_THROW(context != FormulaContext::Probability || !rewardAccumulation.is_initialized(), storm::exceptions::InvalidPropertyException, "Reward accumulations should only be given for time- and reward formulas"); } FormulaContext const& EventuallyFormula::getContext() const {