diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index d6481618e..0afe7b147 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -207,7 +207,16 @@ namespace storm { if(tvarcount == 1) { transientVar = getBoolean(variableStructure.at("transient"), "transient-attribute in variable '" + name + "' (scope: " + scopeDescription + ") "); } + size_t initvalcount = variableStructure.count("initial-value"); + if(transientVar) { + STORM_LOG_THROW(initvalcount == 1, storm::exceptions::InvalidJaniException, "Initial value must be given once for transient variable '" + name + "' (scope: " + scopeDescription + ") "+ name + "' (scope: " + scopeDescription + ") "); + } else { + STORM_LOG_THROW(initvalcount <= 1, storm::exceptions::InvalidJaniException, "Initial value can be given at most one for variable " + name + "' (scope: " + scopeDescription + ")"); + } + boost::optional initValue; + if(initvalcount == 1) { + } STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration."); if(variableStructure.at("type").is_object()) { diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp index e2d5facb4..ad7a1de51 100644 --- a/src/storage/jani/Variable.cpp +++ b/src/storage/jani/Variable.cpp @@ -6,11 +6,16 @@ namespace storm { namespace jani { - - Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : name(name), variable(variable), transient(transient) { + + Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& init, bool transient) : name(name), variable(variable), transient(transient), init(init) { // Intentionally left empty. } - + + Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : name(name), variable(variable), transient(transient), init() { + // Intentionally left empty. + } + + storm::expressions::Variable const& Variable::getExpressionVariable() const { return variable; } @@ -34,6 +39,14 @@ namespace storm { bool Variable::isTransientVariable() const { return transient; } + + bool Variable::hasInitExpression() const { + return static_cast(init); + } + + storm::expressions::Expression const& Variable::getInitExpression() const { + return this->init.get(); + } BooleanVariable& Variable::asBooleanVariable() { return dynamic_cast(*this); diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h index 197cfff65..884bf8d9b 100644 --- a/src/storage/jani/Variable.h +++ b/src/storage/jani/Variable.h @@ -2,6 +2,7 @@ #include #include +#include #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/Expression.h" @@ -16,7 +17,12 @@ namespace storm { class Variable { public: /*! - * Creates a new variable. + * Creates a new variable with initial value construct + */ + Variable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& init, bool transient = false); + + /*! + * Creates a new variable without initial value construct. */ Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient = false); @@ -29,6 +35,20 @@ namespace storm { * Retrieves the name of the variable. */ std::string const& getName() const; + + /*! + * Retrieves whether an initial expression is set. + */ + bool hasInitExpression() const; + + /*! + * Retrieves the initial expression + * Should only be called if an initial expression is set for this variable. + * + * @see hasInitExpression() + */ + storm::expressions::Expression const& getInitExpression() const; + // Methods to determine the type of the variable. virtual bool isBooleanVariable() const; @@ -54,6 +74,9 @@ namespace storm { /// Whether this is a transient variable. bool transient; + + /// Expression for initial values + boost::optional init; }; }