sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

parsing reward accumulations

tempestpy_adaptions
TimQu 6 years ago
parent
ee1dcbd483
commit
701f3832b1
3 changed files with 35 additions and 34 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 64
      src/storm-parsers/parser/JaniParser.cpp
  2. 4
      src/storm-parsers/parser/JaniParser.h
  3. 1
      src/storm/logic/EventuallyFormula.cpp

64
src/storm-parsers/parser/JaniParser.cpp
View File

@ -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<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext,std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& context, boost::optional<storm::logic::Bound> 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<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(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<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)), rewardName, opInfo);
return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(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<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(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<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)), rewardName, opInfo);
return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(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<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(bounds, boundReferences), rewardName, opInfo);
return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(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<storm::logic::Formula const> subformula;
if (propertyStructure.count("reach") > 0) {
auto context = time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward;
subformula = std::make_shared<storm::logic::EventuallyFormula>(parseFormula(propertyStructure.at("reach"), context, globalVars, constants, "Reach-expression of operator " + opString), context);
subformula = std::make_shared<storm::logic::EventuallyFormula>(parseFormula(propertyStructure.at("reach"), context, globalVars, constants, "Reach-expression of operator " + opString), context, rewardAccumulation);
} else {
subformula = std::make_shared<storm::logic::TotalRewardFormula>();
subformula = std::make_shared<storm::logic::TotalRewardFormula>(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()) {

4
src/storm-parsers/parser/JaniParser.h
View File

@ -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<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& context);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::string const& context);
storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants);
storm::logic::RewardAccumulation parseRewardAccumulation(json const& accStructure, std::string const& context);
std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);
storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& globalVars, std::unordered_map<std::string, std::shared_ptr<storm::jani::Constant>> const& constants, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});

1
src/storm/logic/EventuallyFormula.cpp
View File

@ -8,6 +8,7 @@ namespace storm {
namespace logic {
EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context, boost::optional<RewardAccumulation> 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 {

Write Preview
Loading…
Cancel
Save