diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index f60a3ffb5..524d772be 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -18,6 +18,7 @@ #include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/jani/Property.h" +#include "storm/logic/RewardAccumulationEliminationVisitor.h" #include "storm/models/ModelBase.h" @@ -124,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. diff --git a/src/storm-conv/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h index 2b2d6de7a..99e00ea9b 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.h +++ b/src/storm-conv/settings/modules/JaniExportSettings.h @@ -14,16 +14,6 @@ namespace storm { */ JaniExportSettings(); - /** - * Retrievew whether the pgcl file option was set - */ - bool isJaniFileSet() const; - - /** - * Retrieves the pgcl file name - */ - std::string getJaniFilename() const; - bool isExportAsStandardJaniSet() const; bool isExportFlattenedSet() const; @@ -42,8 +32,6 @@ namespace storm { static const std::string moduleName; private: - static const std::string janiFileOptionName; - static const std::string janiFileOptionShortName; static const std::string standardCompliantOptionName; static const std::string standardCompliantOptionShortName; static const std::string exportFlattenOptionName; diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index f6d6251dd..65cd53ad4 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -90,6 +90,15 @@ namespace storm { storm::jani::ModelType type = storm::jani::getModelType(modeltypestring); STORM_LOG_THROW(type != storm::jani::ModelType::UNDEFINED, storm::exceptions::InvalidJaniException, "model type " + modeltypestring + " not recognized"); storm::jani::Model model(name, type, version, expressionManager); + size_t featuresCount = parsedStructure.count("features"); + STORM_LOG_THROW(featuresCount < 2, storm::exceptions::InvalidJaniException, "features-declarations can be given at most once."); + if (featuresCount == 1) { + std::unordered_set supportedFeatures = {"derived-operators", "state-exit-rewards"}; + for (auto const& feature : parsedStructure.at("features")) { + std::string featureStr = getString(feature, "Model feature"); + STORM_LOG_WARN_COND(supportedFeatures.find(featureStr) != supportedFeatures.end(), "Storm does not support the model feature " << featureStr << "."); + } + } size_t actionCount = parsedStructure.count("actions"); STORM_LOG_THROW(actionCount < 2, storm::exceptions::InvalidJaniException, "Action-declarations can be given at most once."); if (actionCount > 0) { @@ -187,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()) { @@ -229,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); @@ -260,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"); } @@ -270,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); @@ -280,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"); } @@ -291,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"); } @@ -317,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); @@ -401,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()) { @@ -478,8 +485,6 @@ namespace storm { } else if(propertyStructure.at("right").count("op") > 0 && (propertyStructure.at("right").at("op") == "Pmin" || propertyStructure.at("right").at("op") == "Pmax" || propertyStructure.at("right").at("op") == "Emin" || propertyStructure.at("right").at("op") == "Emax" || propertyStructure.at("right").at("op") == "Smin" || propertyStructure.at("right").at("op") == "Smax")) { auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get(),{},{}); - STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); - // TODO evaluate this expression directly as rational number return parseFormula(propertyStructure.at("right"),formulaContext, globalVars, constants, "", storm::logic::Bound(ct, expr)); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons are allowed."); @@ -950,8 +955,7 @@ namespace storm { assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); - // TODO implement - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "modulo operation is not yet implemented"); + return arguments[0] % arguments[1]; } else if (opstring == "max") { arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); @@ -988,14 +992,13 @@ namespace storm { arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); - return storm::expressions::abs(arguments[0]); + return storm::expressions::truncate(arguments[0]); } else if (opstring == "pow") { arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); - // TODO implement - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "pow operation is not yet implemented"); + return arguments[0]^arguments[1]; } else if (opstring == "exp") { arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, globalVars, constants, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); 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/builder/DdPrismModelBuilder.h b/src/storm/builder/DdPrismModelBuilder.h index 57d990b23..fb357a6c8 100644 --- a/src/storm/builder/DdPrismModelBuilder.h +++ b/src/storm/builder/DdPrismModelBuilder.h @@ -3,6 +3,7 @@ #include #include +#include #include "storm/storage/prism/Program.h" diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 97c768944..6054e7cd3 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -285,7 +285,11 @@ namespace storm { out << ", "; } if (this->getTimeBoundReference(i).isRewardBound()) { - out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + out << "rew"; + if (this->getTimeBoundReference(i).hasRewardAccumulation()) { + out << "[" << this->getTimeBoundReference(i).getRewardAccumulation() << "]"; + } + out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; } else if (this->getTimeBoundReference(i).isStepBound()) { out << "steps"; //} else if (this->getTimeBoundReference(i).isStepBound()) diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp index d97dd41d6..4b427b1dc 100644 --- a/src/storm/logic/CloneVisitor.cpp +++ b/src/storm/logic/CloneVisitor.cpp @@ -70,7 +70,11 @@ namespace storm { boost::any CloneVisitor::visit(EventuallyFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); - return std::static_pointer_cast(std::make_shared(subformula, f.getContext())); + if (f.hasRewardAccumulation()) { + return std::static_pointer_cast(std::make_shared(subformula, f.getContext(), f.getRewardAccumulation())); + } else { + return std::static_pointer_cast(std::make_shared(subformula, f.getContext())); + } } boost::any CloneVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { @@ -119,8 +123,8 @@ namespace storm { return std::static_pointer_cast(std::make_shared(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); } - boost::any CloneVisitor::visit(TotalRewardFormula const&, boost::any const&) const { - return std::static_pointer_cast(std::make_shared()); + boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const { + return std::static_pointer_cast(std::make_shared(f)); } boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index 19a60a623..bbf21cbf0 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -9,11 +9,11 @@ namespace storm { namespace logic { - CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference) : timeBoundReferences({timeBoundReference}), bounds({bound}) { + CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference, boost::optional rewardAccumulation) : timeBoundReferences({timeBoundReference}), bounds({bound}), rewardAccumulation(rewardAccumulation) { // Intentionally left empty. } - CumulativeRewardFormula::CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences) : timeBoundReferences(timeBoundReferences), bounds(bounds) { + CumulativeRewardFormula::CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences, boost::optional rewardAccumulation) : timeBoundReferences(timeBoundReferences), bounds(bounds), rewardAccumulation(rewardAccumulation) { STORM_LOG_ASSERT(this->timeBoundReferences.size() == this->bounds.size(), "Number of time bounds and number of time bound references does not match."); STORM_LOG_ASSERT(!this->timeBoundReferences.empty(), "No time bounds given."); @@ -137,12 +137,24 @@ namespace storm { STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants."); } + bool CumulativeRewardFormula::hasRewardAccumulation() const { + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& CumulativeRewardFormula::getRewardAccumulation() const { + return rewardAccumulation.get(); + } + + std::shared_ptr CumulativeRewardFormula::restrictToDimension(unsigned i) const { return std::make_shared(bounds.at(i), getTimeBoundReference(i)); } std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const { out << "C"; + if (hasRewardAccumulation()) { + out << "[" << getRewardAccumulation() << "]"; + } if (this->isMultiDimensional()) { out << "^{"; } @@ -151,7 +163,11 @@ namespace storm { out << ", "; } if (this->getTimeBoundReference(i).isRewardBound()) { - out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; + out << "rew"; + if (this->getTimeBoundReference(i).hasRewardAccumulation()) { + out << "[" << this->getTimeBoundReference(i).getRewardAccumulation() << "]"; + } + out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}"; } else if (this->getTimeBoundReference(i).isStepBound()) { out << "steps"; //} else if (this->getTimeBoundReference(i).isStepBound()) diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h index e40370b07..4c436037e 100644 --- a/src/storm/logic/CumulativeRewardFormula.h +++ b/src/storm/logic/CumulativeRewardFormula.h @@ -10,8 +10,8 @@ namespace storm { namespace logic { class CumulativeRewardFormula : public PathFormula { public: - CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time)); - CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences); + CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time), boost::optional rewardAccumulation = boost::none); + CumulativeRewardFormula(std::vector const& bounds, std::vector const& timeBoundReferences, boost::optional rewardAccumulation = boost::none); virtual ~CumulativeRewardFormula() = default; @@ -47,6 +47,9 @@ namespace storm { template ValueType getNonStrictBound() const; + bool hasRewardAccumulation() const; + RewardAccumulation const& getRewardAccumulation() const; + std::shared_ptr restrictToDimension(unsigned i) const; private: @@ -54,6 +57,8 @@ namespace storm { std::vector timeBoundReferences; std::vector bounds; + boost::optional rewardAccumulation; + }; } } diff --git a/src/storm/logic/EventuallyFormula.cpp b/src/storm/logic/EventuallyFormula.cpp index 2f1243f8a..c8ed335e5 100644 --- a/src/storm/logic/EventuallyFormula.cpp +++ b/src/storm/logic/EventuallyFormula.cpp @@ -6,8 +6,9 @@ namespace storm { namespace logic { - EventuallyFormula::EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context) : UnaryPathFormula(subformula), context(context) { + 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 { @@ -42,6 +43,14 @@ namespace storm { return this->isReachabilityTimeFormula(); } + bool EventuallyFormula::hasRewardAccumulation() const { + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& EventuallyFormula::getRewardAccumulation() const { + return rewardAccumulation.get(); + } + boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } @@ -49,6 +58,9 @@ namespace storm { std::ostream& EventuallyFormula::writeToStream(std::ostream& out) const { out << "F "; this->getSubformula().writeToStream(out); + if (hasRewardAccumulation()) { + out << "[" << getRewardAccumulation() << "]"; + } return out; } } diff --git a/src/storm/logic/EventuallyFormula.h b/src/storm/logic/EventuallyFormula.h index 9cc4d853d..5fa30da6d 100644 --- a/src/storm/logic/EventuallyFormula.h +++ b/src/storm/logic/EventuallyFormula.h @@ -1,14 +1,17 @@ #ifndef STORM_LOGIC_EVENTUALLYFORMULA_H_ #define STORM_LOGIC_EVENTUALLYFORMULA_H_ +#include + #include "storm/logic/UnaryPathFormula.h" #include "storm/logic/FormulaContext.h" +#include "storm/logic/RewardAccumulation.h" namespace storm { namespace logic { class EventuallyFormula : public UnaryPathFormula { public: - EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context = FormulaContext::Probability); + EventuallyFormula(std::shared_ptr const& subformula, FormulaContext context = FormulaContext::Probability, boost::optional rewardAccumulation = boost::none); virtual ~EventuallyFormula() { // Intentionally left empty. @@ -27,9 +30,12 @@ namespace storm { virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; + bool hasRewardAccumulation() const; + RewardAccumulation const& getRewardAccumulation() const; private: FormulaContext context; + boost::optional rewardAccumulation; }; } } diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 24ad016c8..adc96728b 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -70,6 +70,9 @@ namespace storm { } else { assert(tbr.isRewardBound()); result = result && inherited.getSpecification().areRewardBoundedUntilFormulasAllowed(); + if (tbr.hasRewardAccumulation()) { + result = result && inherited.getSpecification().isRewardAccumulationAllowed(); + } } } @@ -118,6 +121,7 @@ namespace storm { bool result = inherited.getSpecification().areCumulativeRewardFormulasAllowed(); result = result && (!f.isMultiDimensional() || inherited.getSpecification().areMultiDimensionalCumulativeRewardFormulasAllowed()); + result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); for (uint64_t i = 0; i < f.getDimension(); ++i) { auto tbr = f.getTimeBoundReference(i); if (tbr.isStepBound()) { @@ -127,6 +131,9 @@ namespace storm { } else { assert(tbr.isRewardBound()); result = result && inherited.getSpecification().areRewardBoundedCumulativeRewardFormulasAllowed(); + if (tbr.hasRewardAccumulation()) { + result = result && inherited.getSpecification().isRewardAccumulationAllowed(); + } } } return result; @@ -140,12 +147,15 @@ namespace storm { if (!inherited.getSpecification().areNestedPathFormulasAllowed()) { result = result && !f.getSubformula().isPathFormula(); } + result = result && !f.hasRewardAccumulation(); } else if (f.isReachabilityRewardFormula()) { result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed(); result = result && f.getSubformula().isStateFormula(); + result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); } else if (f.isReachabilityTimeFormula()) { result = result && inherited.getSpecification().areReachbilityTimeFormulasAllowed(); result = result && f.getSubformula().isStateFormula(); + result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); } result = result && boost::any_cast(f.getSubformula().accept(*this, data)); return result; @@ -250,6 +260,7 @@ namespace storm { result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed()); result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula()); result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation); + if (!inherited.getSpecification().areNestedOperatorsAllowed()) { result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { @@ -258,9 +269,11 @@ namespace storm { return result; } - boost::any FragmentChecker::visit(TotalRewardFormula const&, boost::any const& data) const { + boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); - return inherited.getSpecification().areTotalRewardFormulasAllowed(); + bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed()); + result = result && inherited.getSpecification().areTotalRewardFormulasAllowed(); + return result; } boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index cdcfc6ecd..9b5b8b17e 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -1,6 +1,7 @@ #include "storm/logic/FragmentSpecification.h" #include +#include "storm/logic/RewardAccumulation.h" namespace storm { namespace logic { @@ -161,6 +162,8 @@ namespace storm { operatorAtTopLevelRequired = false; multiObjectiveFormulaAtTopLevelRequired = false; operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false; + + rewardAccumulation = false; } FragmentSpecification FragmentSpecification::copy() const { @@ -564,5 +567,15 @@ namespace storm { return *this; } + bool FragmentSpecification::isRewardAccumulationAllowed() const { + return rewardAccumulation; + } + + FragmentSpecification& FragmentSpecification::setRewardAccumulationAllowed(bool newValue) { + rewardAccumulation = newValue; + return *this; + } + + } } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index d90ebd5fb..012716c78 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -1,8 +1,14 @@ #ifndef STORM_LOGIC_FRAGMENTSPECIFICATION_H_ #define STORM_LOGIC_FRAGMENTSPECIFICATION_H_ +#include +#include + namespace storm { namespace logic { + + class RewardAccumulation; + class FragmentSpecification { public: FragmentSpecification(); @@ -139,6 +145,10 @@ namespace storm { bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const; FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue); + bool isRewardAccumulationAllowed() const; + FragmentSpecification& setRewardAccumulationAllowed(bool newValue); + + FragmentSpecification& setOperatorsAllowed(bool newValue); FragmentSpecification& setTimeAllowed(bool newValue); FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); @@ -195,6 +205,8 @@ namespace storm { bool operatorAtTopLevelRequired; bool multiObjectiveFormulaAtTopLevelRequired; bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired; + + bool rewardAccumulation; }; // Propositional. diff --git a/src/storm/logic/RewardAccumulation.cpp b/src/storm/logic/RewardAccumulation.cpp new file mode 100644 index 000000000..32065268a --- /dev/null +++ b/src/storm/logic/RewardAccumulation.cpp @@ -0,0 +1,51 @@ +#include "storm/logic/RewardAccumulation.h" + +namespace storm { + namespace logic { + + RewardAccumulation::RewardAccumulation(bool steps, bool time, bool exit) : steps(steps), time(time), exit(exit){ + // Intentionally left empty + } + + bool RewardAccumulation::isStepsSet() const { + return steps; + } + + bool RewardAccumulation::isTimeSet() const { + return time; + } + + bool RewardAccumulation::isExitSet() const { + return exit; + } + + bool RewardAccumulation::isEmpty() const { + return !isStepsSet() && !isTimeSet() && !isExitSet(); + } + + std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc) { + bool hasEntry = false; + if (acc.isStepsSet()) { + out << "steps"; + hasEntry = true; + } + if (acc.isTimeSet()) { + if (hasEntry) { + out << ", "; + } + out << "time"; + hasEntry = true; + } + if (acc.isExitSet()) { + if (hasEntry) { + out << ", "; + } + out << "exit"; + hasEntry = true; + } + + return out; + } + + } +} diff --git a/src/storm/logic/RewardAccumulation.h b/src/storm/logic/RewardAccumulation.h new file mode 100644 index 000000000..4f8a50b29 --- /dev/null +++ b/src/storm/logic/RewardAccumulation.h @@ -0,0 +1,27 @@ +#pragma once +#include + +namespace storm { + namespace logic { + + class RewardAccumulation { + public: + RewardAccumulation(bool steps, bool time, bool exit); + RewardAccumulation(RewardAccumulation const& other) = default; + + bool isStepsSet() const; // If set, choice rewards and transition rewards are accumulated upon taking the transition + bool isTimeSet() const; // If set, state rewards are accumulated over time (assuming 0 time passes in discrete-time model states) + bool isExitSet() const; // If set, state rewards are accumulated upon exiting the state + + // Returns true iff accumulation for all types of reward is disabled. + bool isEmpty() const; + + private: + bool time, steps, exit; + }; + + std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc); + + } +} + diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.cpp b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp new file mode 100644 index 000000000..710f959f1 --- /dev/null +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.cpp @@ -0,0 +1,153 @@ +#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" + +namespace storm { + namespace logic { + + RewardAccumulationEliminationVisitor::RewardAccumulationEliminationVisitor(storm::jani::Model const& model) : model(model) { + // Intentionally left empty + } + + std::shared_ptr RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const { + boost::any result = f.accept(*this, boost::any()); + return boost::any_cast>(result); + } + + 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) { + if (f.hasLowerBound(i)) { + lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i))); + } else { + lowerBounds.emplace_back(); + } + if (f.hasUpperBound(i)) { + upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i))); + } else { + upperBounds.emplace_back(); + } + storm::logic::TimeBoundReference tbr = f.getTimeBoundReference(i); + if (tbr.hasRewardAccumulation() && canEliminate(tbr.getRewardAccumulation(), tbr.getRewardName())) { + // Eliminate accumulation + tbr = storm::logic::TimeBoundReference(tbr.getRewardName(), boost::none); + } + timeBoundReferences.push_back(std::move(tbr)); + } + if (f.hasMultiDimensionalSubformulas()) { + std::vector> leftSubformulas, rightSubformulas; + for (uint64_t i = 0; i < f.getDimension(); ++i) { + leftSubformulas.push_back(boost::any_cast>(f.getLeftSubformula(i).accept(*this, data))); + rightSubformulas.push_back(boost::any_cast>(f.getRightSubformula(i).accept(*this, data))); + } + return std::static_pointer_cast(std::make_shared(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences)); + } else { + std::shared_ptr left = boost::any_cast>(f.getLeftSubformula().accept(*this, data)); + std::shared_ptr right = boost::any_cast>(f.getRightSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(left, right, lowerBounds, upperBounds, timeBoundReferences)); + } + } + + 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); + if (f.hasRewardAccumulation() && !canEliminate(f.getRewardAccumulation(), rewName)) { + rewAcc = f.getRewardAccumulation(); + } + + std::vector bounds; + std::vector timeBoundReferences; + for (uint64_t i = 0; i < f.getDimension(); ++i) { + bounds.emplace_back(TimeBound(f.isBoundStrict(i), f.getBound(i))); + storm::logic::TimeBoundReference tbr = f.getTimeBoundReference(i); + if (tbr.hasRewardAccumulation() && canEliminate(tbr.getRewardAccumulation(), tbr.getRewardName())) { + // Eliminate accumulation + tbr = storm::logic::TimeBoundReference(tbr.getRewardName(), boost::none); + } + timeBoundReferences.push_back(std::move(tbr)); + } + return std::static_pointer_cast(std::make_shared(bounds, timeBoundReferences, rewAcc)); + } + + 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 (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 (!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()) { + 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 (!canEliminate(f.getRewardAccumulation(), rewName)) { + return std::static_pointer_cast(std::make_shared(subformula, f.getContext(), f.getRewardAccumulation())); + } + } + } + return std::static_pointer_cast(std::make_shared(subformula, f.getContext())); + } + + 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())); + } + + 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)) { + return std::static_pointer_cast(std::make_shared()); + } else { + return std::static_pointer_cast(std::make_shared(f.getRewardAccumulation())); + } + } + + 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; + } + assignmentKinds = storm::jani::AssignmentsFinder().find(model, transientVar); + if ((assignmentKinds.hasEdgeAssignment || assignmentKinds.hasEdgeDestinationAssignment) && !accumulation.isStepsSet()) { + return false; + } + if (assignmentKinds.hasLocationAssignment) { + if (model.isDiscreteTimeModel()) { + if (!accumulation.isExitSet()) { + return false; + } + // accumulating over time in discrete time models has no effect, i.e., the value of accumulation.isTimeSet() does not matter here. + } else { + if (accumulation.isExitSet() || !accumulation.isTimeSet()) { + return false; + } + } + } + return true; + } + } +} diff --git a/src/storm/logic/RewardAccumulationEliminationVisitor.h b/src/storm/logic/RewardAccumulationEliminationVisitor.h new file mode 100644 index 000000000..0b77901d9 --- /dev/null +++ b/src/storm/logic/RewardAccumulationEliminationVisitor.h @@ -0,0 +1,39 @@ +#pragma once + +#include +#include + +#include "storm/logic/CloneVisitor.h" +#include "storm/logic/RewardAccumulation.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" + +namespace storm { + namespace logic { + + class RewardAccumulationEliminationVisitor : public CloneVisitor { + public: + 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; + virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override; + virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; + + + private: + bool canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional rewardModelName) const; + + storm::jani::Model const& model; + }; + + } +} diff --git a/src/storm/logic/TimeBoundType.h b/src/storm/logic/TimeBoundType.h index 0bd6aba0c..ec9a753b0 100644 --- a/src/storm/logic/TimeBoundType.h +++ b/src/storm/logic/TimeBoundType.h @@ -1,5 +1,9 @@ #pragma once +#include + +#include "storm/logic/RewardAccumulation.h" + namespace storm { namespace logic { @@ -13,14 +17,15 @@ namespace storm { class TimeBoundReference { TimeBoundType type; std::string rewardName; - + boost::optional rewardAccumulation; + public: explicit TimeBoundReference(TimeBoundType t) : type(t) { // For rewards, use the other constructor. assert(t != TimeBoundType::Reward); } - explicit TimeBoundReference(std::string const& rewardName) : type(TimeBoundType::Reward), rewardName(rewardName) { + explicit TimeBoundReference(std::string const& rewardName, boost::optional rewardAccumulation = boost::none) : type(TimeBoundType::Reward), rewardName(rewardName), rewardAccumulation(rewardAccumulation) { assert(rewardName != ""); // Empty reward name is reserved. } @@ -44,6 +49,16 @@ namespace storm { assert(isRewardBound()); return rewardName; } + + bool hasRewardAccumulation() const { + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& getRewardAccumulation() const { + assert(isRewardBound()); + return rewardAccumulation.get(); + } + }; diff --git a/src/storm/logic/TotalRewardFormula.cpp b/src/storm/logic/TotalRewardFormula.cpp index 18c79cd67..6136581a3 100644 --- a/src/storm/logic/TotalRewardFormula.cpp +++ b/src/storm/logic/TotalRewardFormula.cpp @@ -4,7 +4,7 @@ namespace storm { namespace logic { - TotalRewardFormula::TotalRewardFormula() { + TotalRewardFormula::TotalRewardFormula(boost::optional rewardAccumulation) : rewardAccumulation(rewardAccumulation) { // Intentionally left empty. } @@ -16,6 +16,14 @@ namespace storm { return true; } + bool TotalRewardFormula::hasRewardAccumulation() const { + return rewardAccumulation.is_initialized(); + } + + RewardAccumulation const& TotalRewardFormula::getRewardAccumulation() const { + return rewardAccumulation.get(); + } + boost::any TotalRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } diff --git a/src/storm/logic/TotalRewardFormula.h b/src/storm/logic/TotalRewardFormula.h index 90caee9e7..a11fb3b03 100644 --- a/src/storm/logic/TotalRewardFormula.h +++ b/src/storm/logic/TotalRewardFormula.h @@ -1,15 +1,16 @@ #ifndef STORM_LOGIC_TOTALREWARDFORMULA_H_ #define STORM_LOGIC_TOTALREWARDFORMULA_H_ -#include +#include +#include "storm/logic/RewardAccumulation.h" #include "storm/logic/PathFormula.h" namespace storm { namespace logic { class TotalRewardFormula : public PathFormula { public: - TotalRewardFormula(); + TotalRewardFormula(boost::optional rewardAccumulation = boost::none); virtual ~TotalRewardFormula() { // Intentionally left empty. @@ -17,11 +18,15 @@ namespace storm { virtual bool isTotalRewardFormula() const override; virtual bool isRewardPathFormula() const override; - + bool hasRewardAccumulation() const; + RewardAccumulation const& getRewardAccumulation() const; + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual std::ostream& writeToStream(std::ostream& out) const override; - + + private: + boost::optional rewardAccumulation; }; } } diff --git a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp index 7f45240d7..d49b864dd 100644 --- a/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp +++ b/src/storm/storage/expressions/SyntacticalEqualityCheckVisitor.cpp @@ -93,7 +93,7 @@ namespace storm { boost::any SyntacticalEqualityCheckVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) { BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); - if (otherBaseExpression.isBinaryBooleanFunctionExpression()) { + if (otherBaseExpression.isUnaryBooleanFunctionExpression()) { UnaryBooleanFunctionExpression const& otherExpression = otherBaseExpression.asUnaryBooleanFunctionExpression(); bool result = expression.getOperatorType() == otherExpression.getOperatorType(); @@ -108,7 +108,7 @@ namespace storm { boost::any SyntacticalEqualityCheckVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) { BaseExpression const& otherBaseExpression = boost::any_cast>(data).get(); - if (otherBaseExpression.isBinaryBooleanFunctionExpression()) { + if (otherBaseExpression.isUnaryNumericalFunctionExpression()) { UnaryNumericalFunctionExpression const& otherExpression = otherBaseExpression.asUnaryNumericalFunctionExpression(); bool result = expression.getOperatorType() == otherExpression.getOperatorType(); diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index cc75d080e..62d2576cf 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -270,6 +270,10 @@ namespace storm { return ConstEdges(it1, it2); } + EdgeContainer const& Automaton::getEdgeContainer() const { + return edges; + } + void Automaton::addEdge(Edge const& edge) { STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'."); assert(validate()); diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index eb1362741..869f5cd09 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -192,6 +192,8 @@ namespace storm { */ ConstEdges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const; + EdgeContainer const& getEdgeContainer() const; + /*! * Adds the template edge to the list of edges */ diff --git a/src/storm/storage/jani/EdgeContainer.cpp b/src/storm/storage/jani/EdgeContainer.cpp index b7a9ca1ec..d735bc80d 100644 --- a/src/storm/storage/jani/EdgeContainer.cpp +++ b/src/storm/storage/jani/EdgeContainer.cpp @@ -121,8 +121,6 @@ namespace storm { } - - std::vector & EdgeContainer::getConcreteEdges() { return edges; } @@ -130,6 +128,10 @@ namespace storm { std::vector const& EdgeContainer::getConcreteEdges() const { return edges; } + + TemplateEdgeContainer const& EdgeContainer::getTemplateEdges() const { + return templates; + } std::set EdgeContainer::getActionIndices() const { std::set result; diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h index f4738e1e0..c2bdfe80c 100644 --- a/src/storm/storage/jani/EdgeContainer.h +++ b/src/storm/storage/jani/EdgeContainer.h @@ -95,6 +95,8 @@ namespace storm { void clearConcreteEdges(); std::vector const& getConcreteEdges() const; std::vector & getConcreteEdges(); + TemplateEdgeContainer const& getTemplateEdges() const; + size_t size() const; iterator begin(); diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index c957cd29b..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,9 +155,58 @@ namespace storm { return iDecl; } - modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model) { + 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()) { + res.push_back("steps"); + } + if (rewardAccumulation.isTimeSet()) { + res.push_back("time"); + } + if (rewardAccumulation.isExitSet()) { + stateExitRewards = true; + res.push_back("exit"); + } + return res; + } + + modernjson::json FormulaToJaniJson::constructStandardRewardAccumulation(std::string const& rewardModelName) const { + if (model.isDiscreteTimeModel()) { + return constructRewardAccumulation(storm::logic::RewardAccumulation(true, false, true), rewardModelName); + } else { + return constructRewardAccumulation(storm::logic::RewardAccumulation(true, true, false), rewardModelName); + } + } + + modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model, std::set& modelFeatures) { FormulaToJaniJson translator(model); - return boost::any_cast(formula.accept(translator)); + auto result = boost::any_cast(formula.accept(translator)); + if (translator.containsStateExitRewards()) { + modelFeatures.insert("state-exit-rewards"); + } + return result; + } + + bool FormulaToJaniJson::containsStateExitRewards() const { + return stateExitRewards; } boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const&) const { @@ -209,11 +260,11 @@ namespace storm { } else if(tbr.isRewardBound()) { modernjson::json rewbound; rewbound["exp"] = tbr.getRewardName(); - std::vector accvec = {"steps"}; - if (!model.isDiscreteTimeModel()) { - accvec.push_back("time"); + if (tbr.hasRewardAccumulation()) { + rewbound["accumulate"] = constructRewardAccumulation(tbr.getRewardAccumulation(), tbr.getRewardName()); + } else { + rewbound["accumulate"] = constructStandardRewardAccumulation(tbr.getRewardName()); } - rewbound["accumulate"] = modernjson::json(accvec); rewbound["bounds"] = propertyInterval; rewardBounds.push_back(std::move(rewbound)); } else { @@ -247,12 +298,14 @@ namespace storm { boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const { modernjson::json opDecl; - std::vector accvec; - if (model.isDiscreteTimeModel()) { - accvec.push_back("steps"); - } else { - accvec.push_back("time"); + + // Create standard reward accumulation for time operator formulas. + storm::logic::RewardAccumulation rewAcc(model.isDiscreteTimeModel(), !model.isDiscreteTimeModel(), false); + if (f.getSubformula().isEventuallyFormula() && f.getSubformula().asEventuallyFormula().hasRewardAccumulation()) { + rewAcc = f.getSubformula().asEventuallyFormula().getRewardAccumulation(); } + auto rewAccJson = constructRewardAccumulation(rewAcc); + if(f.hasBound()) { auto bound = f.getBound(); opDecl["op"] = comparisonTypeToJani(bound.comparisonType); @@ -268,7 +321,7 @@ namespace storm { opDecl["left"]["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); } opDecl["left"]["exp"] = modernjson::json(1); - opDecl["left"]["accumulate"] = modernjson::json(accvec); + opDecl["left"]["accumulate"] = rewAccJson; opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables()); } else { if(f.hasOptimalityType()) { @@ -284,7 +337,7 @@ namespace storm { opDecl["reach"] = boost::any_cast(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data)); } opDecl["exp"] = modernjson::json(1); - opDecl["accumulate"] = modernjson::json(accvec); + opDecl["accumulate"] = rewAccJson; } return opDecl; } @@ -401,12 +454,11 @@ namespace storm { boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const { modernjson::json opDecl; - std::vector accvec = {"steps"}; + std::string instantName; if (model.isDiscreteTimeModel()) { instantName = "step-instant"; } else { - accvec.push_back("time"); instantName = "time-instant"; } @@ -436,21 +488,29 @@ 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(), rewardModelName); + } else { + 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(), rewardModelName); + } else { + opDecl["left"]["accumulate"] = constructStandardRewardAccumulation(rewardModelName); + } } else if (f.getSubformula().isInstantaneousRewardFormula()) { opDecl["left"][instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); } STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion"); opDecl["left"]["exp"] = rewardModelName; - if (f.getSubformula().isReachabilityRewardFormula() || f.getSubformula().isCumulativeRewardFormula()) { - opDecl["left"]["accumulate"] = modernjson::json(accvec); - } opDecl["right"] = buildExpression(bound.threshold, model.getConstants(), model.getGlobalVariables()); } else { if (f.hasOptimalityType()) { opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; - } else { // TODO add checks opDecl["op"] = "Emin"; @@ -458,16 +518,24 @@ 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(), rewardModelName); + } else { + 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(), rewardModelName); + } else { + opDecl["accumulate"] = constructStandardRewardAccumulation(rewardModelName); + } } else if (f.getSubformula().isInstantaneousRewardFormula()) { opDecl[instantName] = buildExpression(f.getSubformula().asInstantaneousRewardFormula().getBound(), model.getConstants(), model.getGlobalVariables()); } - opDecl["exp"] = rewardModelName; - if (f.getSubformula().isReachabilityRewardFormula() || f.getSubformula().isCumulativeRewardFormula()) { - opDecl["accumulate"] = modernjson::json(accvec); - } } return opDecl; } @@ -841,8 +909,8 @@ namespace storm { return modernjson::json(automataDeclarations); } - void JsonExporter::convertModel(storm::jani::Model const& janiModel, bool commentExpressions) { + modelFeatures = {"derived-operators"}; jsonStruct["jani-version"] = janiModel.getJaniVersion(); jsonStruct["name"] = janiModel.getName(); jsonStruct["type"] = to_string(janiModel.getModelType()); @@ -852,14 +920,8 @@ namespace storm { jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction(), janiModel.getConstants(), janiModel.getGlobalVariables()); jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap(), janiModel.getConstants(), janiModel.getGlobalVariables(), commentExpressions); jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition()); - std::vector standardFeatureVector = {"derived-operators"}; - jsonStruct["features"] = standardFeatureVector; - } - - - std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { switch(ft) { case storm::modelchecker::FilterType::MIN: @@ -888,12 +950,12 @@ namespace storm { } } - modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model) { + modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model, std::set& modelFeatures) { modernjson::json propDecl; propDecl["states"]["op"] = "initial"; propDecl["op"] = "filter"; propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); - propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), model); + propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), model, modelFeatures); return propDecl; } @@ -904,7 +966,7 @@ namespace storm { for(auto const& f : formulas) { modernjson::json propDecl; propDecl["name"] = f.getName(); - propDecl["expression"] = convertFilterExpression(f.getFilter(), model); + propDecl["expression"] = convertFilterExpression(f.getFilter(), model, modelFeatures); ++index; properties.push_back(propDecl); } diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index f88bb7330..1f1a49db8 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -41,7 +41,8 @@ namespace storm { class FormulaToJaniJson : public storm::logic::FormulaVisitor { public: - static modernjson::json translate(storm::logic::Formula const& formula, storm::jani::Model const& modeln); + static modernjson::json translate(storm::logic::Formula const& formula, storm::jani::Model const& model, std::set& modelFeatures); + bool containsStateExitRewards() const; // Returns true iff the previously translated formula contained state exit rewards virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const; @@ -64,11 +65,16 @@ namespace storm { virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const; private: - FormulaToJaniJson(storm::jani::Model const& model) : model(model) { } + FormulaToJaniJson(storm::jani::Model const& model) : model(model), stateExitRewards(false) { } 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 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; }; class JsonExporter { @@ -85,11 +91,13 @@ namespace storm { void appendVariableDeclaration(storm::jani::Variable const& variable); modernjson::json finalize() { + std::vector featureVector(modelFeatures.begin(), modelFeatures.end()); + jsonStruct["features"] = featureVector; return jsonStruct; } modernjson::json jsonStruct; - + std::set modelFeatures; }; } diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp new file mode 100644 index 000000000..f1450d004 --- /dev/null +++ b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp @@ -0,0 +1,47 @@ +#include "storm/storage/jani/traverser/AssignmentsFinder.h" + + +namespace storm { + namespace jani { + + AssignmentsFinder::ResultType AssignmentsFinder::find(Model const& model, Variable const& variable) { + ResultType res; + res.hasLocationAssignment = false; + res.hasEdgeAssignment = false; + res.hasEdgeDestinationAssignment = false; + JaniTraverser::traverse(model, std::make_pair(&variable, &res)); + return res; + } + + void AssignmentsFinder::traverse(Location const& location, boost::any const& data) const { + auto resVar = boost::any_cast>(data); + for (auto const& assignment : location.getAssignments()) { + if (assignment.getVariable() == *resVar.first) { + resVar.second->hasLocationAssignment = true; + } + } + JaniTraverser::traverse(location, data); + } + + void AssignmentsFinder::traverse(TemplateEdge const& templateEdge, boost::any const& data) const { + auto resVar = boost::any_cast>(data); + for (auto const& assignment : templateEdge.getAssignments()) { + if (assignment.getVariable() == *resVar.first) { + resVar.second->hasEdgeAssignment = true; + } + } + JaniTraverser::traverse(templateEdge, data); + } + + void AssignmentsFinder::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const { + auto resVar = boost::any_cast>(data); + for (auto const& assignment : templateEdgeDestination.getOrderedAssignments()) { + if (assignment.getVariable() == *resVar.first) { + resVar.second->hasEdgeDestinationAssignment = true; + } + } + JaniTraverser::traverse(templateEdgeDestination, data); + } + } +} + diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.h b/src/storm/storage/jani/traverser/AssignmentsFinder.h new file mode 100644 index 000000000..2a2d2cdd0 --- /dev/null +++ b/src/storm/storage/jani/traverser/AssignmentsFinder.h @@ -0,0 +1,29 @@ +#pragma once + + +#include + +#include "storm/storage/jani/traverser/JaniTraverser.h" + +namespace storm { + namespace jani { + class AssignmentsFinder : public JaniTraverser { + public: + + struct ResultType { + bool hasLocationAssignment, hasEdgeAssignment, hasEdgeDestinationAssignment; + }; + + AssignmentsFinder() = default; + + ResultType find(Model const& model, Variable const& variable); + + virtual ~AssignmentsFinder() = default; + + virtual void traverse(Location const& location, boost::any const& data) const override; + virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const override; + virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const override; + }; + } +} + diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp new file mode 100644 index 000000000..2461792b5 --- /dev/null +++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp @@ -0,0 +1,138 @@ +#include "storm/storage/jani/traverser/JaniTraverser.h" + + +namespace storm { + namespace jani { + void JaniTraverser::traverse(Model const& model, boost::any const& data) const { + for (auto const& act : model.getActions()) { + traverse(act, data); + } + for (auto const& c : model.getConstants()) { + traverse(c, data); + } + traverse(model.getGlobalVariables(), data); + for (auto const& aut : model.getAutomata()) { + traverse(aut, data); + } + if (model.hasInitialStatesRestriction()) { + traverse(model.getInitialStatesRestriction(), data); + } + } + + void JaniTraverser::traverse(Action const& action, boost::any const& data) const { + // Intentionally left empty. + } + + void JaniTraverser::traverse(Automaton const& automaton, boost::any const& data) const { + traverse(automaton.getVariables(), data); + for (auto const& loc : automaton.getLocations()) { + traverse(loc, data); + } + traverse(automaton.getEdgeContainer(), data); + if (automaton.hasInitialStatesRestriction()) { + traverse(automaton.getInitialStatesRestriction(), data); + } + } + + void JaniTraverser::traverse(Constant const& constant, boost::any const& data) const { + if (constant.isDefined()) { + traverse(constant.getExpression(), data); + } + } + + void JaniTraverser::traverse(VariableSet const& variableSet, boost::any const& data) const { + for (auto const& v : variableSet.getBooleanVariables()) { + traverse(v, data); + } + for (auto const& v : variableSet.getBoundedIntegerVariables()) { + traverse(v, data); + } + for (auto const& v : variableSet.getUnboundedIntegerVariables()) { + traverse(v, data); + } + for (auto const& v : variableSet.getRealVariables()) { + traverse(v, data); + } + } + + void JaniTraverser::traverse(Location const& location, boost::any const& data) const { + traverse(location.getAssignments(), data); + } + + void JaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) const { + if (variable.hasInitExpression()) { + traverse(variable.getInitExpression(), data); + } + } + + void JaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any const& data) const { + if (variable.hasInitExpression()) { + traverse(variable.getInitExpression(), data); + } + traverse(variable.getLowerBound(), data); + traverse(variable.getUpperBound(), data); + } + + void JaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const { + if (variable.hasInitExpression()) { + traverse(variable.getInitExpression(), data); + } + } + + void JaniTraverser::traverse(RealVariable const& variable, boost::any const& data) const { + if (variable.hasInitExpression()) { + traverse(variable.getInitExpression(), data); + } + } + + void JaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) const { + for (auto const& templateEdge : edgeContainer.getTemplateEdges()) { + traverse(*templateEdge, data); + } + for (auto const& concreteEdge : edgeContainer.getConcreteEdges()) { + traverse(concreteEdge, data); + } + } + + void JaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any const& data) const { + traverse(templateEdge.getGuard(), data); + for (auto const& dest : templateEdge.getDestinations()) { + traverse(dest, data); + } + traverse(templateEdge.getAssignments(), data); + } + + void JaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const { + traverse(templateEdgeDestination.getOrderedAssignments(), data); + } + + void JaniTraverser::traverse(Edge const& edge, boost::any const& data) const { + if (edge.hasRate()) { + traverse(edge.getRate(), data); + } + for (auto const& dest : edge.getDestinations()) { + traverse(dest, data); + } + } + + void JaniTraverser::traverse(EdgeDestination const& edgeDestination, boost::any const& data) const { + traverse(edgeDestination.getProbability(), data); + } + + void JaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const { + for (auto const& assignment : orderedAssignments) { + traverse(assignment, data); + } + } + + void JaniTraverser::traverse(Assignment const& assignment, boost::any const& data) const { + traverse(assignment.getAssignedExpression(), data); + } + + void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const { + // intentionally left empty. + } + + } +} + diff --git a/src/storm/storage/jani/traverser/JaniTraverser.h b/src/storm/storage/jani/traverser/JaniTraverser.h new file mode 100644 index 000000000..905ad0208 --- /dev/null +++ b/src/storm/storage/jani/traverser/JaniTraverser.h @@ -0,0 +1,36 @@ +#pragma once + + +#include + +#include "storm/storage/jani/Model.h" + +namespace storm { + namespace jani { + class JaniTraverser { + public: + virtual ~JaniTraverser() = default; + + virtual void traverse(Model const& model, boost::any const& data) const; + + virtual void traverse(Action const& action, boost::any const& data) const; + virtual void traverse(Automaton const& automaton, boost::any const& data) const; + virtual void traverse(Constant const& constant, boost::any const& data) const; + virtual void traverse(VariableSet const& variableSet, boost::any const& data) const; + virtual void traverse(Location const& location, boost::any const& data) const; + virtual void traverse(BooleanVariable const& variable, boost::any const& data) const; + virtual void traverse(BoundedIntegerVariable const& variable, boost::any const& data) const; + virtual void traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const; + virtual void traverse(RealVariable const& variable, boost::any const& data) const; + virtual void traverse(EdgeContainer const& edgeContainer, boost::any const& data) const; + virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const; + virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const; + virtual void traverse(Edge const& edge, boost::any const& data) const; + virtual void traverse(EdgeDestination const& edgeDestination, boost::any const& data) const; + virtual void traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const; + virtual void traverse(Assignment const& assignment, boost::any const& data) const; + virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) const; + }; + } +} +