diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp index adf12b165..39ea86304 100644 --- a/src/storage/prism/BooleanVariable.cpp +++ b/src/storage/prism/BooleanVariable.cpp @@ -2,11 +2,11 @@ namespace storm { namespace prism { - BooleanVariable::BooleanVariable(std::string const& variableName) : BooleanVariable(variableName, storm::expressions::Expression::createFalse()) { + BooleanVariable::BooleanVariable(std::string const& variableName) : Variable(variableName, storm::expressions::Expression::createFalse(), true) { // Nothing to do here. } - BooleanVariable::BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression) { + BooleanVariable::BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression, false) { // Nothing to do here. } diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index 7f11a8bc2..10a3f3e88 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -2,11 +2,11 @@ namespace storm { namespace prism { - IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression) : IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, lowerBoundExpression) { + IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression) : Variable(variableName, lowerBoundExpression, true), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { // Intentionally left empty. } - IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { + IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression) : Variable(variableName, initialValueExpression, false), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) { // Intentionally left empty. } @@ -23,7 +23,7 @@ namespace storm { } std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) { - stream << this->getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << variable.getInitialValueExpression() << ";"; + stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << variable.getInitialValueExpression() << ";"; return stream; } } // namespace prism diff --git a/src/storage/prism/Variable.cpp b/src/storage/prism/Variable.cpp index 9527e7f76..a6f6f57ae 100644 --- a/src/storage/prism/Variable.cpp +++ b/src/storage/prism/Variable.cpp @@ -4,11 +4,11 @@ namespace storm { namespace prism { - Variable::Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression) : variableName(variableName), initialValueExpression(initialValueExpression) { + Variable::Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue) : variableName(variableName), initialValueExpression(initialValueExpression), defaultInitialValue(defaultInitialValue) { // Nothing to do here. } - Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map const& renaming) : variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)) { + Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map const& renaming) : variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) { // Intentionally left empty. } @@ -16,6 +16,10 @@ namespace storm { return variableName; } + bool Variable::hasDefaultInitialValue() const { + return this->defaultInitialValue; + } + storm::expressions::Expression const& Variable::getInitialValueExpression() const { return this->initialValueExpression; } diff --git a/src/storage/prism/Variable.h b/src/storage/prism/Variable.h index 248a0e533..ef77a2c2d 100644 --- a/src/storage/prism/Variable.h +++ b/src/storage/prism/Variable.h @@ -28,7 +28,14 @@ namespace storm { * @return The expression defining the initial value of the variable. */ storm::expressions::Expression const& getInitialValueExpression() const; - + + /*! + * Retrieves whether the variable has the default initial value with respect to its type. + * + * @return True iff the variable has the default initial value. + */ + bool hasDefaultInitialValue() const; + // Make the constructors protected to forbid instantiation of this class. protected: Variable() = default; @@ -38,8 +45,10 @@ namespace storm { * * @param variableName The name of the variable. * @param initialValueExpression The constant expression that defines the initial value of the variable. + * @param hasDefaultInitialValue A flag indicating whether the initial value of the variable is its default + * value. */ - Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression); + Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue); /*! * Creates a copy of the given variable and performs the provided renaming. @@ -56,6 +65,9 @@ namespace storm { // The constant expression defining the initial value of the variable. storm::expressions::Expression initialValueExpression; + + // A flag that stores whether the variable has its default initial expression. + bool defaultInitialValue; }; } // namespace prism