From 83f9832e2dce56d65112a2ae1877db7ebdc264b5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 4 May 2014 21:51:05 +0200 Subject: [PATCH] Added type check visitor to validate types of identifiers in expressions. Started writing validation method on PRISM program class. Former-commit-id: 6416bea711db3cc55296f04bda77e0e69ed74491 --- src/storage/expressions/Expression.cpp | 24 ++- src/storage/expressions/Expression.h | 23 +++ .../expressions/SubstitutionVisitor.cpp | 15 +- src/storage/expressions/TypeCheckVisitor.cpp | 97 ++++++++++ src/storage/expressions/TypeCheckVisitor.h | 50 +++++ src/storage/prism/Program.cpp | 181 ++++++++++++++++++ src/storage/prism/Program.h | 6 + 7 files changed, 378 insertions(+), 18 deletions(-) create mode 100644 src/storage/expressions/TypeCheckVisitor.cpp create mode 100644 src/storage/expressions/TypeCheckVisitor.h diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index 90570f244..51d085fe4 100644 --- a/src/storage/expressions/Expression.cpp +++ b/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 const& identifierToExpressionMap) const { - return SubstitutionVisitor< std::map >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); + return SubstitutionVisitor>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); } Expression Expression::substitute(std::unordered_map const& identifierToExpressionMap) const { - return SubstitutionVisitor< std::unordered_map >(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); + return SubstitutionVisitor>(identifierToExpressionMap).substitute(this->getBaseExpressionPointer().get()); } Expression Expression::substitute(std::map const& identifierToIdentifierMap) const { - return IdentifierSubstitutionVisitor< std::map >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); + return IdentifierSubstitutionVisitor>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); } Expression Expression::substitute(std::unordered_map const& identifierToIdentifierMap) const { - return IdentifierSubstitutionVisitor< std::unordered_map >(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); + return IdentifierSubstitutionVisitor>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get()); } + void Expression::check(std::map const& identifierToTypeMap) const { + return TypeCheckVisitor>(identifierToTypeMap).check(this->getBaseExpressionPointer().get()); + } + + void Expression::check(std::unordered_map const& identifierToTypeMap) const { + return TypeCheckVisitor>(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 Expression::getIdentifiers() const { + std::set result = this->getConstants(); + std::set variables = this->getVariables(); + result.insert(variables.begin(), variables.end()); + return result; + } + BaseExpression const& Expression::getBaseExpression() const { return *this->expressionPtr; } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 15936219c..36c367639 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -110,6 +110,22 @@ namespace storm { */ Expression substitute(std::unordered_map 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 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 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 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 getIdentifiers() const; + /*! * Retrieves the base expression underlying this expression object. Note that prior to calling this, the * expression object must be properly initialized. diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index 54b533d49..402febc2e 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -3,20 +3,7 @@ #include #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 { diff --git a/src/storage/expressions/TypeCheckVisitor.cpp b/src/storage/expressions/TypeCheckVisitor.cpp new file mode 100644 index 000000000..b1cd6a205 --- /dev/null +++ b/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 + TypeCheckVisitor::TypeCheckVisitor(MapType const& identifierToTypeMap) : identifierToTypeMap(identifierToTypeMap) { + // Intentionally left empty. + } + + template + void TypeCheckVisitor::check(BaseExpression const* expression) { + expression->accept(this); + } + + template + void TypeCheckVisitor::visit(IfThenElseExpression const* expression) { + expression->getCondition()->accept(this); + expression->getThenExpression()->accept(this); + expression->getElseExpression()->accept(this); + } + + template + void TypeCheckVisitor::visit(BinaryBooleanFunctionExpression const* expression) { + expression->getFirstOperand()->accept(this); + expression->getSecondOperand()->accept(this); + } + + template + void TypeCheckVisitor::visit(BinaryNumericalFunctionExpression const* expression) { + expression->getFirstOperand()->accept(this); + expression->getSecondOperand()->accept(this); + } + + template + void TypeCheckVisitor::visit(BinaryRelationExpression const* expression) { + expression->getFirstOperand()->accept(this); + expression->getSecondOperand()->accept(this); + } + + template + void TypeCheckVisitor::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 + void TypeCheckVisitor::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 + void TypeCheckVisitor::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 + void TypeCheckVisitor::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 + void TypeCheckVisitor::visit(UnaryBooleanFunctionExpression const* expression) { + expression->getOperand()->accept(this); + } + + template + void TypeCheckVisitor::visit(UnaryNumericalFunctionExpression const* expression) { + expression->getOperand()->accept(this); + } + + template + void TypeCheckVisitor::visit(BooleanLiteralExpression const* expression) { + // Intentionally left empty. + } + + template + void TypeCheckVisitor::visit(IntegerLiteralExpression const* expression) { + // Intentionally left empty. + } + + template + void TypeCheckVisitor::visit(DoubleLiteralExpression const* expression) { + // Intentionally left empty. + } + } +} \ No newline at end of file diff --git a/src/storage/expressions/TypeCheckVisitor.h b/src/storage/expressions/TypeCheckVisitor.h new file mode 100644 index 000000000..e39a536a6 --- /dev/null +++ b/src/storage/expressions/TypeCheckVisitor.h @@ -0,0 +1,50 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_TYPECHECKVISITOR_H_ +#define STORM_STORAGE_EXPRESSIONS_TYPECHECKVISITOR_H_ + +#include + +#include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/ExpressionVisitor.h" + +namespace storm { + namespace expressions { + template + 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_ */ \ No newline at end of file diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 1c4118b8b..5e024cd53 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1,7 +1,11 @@ #include "src/storage/prism/Program.h" + +#include + #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 identifierToTypeMap; + + // Start by checking the constant declarations. + std::set allIdentifiers; + std::set 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 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 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 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 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 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 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 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 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 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 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; diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 40f8047e1..b1b387427 100644 --- a/src/storage/prism/Program.h +++ b/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: