Minor update: PRISM variables now store whether an initial value for them was given explicitly in the program.

Former-commit-id: 6672539447

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

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

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<std::string, std::string> const& renaming) : variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute<std::map>(renaming)) {
+        Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming) : variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute<std::map>(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;
         }

src/storage/prism/Variable.h

@@ -29,6 +29,13 @@ namespace storm {
              */
             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