Merge branch 'master' into dft_gspn_new

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.

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;

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<std::string> 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<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()) {
@@ -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<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(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<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");
                             }
@@ -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<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(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<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");
                             }
@@ -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<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");
                         }
@@ -317,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);
@@ -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<std::string>(),{},{});
-                        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);

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<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 = {});

src/storm/builder/DdPrismModelBuilder.h

@@ -3,6 +3,7 @@
 
 #include <map>
 #include <boost/optional.hpp>
+#include <boost/variant.hpp>
 
 #include "storm/storage/prism/Program.h"
 

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())

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<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
-            return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext()));
+            if (f.hasRewardAccumulation()) {
+                return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+            } else {
+                return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(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<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
         }
         
-        boost::any CloneVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
-            return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>());
+        boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f));
         }
         
         boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {

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> rewardAccumulation) : timeBoundReferences({timeBoundReference}), bounds({bound}), rewardAccumulation(rewardAccumulation) {
             // Intentionally left empty.
         }
 
-        CumulativeRewardFormula::CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences) : timeBoundReferences(timeBoundReferences), bounds(bounds) {
+        CumulativeRewardFormula::CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences, boost::optional<RewardAccumulation> 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 const> CumulativeRewardFormula::restrictToDimension(unsigned i) const {
             return std::make_shared<CumulativeRewardFormula const>(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())

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<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences);
+            CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time), boost::optional<RewardAccumulation> rewardAccumulation = boost::none);
+            CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences, boost::optional<RewardAccumulation> rewardAccumulation = boost::none);
             
             virtual ~CumulativeRewardFormula() = default;
 
@@ -47,6 +47,9 @@ namespace storm {
             template <typename ValueType>
             ValueType getNonStrictBound() const;
             
+            bool hasRewardAccumulation() const;
+            RewardAccumulation const& getRewardAccumulation() const;
+            
             std::shared_ptr<CumulativeRewardFormula const> restrictToDimension(unsigned i) const;
             
         private:
@@ -54,6 +57,8 @@ namespace storm {
 
             std::vector<TimeBoundReference> timeBoundReferences;
             std::vector<TimeBound> bounds;
+            boost::optional<RewardAccumulation> rewardAccumulation;
+
         };
     }
 }

src/storm/logic/EventuallyFormula.cpp

@@ -6,8 +6,9 @@
 
 namespace storm {
     namespace logic {
-        EventuallyFormula::EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context) : UnaryPathFormula(subformula), context(context) {
+        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 {
@@ -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;
         }
     }

src/storm/logic/EventuallyFormula.h

@@ -1,14 +1,17 @@
 #ifndef STORM_LOGIC_EVENTUALLYFORMULA_H_
 #define STORM_LOGIC_EVENTUALLYFORMULA_H_
 
+#include <boost/optional.hpp>
+
 #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<Formula const> const& subformula, FormulaContext context = FormulaContext::Probability);
+            EventuallyFormula(std::shared_ptr<Formula const> const& subformula, FormulaContext context = FormulaContext::Probability, boost::optional<RewardAccumulation> 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> rewardAccumulation;
         };
     }
 }

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<bool>(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<bool>(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<InheritedInformation const&>(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 {

src/storm/logic/FragmentSpecification.cpp

@@ -1,6 +1,7 @@
 #include "storm/logic/FragmentSpecification.h"
 
 #include <iostream>
+#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;
+        }
+
+        
     }
 }

src/storm/logic/FragmentSpecification.h

@@ -1,8 +1,14 @@
 #ifndef STORM_LOGIC_FRAGMENTSPECIFICATION_H_
 #define STORM_LOGIC_FRAGMENTSPECIFICATION_H_
 
+#include <map>
+#include <string>
+
 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.

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;
+        }
+        
+    }
+}

src/storm/logic/RewardAccumulation.h

@@ -0,0 +1,27 @@
+#pragma once
+#include <iostream>
+
+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);
+
+    }
+}
+

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<Formula> RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<std::shared_ptr<Formula>>(result);
+        }
+        
+        void RewardAccumulationEliminationVisitor::eliminateRewardAccumulations(std::vector<storm::jani::Property>& 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<boost::optional<TimeBound>> lowerBounds, upperBounds;
+            std::vector<TimeBoundReference> 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<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas;
+                for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                    leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula(i).accept(*this, data)));
+                    rightSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula(i).accept(*this, data)));
+                }
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
+            } else {
+                std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+                std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
+            }
+        }
+        
+        boost::any RewardAccumulationEliminationVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
+            boost::optional<storm::logic::RewardAccumulation> 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<boost::optional<std::string>>(data);
+            if (f.hasRewardAccumulation() && !canEliminate(f.getRewardAccumulation(), rewName)) {
+                rewAcc = f.getRewardAccumulation();
+            }
+
+            std::vector<TimeBound> bounds;
+            std::vector<TimeBoundReference> 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<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, rewAcc));
+        }
+        
+        boost::any RewardAccumulationEliminationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
+           std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(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<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+                    } else if (!model.isDiscreteTimeModel() && (!f.getRewardAccumulation().isTimeSet() || f.getRewardAccumulation().isExitSet() || f.getRewardAccumulation().isStepsSet())) {
+                        return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(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<boost::optional<std::string>>(data);
+                    if (!canEliminate(f.getRewardAccumulation(), rewName)) {
+                        return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+                    }
+                }
+            }
+            return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext()));
+        }
+        
+        boost::any RewardAccumulationEliminationVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, f.getOptionalRewardModelName()));
+            return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(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<boost::optional<std::string>>(data);
+            if (f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) {
+                return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>());
+            } else {
+                return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f.getRewardAccumulation()));
+            }
+        }
+        
+        bool RewardAccumulationEliminationVisitor::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> 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;
+        }
+    }
+}

src/storm/logic/RewardAccumulationEliminationVisitor.h

@@ -0,0 +1,39 @@
+#pragma once
+
+#include <unordered_map>
+#include <boost/optional.hpp>
+
+#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<Formula> eliminateRewardAccumulations(Formula const& f) const;
+            
+            void eliminateRewardAccumulations(std::vector<storm::jani::Property>& 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<std::string> rewardModelName) const;
+            
+            storm::jani::Model const& model;
+        };
+        
+    }
+}

src/storm/logic/TimeBoundType.h

@@ -1,5 +1,9 @@
 #pragma once
 
+#include <boost/optional.hpp>
+
+#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> 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> 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();
+            }
+            
         };
 
 

src/storm/logic/TotalRewardFormula.cpp

@@ -4,7 +4,7 @@
 
 namespace storm {
     namespace logic {
-        TotalRewardFormula::TotalRewardFormula() {
+        TotalRewardFormula::TotalRewardFormula(boost::optional<RewardAccumulation> 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);
         }

src/storm/logic/TotalRewardFormula.h

@@ -1,15 +1,16 @@
 #ifndef STORM_LOGIC_TOTALREWARDFORMULA_H_
 #define STORM_LOGIC_TOTALREWARDFORMULA_H_
 
-#include <boost/variant.hpp>
+#include <boost/optional.hpp>
 
+#include "storm/logic/RewardAccumulation.h"
 #include "storm/logic/PathFormula.h"
 
 namespace storm {
     namespace logic {
         class TotalRewardFormula : public PathFormula {
         public:
-            TotalRewardFormula();
+            TotalRewardFormula(boost::optional<RewardAccumulation> 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> rewardAccumulation;
         };
     }
 }

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<std::reference_wrapper<BaseExpression const>>(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<std::reference_wrapper<BaseExpression const>>(data).get();
-            if (otherBaseExpression.isBinaryBooleanFunctionExpression()) {
+            if (otherBaseExpression.isUnaryNumericalFunctionExpression()) {
                 UnaryNumericalFunctionExpression const& otherExpression = otherBaseExpression.asUnaryNumericalFunctionExpression();
                 
                 bool result = expression.getOperatorType() == otherExpression.getOperatorType();

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());

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
              */

src/storm/storage/jani/EdgeContainer.cpp

@@ -121,8 +121,6 @@ namespace storm {
 
         }
 
-
-
         std::vector<Edge> & EdgeContainer::getConcreteEdges() {
             return edges;
         }
@@ -130,6 +128,10 @@ namespace storm {
         std::vector<Edge> const& EdgeContainer::getConcreteEdges() const {
             return edges;
         }
+        
+        TemplateEdgeContainer const& EdgeContainer::getTemplateEdges() const {
+            return templates;
+        }
 
         std::set<uint64_t> EdgeContainer::getActionIndices() const {
             std::set<uint64_t> result;

src/storm/storage/jani/EdgeContainer.h

@@ -95,6 +95,8 @@ namespace storm {
             void clearConcreteEdges();
             std::vector<Edge> const& getConcreteEdges() const;
             std::vector<Edge> & getConcreteEdges();
+            TemplateEdgeContainer const& getTemplateEdges() const;
+            
             size_t size() const;
 
             iterator begin();

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<std::string> 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<std::string>& modelFeatures) {
             FormulaToJaniJson translator(model);
-            return boost::any_cast<modernjson::json>(formula.accept(translator));
+            auto result = boost::any_cast<modernjson::json>(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<std::string> 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<std::string> 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<modernjson::json>(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<modernjson::json>(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<std::string> 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<modernjson::json>(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<modernjson::json>(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<std::string> 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<std::string>& 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);
             }

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<std::string>& 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<storm::expressions::Expression> const& lower, boost::optional<bool> const& lowerExclusive, boost::optional<storm::expressions::Expression> const& upper, boost::optional<bool> 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<std::string> featureVector(modelFeatures.begin(), modelFeatures.end());
+                jsonStruct["features"] = featureVector;
                 return jsonStruct;
             }
             
             modernjson::json jsonStruct;
-            
+            std::set<std::string> modelFeatures;
             
         };
     }

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<std::pair<Variable const*, ResultType*>>(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<std::pair<Variable const*, ResultType*>>(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<std::pair<Variable const*, ResultType*>>(data);
+            for (auto const& assignment : templateEdgeDestination.getOrderedAssignments()) {
+                if (assignment.getVariable() == *resVar.first) {
+                    resVar.second->hasEdgeDestinationAssignment = true;
+                }
+            }
+            JaniTraverser::traverse(templateEdgeDestination, data);
+        }
+    }
+}
+

src/storm/storage/jani/traverser/AssignmentsFinder.h

@@ -0,0 +1,29 @@
+#pragma once
+
+
+#include <boost/any.hpp>
+
+#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;
+        };
+    }
+}
+

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.
+        }
+                
+    }
+}
+

src/storm/storage/jani/traverser/JaniTraverser.h

@@ -0,0 +1,36 @@
+#pragma once
+
+
+#include <boost/any.hpp>
+
+#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;
+        };
+    }
+}
+