From 5407978e8e9d31ece2e03af4dec29b3fb0595b3e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 7 Apr 2014 17:12:49 +0200
Subject: [PATCH] Minor update: PRISM variables now store whether an initial
value for them was given explicitly in the program.
Former-commit-id: 6672539447630f05052ee073cfd2ccdee767ed5a
---
src/storage/prism/BooleanVariable.cpp | 4 ++--
src/storage/prism/IntegerVariable.cpp | 6 +++---
src/storage/prism/Variable.cpp | 8 ++++++--
src/storage/prism/Variable.h | 16 ++++++++++++++--
4 files changed, 25 insertions(+), 9 deletions(-)
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<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;
}
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