Added type check visitor to validate types of identifiers in expressions. Started writing validation method on PRISM program class.

Former-commit-id: 6416bea711

src/storage/expressions/Expression.cpp

@@ -4,6 +4,7 @@
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/SubstitutionVisitor.h"
 #include "src/storage/expressions/IdentifierSubstitutionVisitor.h"
+#include "src/storage/expressions/TypeCheckVisitor.h"
 #include "src/exceptions/InvalidTypeException.h"
 #include "src/exceptions/ExceptionMacros.h"
 
@@ -28,21 +29,29 @@ namespace storm {
         }
         
 		Expression Expression::substitute(std::map<std::string, Expression> const& identifierToExpressionMap) const {
-            return SubstitutionVisitor< std::map<std::string, Expression> >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
+            return SubstitutionVisitor<std::map<std::string, Expression>>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
         }
 
 		Expression Expression::substitute(std::unordered_map<std::string, Expression> const& identifierToExpressionMap) const {
-			return SubstitutionVisitor< std::unordered_map<std::string, Expression> >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
+			return SubstitutionVisitor<std::unordered_map<std::string, Expression>>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get());
 		}
         
 		Expression Expression::substitute(std::map<std::string, std::string> const& identifierToIdentifierMap) const {
-			return IdentifierSubstitutionVisitor< std::map<std::string, std::string> >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
+			return IdentifierSubstitutionVisitor<std::map<std::string, std::string>>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
         }
 
 		Expression Expression::substitute(std::unordered_map<std::string, std::string> const& identifierToIdentifierMap) const {
-			return IdentifierSubstitutionVisitor< std::unordered_map<std::string, std::string> >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
+			return IdentifierSubstitutionVisitor<std::unordered_map<std::string, std::string>>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
 		}
         
+        void Expression::check(std::map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const {
+            return TypeCheckVisitor<std::map<std::string, storm::expressions::ExpressionReturnType>>(identifierToTypeMap).check(this->getBaseExpressionPointer().get());
+        }
+
+        void Expression::check(std::unordered_map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const {
+            return TypeCheckVisitor<std::unordered_map<std::string, storm::expressions::ExpressionReturnType>>(identifierToTypeMap).check(this->getBaseExpressionPointer().get());
+        }
+
         bool Expression::evaluateAsBool(Valuation const* valuation) const {
             return this->getBaseExpression().evaluateAsBool(valuation);
         }
@@ -79,6 +88,13 @@ namespace storm {
             return this->getBaseExpression().getConstants();
         }
         
+        std::set<std::string> Expression::getIdentifiers() const {
+            std::set<std::string> result = this->getConstants();
+            std::set<std::string> variables = this->getVariables();
+            result.insert(variables.begin(), variables.end());
+            return result;
+        }
+        
         BaseExpression const& Expression::getBaseExpression() const {
             return *this->expressionPtr;
         }

src/storage/expressions/Expression.h

@@ -110,6 +110,22 @@ namespace storm {
 			*/
 			Expression substitute(std::unordered_map<std::string, std::string> const& identifierToIdentifierMap) const;
             
+            /*!
+             * Checks that all identifiers appearing in the expression have the types given by the map. An exception
+             * is thrown in case a violation is found.
+             *
+             * @param identifierToTypeMap A mapping from identifiers to the types that are supposed to have.
+             */
+            void check(std::map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const;
+            
+            /*!
+             * Checks that all identifiers appearing in the expression have the types given by the map. An exception
+             * is thrown in case a violation is found.
+             *
+             * @param identifierToTypeMap A mapping from identifiers to the types that are supposed to have.
+             */
+            void check(std::unordered_map<std::string, storm::expressions::ExpressionReturnType> const& identifierToTypeMap) const;
+            
             /*!
              * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
              * valuation and returns the resulting boolean value. If the return type of the expression is not a boolean
@@ -182,6 +198,13 @@ namespace storm {
              */
             std::set<std::string> getConstants() const;
             
+            /*!
+             * Retrieves the set of all identifiers (constants and variables) that appear in the expression.
+             *
+             * @return The est of all identifiers that appear in the expression.
+             */
+            std::set<std::string> getIdentifiers() const;
+            
             /*!
              * Retrieves the base expression underlying this expression object. Note that prior to calling this, the
              * expression object must be properly initialized.

src/storage/expressions/SubstitutionVisitor.cpp

@@ -3,20 +3,7 @@
 #include <string>
 
 #include "src/storage/expressions/SubstitutionVisitor.h"
-
-#include "src/storage/expressions/IfThenElseExpression.h"
-#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
-#include "src/storage/expressions/BinaryRelationExpression.h"
-#include "src/storage/expressions/BooleanConstantExpression.h"
-#include "src/storage/expressions/IntegerConstantExpression.h"
-#include "src/storage/expressions/DoubleConstantExpression.h"
-#include "src/storage/expressions/BooleanLiteralExpression.h"
-#include "src/storage/expressions/IntegerLiteralExpression.h"
-#include "src/storage/expressions/DoubleLiteralExpression.h"
-#include "src/storage/expressions/VariableExpression.h"
-#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
-#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
+#include "src/storage/expressions/Expressions.h"
 
 namespace storm {
     namespace expressions  {

src/storage/expressions/TypeCheckVisitor.cpp

@@ -0,0 +1,97 @@
+#include "src/storage/expressions/TypeCheckVisitor.h"
+#include "src/storage/expressions/Expressions.h"
+
+#include "src/exceptions/ExceptionMacros.h"
+#include "src/exceptions/InvalidTypeException.h"
+
+namespace storm {
+    namespace expressions {
+        template<typename MapType>
+        TypeCheckVisitor<MapType>::TypeCheckVisitor(MapType const& identifierToTypeMap) : identifierToTypeMap(identifierToTypeMap) {
+            // Intentionally left empty.
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::check(BaseExpression const* expression) {
+            expression->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(IfThenElseExpression const* expression) {
+            expression->getCondition()->accept(this);
+            expression->getThenExpression()->accept(this);
+            expression->getElseExpression()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BinaryBooleanFunctionExpression const* expression) {
+            expression->getFirstOperand()->accept(this);
+            expression->getSecondOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BinaryNumericalFunctionExpression const* expression) {
+            expression->getFirstOperand()->accept(this);
+            expression->getSecondOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BinaryRelationExpression const* expression) {
+            expression->getFirstOperand()->accept(this);
+            expression->getSecondOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BooleanConstantExpression const* expression) {
+            auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName());
+            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'.");
+            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected bool, but found " << expression->getReturnType() << ".");
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(DoubleConstantExpression const* expression) {
+            auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName());
+            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'.");
+            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected double, but found " << expression->getReturnType() << ".");
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(IntegerConstantExpression const* expression) {
+            auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName());
+            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'.");
+            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected int, but found " << expression->getReturnType() << ".");
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(VariableExpression const* expression) {
+            auto identifierTypePair = this->identifierToTypeMap.find(expression->getVariableName());
+            LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getVariableName() << "'.");
+            LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for variable '" << expression->getVariableName() << "': expected " << identifierTypePair->first << ", but found " << expression->getReturnType() << ".");
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(UnaryBooleanFunctionExpression const* expression) {
+            expression->getOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(UnaryNumericalFunctionExpression const* expression) {
+            expression->getOperand()->accept(this);
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(BooleanLiteralExpression const* expression) {
+            // Intentionally left empty.
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(IntegerLiteralExpression const* expression) {
+            // Intentionally left empty.
+        }
+        
+        template<typename MapType>
+        void TypeCheckVisitor<MapType>::visit(DoubleLiteralExpression const* expression) {
+            // Intentionally left empty.
+        }
+    }
+}

src/storage/expressions/TypeCheckVisitor.h

@@ -0,0 +1,50 @@
+#ifndef STORM_STORAGE_EXPRESSIONS_TYPECHECKVISITOR_H_
+#define STORM_STORAGE_EXPRESSIONS_TYPECHECKVISITOR_H_
+
+#include <stack>
+
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/ExpressionVisitor.h"
+
+namespace storm {
+    namespace expressions {
+        template<typename MapType>
+        class TypeCheckVisitor : public ExpressionVisitor {
+        public:
+            /*!
+             * Creates a new type check visitor that uses the given map to check the types of variables and constants.
+             *
+             * @param identifierToTypeMap A mapping from identifiers to expressions.
+             */
+            TypeCheckVisitor(MapType const& identifierToTypeMap);
+            
+            /*!
+             * Checks that the types of the identifiers in the given expression match the ones in the previously given
+             * map.
+             *
+             * @param expression The expression in which to check the types.
+             */
+            void check(BaseExpression const* expression);
+            
+            virtual void visit(IfThenElseExpression const* expression) override;
+            virtual void visit(BinaryBooleanFunctionExpression const* expression) override;
+            virtual void visit(BinaryNumericalFunctionExpression const* expression) override;
+            virtual void visit(BinaryRelationExpression const* expression) override;
+            virtual void visit(BooleanConstantExpression const* expression) override;
+            virtual void visit(DoubleConstantExpression const* expression) override;
+            virtual void visit(IntegerConstantExpression const* expression) override;
+            virtual void visit(VariableExpression const* expression) override;
+            virtual void visit(UnaryBooleanFunctionExpression const* expression) override;
+            virtual void visit(UnaryNumericalFunctionExpression const* expression) override;
+            virtual void visit(BooleanLiteralExpression const* expression) override;
+            virtual void visit(IntegerLiteralExpression const* expression) override;
+            virtual void visit(DoubleLiteralExpression const* expression) override;
+            
+        private:            
+            // A mapping of identifier names to expressions with which they shall be replaced.
+            MapType const& identifierToTypeMap;
+        };
+    }
+}
+
+#endif /* STORM_STORAGE_EXPRESSIONS_TYPECHECKVISITOR_H_ */

src/storage/prism/Program.cpp

@@ -1,7 +1,11 @@
 #include "src/storage/prism/Program.h"
+
+#include <algorithm>
+
 #include "src/exceptions/ExceptionMacros.h"
 #include "exceptions/InvalidArgumentException.h"
 #include "src/exceptions/OutOfRangeException.h"
+#include "src/exceptions/WrongFormatException.h"
 
 namespace storm {
     namespace prism {
@@ -317,6 +321,183 @@ namespace storm {
             return Program(this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, newRewardModels, this->definesInitialStatesExpression(), newInitialStateExpression, newLabels);
         }
         
+        void Program::checkValidity() const {
+            // We need to construct a mapping from identifiers to their types, so we can type-check the expressions later.
+            std::map<std::string, storm::expressions::ExpressionReturnType> identifierToTypeMap;
+            
+            // Start by checking the constant declarations.
+            std::set<std::string> allIdentifiers;
+            std::set<std::string> constantNames;
+            for (auto const& constant : this->getConstants()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(constant.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": duplicate identifier '" << constant.getName() << "'.");
+                
+                // Check defining expressions of defined constants.
+                if (constant.isDefined()) {
+                    LOG_THROW(constant.getExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": definition of constant " << constant.getName() << " must not refer to variables.");
+                    
+                    std::set<std::string> containedConstantNames = constant.getExpression().getConstants();
+                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstantNames.begin(), containedConstantNames.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown constants.");
+                    
+                    // Now check that the constants appear with the right types (this throws an exception if this is not
+                    // the case).
+                    constant.getExpression().check(identifierToTypeMap);
+                }
+                
+                // Finally, register the type of the constant for later type checks.
+                identifierToTypeMap.emplace(constant.getName(), constant.getType());
+                
+                // Record the new identifier for future checks.
+                constantNames.insert(constant.getName());
+                allIdentifiers.insert(constant.getName());
+            }
+            
+            // Now we check the variable declarations. We start with the global variables.
+            std::set<std::string> variableNames;
+            for (auto const& variable : this->getGlobalBooleanVariables()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+                
+                // Check the initial value of the variable.
+                LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
+                std::set<std::string> containedConstants = variable.getInitialValueExpression().getConstants();
+                bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+                variable.getInitialValueExpression().check(identifierToTypeMap);
+
+                // Register the type of the constant for later type checks.
+                identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool);
+                
+                // Record the new identifier for future checks.
+                variableNames.insert(variable.getName());
+                allIdentifiers.insert(variable.getName());
+            }
+            for (auto const& variable : this->getGlobalIntegerVariables()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+                
+                // Check that bound expressions of the range.
+                LOG_THROW(variable.getLowerBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression must not refer to variables.");
+                std::set<std::string> containedConstants = variable.getLowerBoundExpression().getConstants();
+                bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
+                variable.getLowerBoundExpression().check(identifierToTypeMap);
+                LOG_THROW(variable.getUpperBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression must not refer to variables.");
+                containedConstants = variable.getLowerBoundExpression().getConstants();
+                isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
+                variable.getUpperBoundExpression().check(identifierToTypeMap);
+                
+                // Check the initial value of the variable.
+                LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
+                containedConstants = variable.getInitialValueExpression().getConstants();
+                isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+                variable.getInitialValueExpression().check(identifierToTypeMap);
+                
+                // Register the type of the constant for later type checks.
+                identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
+
+                // Record the new identifier for future checks.
+                variableNames.insert(variable.getName());
+                allIdentifiers.insert(variable.getName());
+            }
+
+            // Now go through the variables of the modules.
+            for (auto const& module : this->getModules()) {
+                for (auto const& variable : module.getBooleanVariables()) {
+                    // Check for duplicate identifiers.
+                    LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+                    
+                    // Check the initial value of the variable.
+                    LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
+                    std::set<std::string> containedConstants = variable.getInitialValueExpression().getConstants();
+                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+                    variable.getInitialValueExpression().check(identifierToTypeMap);
+                    
+                    // Register the type of the constant for later type checks.
+                    identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool);
+                    
+                    // Record the new identifier for future checks.
+                    variableNames.insert(variable.getName());
+                    allIdentifiers.insert(variable.getName());
+                }
+                for (auto const& variable : module.getIntegerVariables()) {
+                    // Check for duplicate identifiers.
+                    LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
+                    
+                    // Register the type of the constant for later type checks.
+                    identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
+                    
+                    // Check that bound expressions of the range.
+                    LOG_THROW(variable.getLowerBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression must not refer to variables.");
+                    std::set<std::string> containedConstants = variable.getLowerBoundExpression().getConstants();
+                    bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": lower bound expression refers to unknown constants.");
+                    variable.getLowerBoundExpression().check(identifierToTypeMap);
+                    LOG_THROW(variable.getUpperBoundExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression must not refer to variables.");
+                    containedConstants = variable.getLowerBoundExpression().getConstants();
+                    isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": upper bound expression refers to unknown constants.");
+                    variable.getUpperBoundExpression().check(identifierToTypeMap);
+                    
+                    // Check the initial value of the variable.
+                    LOG_THROW(variable.getInitialValueExpression().getVariables().empty(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression must not refer to variables.");
+                    containedConstants = variable.getInitialValueExpression().getConstants();
+                    isValid = std::includes(constantNames.begin(), constantNames.end(), containedConstants.begin(), containedConstants.end());
+                    LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
+                    variable.getInitialValueExpression().check(identifierToTypeMap);
+                    
+                    // Record the new identifier for future checks.
+                    variableNames.insert(variable.getName());
+                    allIdentifiers.insert(variable.getName());
+                }
+            }
+            
+            // Create the set of valid identifiers for future checks.
+            std::set<std::string> variablesAndConstants;
+            std::set_union(variableNames.begin(), variableNames.end(), constantNames.begin(), constantNames.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
+            
+            // TODO: check commands.
+            
+            // TODO: check reward models.
+            
+            // Check the initial states expression (if the program defines it).
+            if (this->hasInitialStatesExpression) {
+                std::set<std::string> containedIdentifiers = this->initialStatesExpression.getIdentifiers();
+                bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << this->getFilename() << ", line " << this->getLineNumber() << ": initial expression refers to unknown identifiers.");
+                this->initialStatesExpression.check(identifierToTypeMap);
+            }
+            
+            // Check the labels.
+            for (auto const& label : this->getLabels()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(label.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": duplicate identifier '" << label.getName() << "'.");
+                
+                std::set<std::string> containedIdentifiers = label.getStatePredicateExpression().getIdentifiers();
+                bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label expression refers to unknown identifiers.");
+                label.getStatePredicateExpression().check(identifierToTypeMap);
+            }
+            
+            // Check the formulas.
+            for (auto const& formula : this->getFormulas()) {
+                // Check for duplicate identifiers.
+                LOG_THROW(allIdentifiers.find(formula.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": duplicate identifier '" << formula.getName() << "'.");
+                
+                std::set<std::string> containedIdentifiers = formula.getExpression().getIdentifiers();
+                bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
+                LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
+                formula.getExpression().check(identifierToTypeMap);
+                
+                // Record the new identifier for future checks.
+                allIdentifiers.insert(formula.getName());
+            }
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Program const& program) {
             switch (program.getModelType()) {
                 case Program::ModelType::UNDEFINED: stream << "undefined"; break;

src/storage/prism/Program.h

@@ -285,6 +285,12 @@ namespace storm {
              */
             Program substituteConstants() const;
             
+            /*!
+             * Checks the validity of the program. If the program is not valid, an exception is thrown with a message
+             * that indicates the source of the problem.
+             */
+            void checkValidity() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Program const& program);
             
         private: