diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index f86f905f5..03b3e3063 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -16,12 +16,22 @@ namespace storm { namespace parser { + //////////// + // Defaults + //////////// + const bool JaniParser::defaultVariableTransient = false; + std::string getString(json const& structure, std::string const& errorInfo) { STORM_LOG_THROW(structure.is_string(), storm::exceptions::InvalidJaniException, "Expected a string in " << errorInfo << ", got '" << structure.dump() << "'"); return structure.front(); } + bool getBoolean(json const& structure, std::string const& errorInfo) { + STORM_LOG_THROW(structure.is_boolean(), storm::exceptions::InvalidJaniException, "Expected a Boolean in " << errorInfo << ", got " << structure.dump() << "'"); + return structure.front(); + } + uint64_t getUnsignedInt(json const& structure, std::string const& errorInfo) { STORM_LOG_THROW(structure.is_number(), storm::exceptions::InvalidJaniException, "Expected a number in " << errorInfo << ", got '" << structure.dump() << "'"); int num = structure.front(); @@ -189,6 +199,13 @@ namespace storm { // TODO check existance of name. // TODO store prefix in variable. std::string exprManagerName = pref + name; + bool transientVar = defaultVariableTransient; // Default value for variables. + size_t tvarcount = variableStructure.count("transient"); + STORM_LOG_THROW(tvarcount <= 1, storm::exceptions::InvalidJaniException, "Multiple definitions of transient not allowed in variable '" + name + "' (scope: " + scopeDescription + ") "); + if(tvarcount == 1) { + transientVar = getBoolean(variableStructure.at("transient"), "transient-attribute in variable '" + name + "' (scope: " + scopeDescription + ") "); + } + 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()) { @@ -207,7 +224,7 @@ namespace storm { if(basictype == "int") { STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed"); - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), lowerboundExpr, upperboundExpr); + return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar, lowerboundExpr, upperboundExpr); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") "); } @@ -220,9 +237,9 @@ namespace storm { // expressionManager->declareRationalVariable(name); // TODO something. } else if(variableStructure.at("type") == "bool") { - return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName)); + return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), transientVar); } else if(variableStructure.at("type") == "int") { - return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName)); + return std::make_shared(name, expressionManager->declareIntegerVariable(exprManagerName), transientVar); } else { // TODO clocks. STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump() << " for Variable '" << name << "' (scope: " << scopeDescription << ")"); diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index 09e195894..1e1d66d66 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -67,6 +67,10 @@ namespace storm { std::shared_ptr expressionManager; + ////////// + // Default values -- assumptions from JANI. + ////////// + static const bool defaultVariableTransient; }; } diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp index 8f4f6f106..56cdf88bd 100644 --- a/src/storage/jani/BooleanVariable.cpp +++ b/src/storage/jani/BooleanVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) { + BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { // Intentionally left empty. } diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h index eacff6fb4..5f7292cbf 100644 --- a/src/storage/jani/BooleanVariable.h +++ b/src/storage/jani/BooleanVariable.h @@ -10,7 +10,7 @@ namespace storm { /*! * Creates a boolean variable. */ - BooleanVariable(std::string const& name, storm::expressions::Variable const& variable); + BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); virtual bool isBooleanVariable() const override; }; diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp index 7ef1774fc..def815616 100644 --- a/src/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storage/jani/BoundedIntegerVariable.cpp @@ -3,10 +3,15 @@ namespace storm { namespace jani { + BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable, transient), lowerBound(lowerBound), upperBound(upperBound) { + // Intentionally left empty. + } + BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) { // Intentionally left empty. } - + + storm::expressions::Expression const& BoundedIntegerVariable::getLowerBound() const { return lowerBound; } diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index bc2298d05..2fa515dec 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -11,8 +11,12 @@ namespace storm { /*! * Creates a bounded integer variable. */ + BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); + /*! + * Creates a bounded integer variable with transient set to false. + */ BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); - + /*! * Retrieves the expression defining the lower bound of the variable. */ diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp index 294dfc549..9b097757d 100644 --- a/src/storage/jani/Property.cpp +++ b/src/storage/jani/Property.cpp @@ -15,7 +15,7 @@ namespace storm { return this->comment; } - std::shared_ptr Property::getFormula() const { + std::shared_ptr const& Property::getFormula() const { return this->formula; } diff --git a/src/storage/jani/UnboundedIntegerVariable.cpp b/src/storage/jani/UnboundedIntegerVariable.cpp index bf8f7615f..686d6debe 100644 --- a/src/storage/jani/UnboundedIntegerVariable.cpp +++ b/src/storage/jani/UnboundedIntegerVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) { + UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { // Intentionally left empty. } diff --git a/src/storage/jani/UnboundedIntegerVariable.h b/src/storage/jani/UnboundedIntegerVariable.h index 585b953d4..38255591b 100644 --- a/src/storage/jani/UnboundedIntegerVariable.h +++ b/src/storage/jani/UnboundedIntegerVariable.h @@ -10,7 +10,7 @@ namespace storm { /*! * Creates an unbounded integer variable. */ - UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable); + UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); virtual bool isUnboundedIntegerVariable() const override; }; diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp index 3bcb8fcd0..e2d5facb4 100644 --- a/src/storage/jani/Variable.cpp +++ b/src/storage/jani/Variable.cpp @@ -7,7 +7,7 @@ namespace storm { namespace jani { - Variable::Variable(std::string const& name, storm::expressions::Variable const& variable) : name(name), variable(variable) { + Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : name(name), variable(variable), transient(transient) { // Intentionally left empty. } @@ -30,6 +30,10 @@ namespace storm { bool Variable::isUnboundedIntegerVariable() const { return false; } + + bool Variable::isTransientVariable() const { + return transient; + } BooleanVariable& Variable::asBooleanVariable() { return dynamic_cast(*this); diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h index 2ef15321b..197cfff65 100644 --- a/src/storage/jani/Variable.h +++ b/src/storage/jani/Variable.h @@ -18,7 +18,7 @@ namespace storm { /*! * Creates a new variable. */ - Variable(std::string const& name, storm::expressions::Variable const& variable); + Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient = false); /*! * Retrieves the associated expression variable @@ -34,6 +34,8 @@ namespace storm { virtual bool isBooleanVariable() const; virtual bool isBoundedIntegerVariable() const; virtual bool isUnboundedIntegerVariable() const; + + virtual bool isTransientVariable() const; // Methods to get the variable as a different type. BooleanVariable& asBooleanVariable(); @@ -49,6 +51,9 @@ namespace storm { // The expression variable associated with this variable. storm::expressions::Variable variable; + + /// Whether this is a transient variable. + bool transient; }; }