From d0d80cf5e1986596ee0b06e663021fd048c0f6f3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 1 May 2014 11:49:49 +0200 Subject: [PATCH 1/8] Started on making the PrismParser more robust. Former-commit-id: 7ce1351d0c7221ef303052d9ab1264f2baaa5f50 --- src/parser/PrismParser.h | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 4a0eec392..6a31ef367 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -27,9 +27,11 @@ typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost: #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expressions.h" #include "src/exceptions/ExceptionMacros.h" +#include "src/exceptions/WrongFormatException.h" namespace storm { namespace parser { + // A class that stores information about the parsed program. class GlobalProgramInformation { public: // Default construct the header information. @@ -117,13 +119,7 @@ namespace storm { template qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { - // LOG4CPLUS_ERROR(logger, "Error: expecting " << what << " in line " << get_line(where) << " at column " << get_column(b, where, 4) << "."); - std::cerr << "Error: expecting " << what << " in line " << get_line(where) << "." << std::endl; - T3 end(where); - while (end != e && *end != '\r' && *end != '\n') { - ++end; - } - std::cerr << "Error: expecting " << what << " in line " << get_line(where) << ": \n" << std::string(get_line_start(b, where), end) << " ... \n" << std::setw(std::distance(b, where)) << '^' << "---- here\n"; + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << what << "."); return qi::fail; } }; From 6f9dd7107d77b2c5e931698bd4064737fe753112 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 1 May 2014 14:14:25 +0200 Subject: [PATCH 2/8] Added universal abstraction function to DD layer. Former-commit-id: 56e5d62b5a780a138ebbfb4276012153d27517e1 --- src/storage/dd/CuddDd.cpp | 17 +++++++++++++++++ src/storage/dd/CuddDd.h | 7 +++++++ 2 files changed, 24 insertions(+) diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index bbce93902..72abb87bf 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -184,6 +184,23 @@ namespace storm { this->cuddAdd = this->cuddAdd.OrAbstract(cubeDd.getCuddAdd()); } + void Dd::universalAbstract(std::set const& metaVariableNames) { + Dd cubeDd(this->getDdManager()->getOne()); + + for (auto const& metaVariableName : metaVariableNames) { + // First check whether the DD contains the meta variable and erase it, if this is the case. + if (!this->containsMetaVariable(metaVariableName)) { + throw storm::exceptions::InvalidArgumentException() << "Cannot abstract from meta variable that is not present in the DD."; + } + this->getContainedMetaVariableNames().erase(metaVariableName); + + DdMetaVariable const& metaVariable = this->getDdManager()->getMetaVariable(metaVariableName); + cubeDd *= metaVariable.getCube(); + } + + this->cuddAdd = this->cuddAdd.UnivAbstract(cubeDd.getCuddAdd()); + } + void Dd::sumAbstract(std::set const& metaVariableNames) { Dd cubeDd(this->getDdManager()->getOne()); diff --git a/src/storage/dd/CuddDd.h b/src/storage/dd/CuddDd.h index 6c7bffd6a..f345c28a2 100644 --- a/src/storage/dd/CuddDd.h +++ b/src/storage/dd/CuddDd.h @@ -233,6 +233,13 @@ namespace storm { */ void existsAbstract(std::set const& metaVariableNames); + /*! + * Universally abstracts from the given meta variables. + * + * @param metaVariableNames The names of all meta variables from which to abstract. + */ + void universalAbstract(std::set const& metaVariableNames); + /*! * Sum-abstracts from the given meta variables. * From 82836f1ad1d5ad06fd0541636b130a1377135819 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 2 May 2014 00:01:14 +0200 Subject: [PATCH 3/8] Added some checks for validity of identifiers in PRISM programs. Added some illegal tests to test suite. Former-commit-id: fc44db75a74221692e6a1ec36ec4f15a8892b17f --- src/parser/PrismParser.cpp | 67 +++++++++++++----- src/parser/PrismParser.h | 2 +- test/functional/parser/PrismParserTest.cpp | 79 ++++++++++++++++++++++ 3 files changed, 129 insertions(+), 19 deletions(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index ed15050cb..b96a0b823 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -147,13 +147,7 @@ namespace storm { globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)])); globalVariableDefinition.name("global variable declaration list"); - - programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1] - > *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)] | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)]) - > *(formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_r1), qi::_1)]) - > *(globalVariableDefinition(qi::_r1)); - programHeader.name("program header"); - + stateRewardDefinition = (expression > qi::lit(":") > plusExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)]; stateRewardDefinition.name("state reward definition"); @@ -199,7 +193,19 @@ namespace storm { moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)]; moduleDefinitionList.name("module list"); - start = (qi::eps > programHeader(qi::_a) > moduleDefinitionList(qi::_a) > *(initialStatesConstruct(qi::_a) | rewardModelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)] | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)] | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)]; + start = (qi::eps + > modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_a) = qi::_1] + > *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] + | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_a), qi::_1)] + | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)] + | globalVariableDefinition(qi::_a) + | (moduleRenaming(qi::_a) | moduleDefinition(qi::_a))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_a), qi::_1)] + | initialStatesConstruct(qi::_a) + | rewardModelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)] + | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)] + | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)] + ) + > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)]; start.name("probabilistic program"); // Enable error reporting. @@ -258,7 +264,7 @@ namespace storm { } bool PrismParser::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { - LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::InvalidArgumentException, "Program must not define two initial constructs."); + LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::WrongFormatException, "Program must not define two initial constructs."); if (globalProgramInformation.hasInitialStatesExpression) { return false; } @@ -483,37 +489,56 @@ namespace storm { } storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename()); } storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename()); } storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename()); } storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const { - this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename()); } storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const { - if (this->secondRun) { + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << formulaName << "'."); this->identifiers_.add(formulaName, expression); } return storm::prism::Formula(formulaName, expression, this->getFilename()); @@ -550,12 +575,18 @@ namespace storm { } storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const { - this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'."); + this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName)); + } return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename()); } storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const { - this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName)); + if (!this->secondRun) { + LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'."); + this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName)); + } return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename()); } diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 6a31ef367..b5013eee8 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -189,7 +189,7 @@ namespace storm { qi::rule modelTypeDefinition; // Rules for parsing the program header. - qi::rule programHeader; + qi::rule undefinedConstantDefinition; qi::rule undefinedBooleanConstantDefinition; qi::rule undefinedIntegerConstantDefinition; diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index 81731114b..dca09244a 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -54,6 +54,21 @@ TEST(PrismParser, SimpleFullTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true)); EXPECT_EQ(1, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType()); + + testInput = + R"(mdp + + module main + x : [1..5] init 1; + [] x=1 -> 1:(x'=2); + [] x=2 -> 1:(x'=3); + [] x=3 -> 1:(x'=1); + [] x=3 -> 1:(x'=4); + [] x=4 -> 1:(x'=5); + endmodule)"; + EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true)); + EXPECT_EQ(1, result.getNumberOfModules()); + EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType()); } TEST(PrismParser, ComplexFullTest) { @@ -167,4 +182,68 @@ TEST(PrismParser, ComplexParsingTest) { EXPECT_EQ(2, result.getNumberOfRewardModels()); EXPECT_EQ(1, result.getNumberOfLabels()); EXPECT_TRUE(result.definesInitialStatesExpression()); +} + +TEST(PrismParser, IllegalInputTest) { + std::string testInput = + R"(ctmc + + const int a; + const bool a = true; + + module mod1 + c : [0 .. 8] init 1; + [] c < 3 -> 2: (c' = c+1); + endmodule + )"; + + storm::prism::Program result; + EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException); + + testInput = + R"(dtmc + + const int a; + + module mod1 + a : [0 .. 8] init 1; + [] a < 3 -> 1: (a' = a+1); + endmodule)"; + + EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException); + + testInput = + R"(dtmc + + const int a = 2; + formula a = 41; + + module mod1 + c : [0 .. 8] init 1; + [] c < 3 -> 1: (c' = c+1); + endmodule)"; + + EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException); + + testInput = + R"(dtmc + + const int a = 2; + + init + c > 3 + endinit + + module mod1 + c : [0 .. 8] init 1; + [] c < 3 -> 1: (c' = c+1); + endmodule + + init + c > 3 + endinit + + )"; + + EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile", false), storm::exceptions::WrongFormatException); } \ No newline at end of file From 873d80cd2d0bc279c7a99e512756924ae80f6b75 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 3 May 2014 13:20:25 +0200 Subject: [PATCH 4/8] If a module is renamed from some other module, this is now kept track of in the respective PRISM classes. Former-commit-id: c07e25ac55e86520522047ad4b7bc394fd36b556 --- src/parser/PrismParser.cpp | 169 ++++++++++++++++++++++++++--------- src/parser/PrismParser.h | 1 - src/storage/prism/Module.cpp | 21 ++++- src/storage/prism/Module.h | 47 +++++++++- 4 files changed, 191 insertions(+), 47 deletions(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index b96a0b823..ffda5e219 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -1,5 +1,6 @@ #include "src/parser/PrismParser.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/WrongFormatException.h" namespace storm { @@ -7,7 +8,7 @@ namespace storm { storm::prism::Program PrismParser::parse(std::string const& filename, bool typeCheck) { // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); - LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file " << filename << "."); + LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); storm::prism::Program result; @@ -264,7 +265,7 @@ namespace storm { } bool PrismParser::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { - LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::WrongFormatException, "Program must not define two initial constructs."); + LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs."); if (globalProgramInformation.hasInitialStatesExpression) { return false; } @@ -277,7 +278,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1.ite(e2, e3); + try { + return e1.ite(e2, e3); + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -285,7 +290,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1.implies(e2); + try { + return e1.implies(e2); + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -293,7 +302,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 || e2; + try { + return e1 || e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -301,7 +314,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 && e2; + try{ + return e1 && e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -309,7 +326,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 > e2; + try { + return e1 > e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -317,7 +338,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 >= e2; + try { + return e1 >= e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -325,7 +350,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 < e2; + try { + return e1 < e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -333,7 +362,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 <= e2; + try { + return e1 <= e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -341,10 +374,14 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { - return e1.iff(e2); - } else { - return e1 == e2; + try { + if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { + return e1.iff(e2); + } else { + return e1 == e2; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); } } } @@ -353,10 +390,14 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { - return e1 ^ e2; - } else { - return e1 != e2; + try { + if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { + return e1 ^ e2; + } else { + return e1 != e2; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); } } } @@ -365,7 +406,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 + e2; + try { + return e1 + e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -373,7 +418,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 - e2; + try { + return e1 - e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -381,7 +430,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 * e2; + try { + return e1 * e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -389,7 +442,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1 / e2; + try { + return e1 / e2; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -397,7 +454,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return !e1; + try { + return !e1; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -405,7 +466,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return -e1; + try { + return -e1; + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -450,7 +515,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return storm::expressions::Expression::minimum(e1, e2); + try { + return storm::expressions::Expression::minimum(e1, e2); + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -458,7 +527,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return storm::expressions::Expression::maximum(e1, e2); + try { + return storm::expressions::Expression::maximum(e1, e2); + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -466,7 +539,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1.floor(); + try { + return e1.floor(); + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -474,7 +551,11 @@ namespace storm { if (!this->secondRun) { return storm::expressions::Expression::createFalse(); } else { - return e1.ceil(); + try { + return e1.ceil(); + } catch (storm::exceptions::InvalidTypeException const& e) { + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << "."); + } } } @@ -483,14 +564,14 @@ namespace storm { return storm::expressions::Expression::createFalse(); } else { storm::expressions::Expression const* expression = this->identifiers_.find(identifier); - LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Undeclared identifier '" << identifier << "'."); + LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'."); return *expression; } } storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const { if (!this->secondRun) { - LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename()); @@ -498,7 +579,7 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const { if (!this->secondRun) { - LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename()); @@ -506,7 +587,7 @@ namespace storm { storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const { if (!this->secondRun) { - LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename()); @@ -514,7 +595,7 @@ namespace storm { storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { - LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename()); @@ -522,7 +603,7 @@ namespace storm { storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { - LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename()); @@ -530,7 +611,7 @@ namespace storm { storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const { if (!this->secondRun) { - LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'."); + LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'."); this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); } return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename()); @@ -538,7 +619,7 @@ namespace storm { storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const { if (!this->secondRun) { - LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << formulaName << "'."); + LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'."); this->identifiers_.add(formulaName, expression); } return storm::prism::Formula(formulaName, expression, this->getFilename()); @@ -576,7 +657,7 @@ namespace storm { storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const { if (!this->secondRun) { - LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'."); + LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'."); this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName)); } return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename()); @@ -584,7 +665,7 @@ namespace storm { storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const { if (!this->secondRun) { - LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'."); + LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'."); this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName)); } return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename()); @@ -598,19 +679,19 @@ namespace storm { storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const { // Check whether the module to rename actually exists. auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName); - LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "No module named '" << oldModuleName << "' to rename."); + LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": No module named '" << oldModuleName << "' to rename."); storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second]; if (!this->secondRun) { // Register all (renamed) variables for later use. for (auto const& variable : moduleToRename.getBooleanVariables()) { auto const& renamingPair = renaming.find(variable.getName()); - LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed."); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed."); this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createBooleanVariable(renamingPair->second)); } for (auto const& variable : moduleToRename.getIntegerVariables()) { auto const& renamingPair = renaming.find(variable.getName()); - LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed."); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed."); this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createIntegerVariable(renamingPair->second)); } @@ -634,7 +715,7 @@ namespace storm { std::vector booleanVariables; for (auto const& variable : moduleToRename.getBooleanVariables()) { auto const& renamingPair = renaming.find(variable.getName()); - LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed."); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed."); booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); } @@ -643,7 +724,7 @@ namespace storm { std::vector integerVariables; for (auto const& variable : moduleToRename.getIntegerVariables()) { auto const& renamingPair = renaming.find(variable.getName()); - LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed."); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed."); integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); } @@ -676,7 +757,7 @@ namespace storm { ++globalProgramInformation.currentCommandIndex; } - return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, this->getFilename()); + return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, oldModuleName, renaming); } } diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index b5013eee8..3312768c3 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -189,7 +189,6 @@ namespace storm { qi::rule modelTypeDefinition; // Rules for parsing the program header. - qi::rule undefinedConstantDefinition; qi::rule undefinedBooleanConstantDefinition; qi::rule undefinedIntegerConstantDefinition; diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index f17e1bc12..d7b3fb572 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -2,10 +2,15 @@ #include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/InvalidAccessException.h" namespace storm { namespace prism { - Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap() { + Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& filename, uint_fast64_t lineNumber) : Module(moduleName, booleanVariables, integerVariables, commands, "", std::map(), filename, lineNumber) { + // Intentionally left empty. + } + + Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& renamedFromModule, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) { // Initialize the internal mappings for fast information retrieval. this->createMappings(); } @@ -71,6 +76,20 @@ namespace storm { return actionEntry != this->actions.end(); } + bool Module::isRenamedFromModule() const { + return this->renamedFromModule != ""; + } + + std::string const& Module::getBaseModule() const { + LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve base module of module that was not created by renaming."); + return this->renamedFromModule; + } + + std::map const& Module::getRenaming() const { + LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve renaming of module that was not created by renaming."); + return this->renaming; + } + std::set const& Module::getCommandIndicesByAction(std::string const& action) const { auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action); if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) { diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index f4fd21f29..1031cbf27 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_PRISM_MODULE_H_ #include +#include #include #include #include @@ -28,7 +29,22 @@ namespace storm { * @param lineNumber The line number in which the module is defined. */ Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0); - + + /*! + * Creates a module with the given name, variables and commands that is marked as being renamed from the + * given module with the given renaming. + * + * @param moduleName The name of the module. + * @param booleanVariables The boolean variables defined by the module. + * @param integerVariables The integer variables defined by the module. + * @param commands The commands of the module. + * @param renamedFromModule The name of the module from which this module was renamed. + * @param renaming The renaming of identifiers used to create this module. + * @param filename The filename in which the module is defined. + * @param lineNumber The line number in which the module is defined. + */ + Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& renamedFromModule, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); + // Create default implementations of constructors/assignment. Module() = default; Module(Module const& other) = default; @@ -133,6 +149,29 @@ namespace storm { */ bool hasAction(std::string const& action) const; + /*! + * Retrieves whether this module was created from another module via renaming. + * + * @return True iff the module was created via renaming. + */ + bool isRenamedFromModule() const; + + /*! + * If the module was created via renaming, this method retrieves the name of the module that was used as the + * in the base in the renaming process. + * + * @return The name of the module from which this module was created via renaming. + */ + std::string const& getBaseModule() const; + + /*! + * If the module was created via renaming, this method returns the applied renaming of identifiers used for + * the renaming process. + * + * @return A mapping of identifiers to new identifiers that was used in the renaming process. + */ + std::map const& getRenaming() const; + /*! * Retrieves the indices of all commands within this module that are labelled by the given action. * @@ -188,6 +227,12 @@ namespace storm { // A map of actions to the set of commands labeled with this action. std::map> actionsToCommandIndexMap; + + // This string indicates whether and from what module this module was created via renaming. + std::string renamedFromModule; + + // If the module was created by renaming, this mapping contains the provided renaming of identifiers. + std::map renaming; }; } // namespace prism From 83f9832e2dce56d65112a2ae1877db7ebdc264b5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 4 May 2014 21:51:05 +0200 Subject: [PATCH 5/8] 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: From c76e0e8d4d63be0f7371807bd5e15499fd809c39 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 5 May 2014 14:41:17 +0200 Subject: [PATCH 6/8] Added class for initial construct of PRISM programs (to capture position information). Added more validity checks for programs and tests for them (not all though). Former-commit-id: cf4e985684a225d4f99e9ad58d7737cd67409e3e --- src/parser/PrismParser.cpp | 38 +-- src/parser/PrismParser.h | 16 +- src/storage/expressions/BaseExpression.cpp | 7 +- .../expressions/SubstitutionVisitor.cpp | 4 +- src/storage/expressions/TypeCheckVisitor.cpp | 12 +- src/storage/prism/Command.cpp | 2 +- src/storage/prism/Constant.cpp | 4 +- src/storage/prism/Formula.cpp | 4 +- src/storage/prism/InitialConstruct.cpp | 24 ++ src/storage/prism/InitialConstruct.h | 56 ++++ src/storage/prism/Label.cpp | 4 +- src/storage/prism/LocatedInformation.cpp | 4 +- src/storage/prism/Module.cpp | 3 +- src/storage/prism/Program.cpp | 265 ++++++++++++++---- src/storage/prism/Program.h | 35 +-- src/storage/prism/Update.cpp | 2 +- test/functional/parser/PrismParserTest.cpp | 184 ++++++------ 17 files changed, 442 insertions(+), 222 deletions(-) create mode 100644 src/storage/prism/InitialConstruct.cpp create mode 100644 src/storage/prism/InitialConstruct.h diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index ffda5e219..727579dff 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -5,7 +5,7 @@ namespace storm { namespace parser { - storm::prism::Program PrismParser::parse(std::string const& filename, bool typeCheck) { + storm::prism::Program PrismParser::parse(std::string const& filename) { // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); @@ -15,7 +15,7 @@ namespace storm { // Now try to parse the contents of the file. try { std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); - result = parseFromString(fileContent, filename, typeCheck); + result = parseFromString(fileContent, filename); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. inputFileStream.close(); @@ -27,7 +27,7 @@ namespace storm { return result; } - storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool typeCheck) { + storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename) { PositionIteratorType first(input.begin()); PositionIteratorType iter = first; PositionIteratorType last(input.end()); @@ -38,17 +38,17 @@ namespace storm { // Create grammar. storm::parser::PrismParser grammar(filename, first); try { - // Now parse the content using phrase_parse in order to be able to supply a skipping parser. + // Start first run. bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass."); - if (typeCheck) { - first = PositionIteratorType(input.begin()); - iter = first; - last = PositionIteratorType(input.end()); - grammar.moveToSecondRun(); - succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); - LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in second pass."); - } + + // Start second run. + first = PositionIteratorType(input.begin()); + iter = first; + last = PositionIteratorType(input.end()); + grammar.moveToSecondRun(); + succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); + LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in second pass."); } catch (qi::expectation_failure const& e) { // If the parser expected content different than the one provided, display information about the location of the error. std::size_t lineNumber = boost::spirit::get_line(e.first); @@ -162,7 +162,7 @@ namespace storm { >> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; rewardModelDefinition.name("reward model definition"); - initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesExpression, phoenix::ref(*this), qi::_1, qi::_r1)]; + initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; initialStatesConstruct.name("initial construct"); labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -264,13 +264,13 @@ namespace storm { return true; } - bool PrismParser::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { - LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs."); - if (globalProgramInformation.hasInitialStatesExpression) { + bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { + LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs."); + if (globalProgramInformation.hasInitialConstruct) { return false; } - globalProgramInformation.hasInitialStatesExpression = true; - globalProgramInformation.initialStatesExpression = initialStatesExpression; + globalProgramInformation.hasInitialConstruct = true; + globalProgramInformation.initialConstruct = storm::prism::InitialConstruct(initialStatesExpression, this->getFilename(), get_line(qi::_3)); return true; } @@ -762,7 +762,7 @@ namespace storm { } storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const { - return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, globalProgramInformation.hasInitialStatesExpression, globalProgramInformation.initialStatesExpression, globalProgramInformation.labels, this->getFilename()); + return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun); } } // namespace parser } // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 3312768c3..e1a9136ba 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -35,7 +35,9 @@ namespace storm { class GlobalProgramInformation { public: // Default construct the header information. - GlobalProgramInformation() : hasInitialStatesExpression(false), currentCommandIndex(0), currentUpdateIndex(0) {} + GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(),hasInitialConstruct(false), initialConstruct(storm::expressions::Expression::createFalse()), currentCommandIndex(0), currentUpdateIndex(0) { + // Intentionally left empty. + } // Members for all essential information that needs to be collected. storm::prism::Program::ModelType modelType; @@ -47,8 +49,8 @@ namespace storm { std::vector modules; std::vector rewardModels; std::vector labels; - storm::expressions::Expression initialStatesExpression; - bool hasInitialStatesExpression; + bool hasInitialConstruct; + storm::prism::InitialConstruct initialConstruct; // Counters to provide unique indexing for commands and updates. uint_fast64_t currentCommandIndex; @@ -61,20 +63,18 @@ namespace storm { * Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax. * * @param filename the name of the file to parse. - * @param typeCheck Sets whether the expressions are generated and therefore typechecked. * @return The resulting PRISM program. */ - static storm::prism::Program parse(std::string const& filename, bool typeCheck = true); + static storm::prism::Program parse(std::string const& filename); /*! * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax. * * @param input The input string to parse. * @param filename The name of the file from which the input was read. - * @param typeCheck Sets whether the expressions are generated and therefore typechecked. * @return The resulting PRISM program. */ - static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool typeCheck = true); + static storm::prism::Program parseFromString(std::string const& input, std::string const& filename); private: struct modelTypeStruct : qi::symbols { @@ -263,7 +263,7 @@ namespace storm { // Helper methods used in the grammar. bool isValidIdentifier(std::string const& identifier); - bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); + bool addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const; storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index b9734a9ad..bb4ea0921 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/src/storage/expressions/BaseExpression.cpp @@ -53,7 +53,12 @@ namespace storm { } std::ostream& operator<<(std::ostream& stream, ExpressionReturnType const& enumValue) { - stream << static_cast::type>(enumValue); + switch (enumValue) { + case ExpressionReturnType::Undefined: stream << "undefined"; break; + case ExpressionReturnType::Bool: stream << "bool"; break; + case ExpressionReturnType::Int: stream << "int"; break; + case ExpressionReturnType::Double: stream << "double"; break; + } return stream; } diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index 402febc2e..7990ab4f9 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -182,7 +182,7 @@ namespace storm { } // Explicitly instantiate the class with map and unordered_map. - template class SubstitutionVisitor< std::map >; - template class SubstitutionVisitor< std::unordered_map >; + template class SubstitutionVisitor>; + template class SubstitutionVisitor>; } } diff --git a/src/storage/expressions/TypeCheckVisitor.cpp b/src/storage/expressions/TypeCheckVisitor.cpp index b1cd6a205..d5cef0381 100644 --- a/src/storage/expressions/TypeCheckVisitor.cpp +++ b/src/storage/expressions/TypeCheckVisitor.cpp @@ -45,28 +45,28 @@ namespace storm { 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() << "."); + 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() << "."); + LOG_THROW(identifierTypePair->second == ExpressionReturnType::Double, 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() << "."); + LOG_THROW(identifierTypePair->second == ExpressionReturnType::Int, 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() << "."); + LOG_THROW(identifierTypePair->second == expression->getReturnType(), storm::exceptions::InvalidTypeException, "Type mismatch for variable '" << expression->getVariableName() << "': expected '" << identifierTypePair->first << "', but found '" << expression->getReturnType() << "'."); } template @@ -93,5 +93,9 @@ namespace storm { void TypeCheckVisitor::visit(DoubleLiteralExpression const* expression) { // Intentionally left empty. } + + // Explicitly instantiate the class with map and unordered_map. + template class TypeCheckVisitor>; + template class TypeCheckVisitor>; } } \ No newline at end of file diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index 4b36942df..4c1619732 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -51,5 +51,5 @@ namespace storm { stream << ";"; return stream; } - } // namespace ir + } // namespace prism } // namespace storm diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp index 641336c76..c02deea99 100644 --- a/src/storage/prism/Constant.cpp +++ b/src/storage/prism/Constant.cpp @@ -48,5 +48,5 @@ namespace storm { stream << ";"; return stream; } - } -} \ No newline at end of file + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/Formula.cpp b/src/storage/prism/Formula.cpp index fbda0c69d..a120078b8 100644 --- a/src/storage/prism/Formula.cpp +++ b/src/storage/prism/Formula.cpp @@ -26,5 +26,5 @@ namespace storm { stream << "formula " << formula.getName() << " = " << formula.getExpression() << ";"; return stream; } - } -} \ No newline at end of file + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/InitialConstruct.cpp b/src/storage/prism/InitialConstruct.cpp new file mode 100644 index 000000000..61c662843 --- /dev/null +++ b/src/storage/prism/InitialConstruct.cpp @@ -0,0 +1,24 @@ +#include "src/storage/prism/InitialConstruct.h" + +namespace storm { + namespace prism { + InitialConstruct::InitialConstruct(storm::expressions::Expression initialStatesExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), initialStatesExpression(initialStatesExpression) { + // Intentionally left empty. + } + + storm::expressions::Expression InitialConstruct::getInitialStatesExpression() const { + return this->initialStatesExpression; + } + + InitialConstruct InitialConstruct::substitute(std::map const& substitution) const { + return InitialConstruct(this->getInitialStatesExpression().substitute(substitution)); + } + + std::ostream& operator<<(std::ostream& stream, InitialConstruct const& initialConstruct) { + stream << "initial " << std::endl; + stream << "\t" << initialConstruct.getInitialStatesExpression() << std::endl; + stream << "endinitial" << std::endl; + return stream; + } + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/InitialConstruct.h b/src/storage/prism/InitialConstruct.h new file mode 100644 index 000000000..6f7f6adb9 --- /dev/null +++ b/src/storage/prism/InitialConstruct.h @@ -0,0 +1,56 @@ +#ifndef STORM_STORAGE_PRISM_INITIALCONSTRUCT_H_ +#define STORM_STORAGE_PRISM_INITIALCONSTRUCT_H_ + +#include + +#include "src/storage/prism/LocatedInformation.h" +#include "src/storage/expressions/Expression.h" +#include "src/utility/OsDetection.h" + +namespace storm { + namespace prism { + class InitialConstruct : public LocatedInformation { + public: + /*! + * Creates an initial construct with the given expression. + * + * @param initialStatesExpression An expression characterizing the initial states. + * @param filename The filename in which the command is defined. + * @param lineNumber The line number in which the command is defined. + */ + InitialConstruct(storm::expressions::Expression initialStatesExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + // Create default implementations of constructors/assignment. + InitialConstruct() = default; + InitialConstruct(InitialConstruct const& other) = default; + InitialConstruct& operator=(InitialConstruct const& other)= default; +#ifndef WINDOWS + InitialConstruct(InitialConstruct&& other) = default; + InitialConstruct& operator=(InitialConstruct&& other) = default; +#endif + + /*! + * Retrieves the expression characterizing the initial states. + * + * @return The expression characterizing the initial states. + */ + storm::expressions::Expression getInitialStatesExpression() const; + + /*! + * Substitutes all identifiers in the constant according to the given map. + * + * @param substitution The substitution to perform. + * @return The resulting initial construct. + */ + InitialConstruct substitute(std::map const& substitution) const; + + friend std::ostream& operator<<(std::ostream& stream, InitialConstruct const& initialConstruct); + + private: + // An expression characterizing the initial states. + storm::expressions::Expression initialStatesExpression; + }; + } +} + +#endif /* STORM_STORAGE_PRISM_INITIALCONSTRUCT_H_ */ \ No newline at end of file diff --git a/src/storage/prism/Label.cpp b/src/storage/prism/Label.cpp index cb8a13f25..d11091cf0 100644 --- a/src/storage/prism/Label.cpp +++ b/src/storage/prism/Label.cpp @@ -22,5 +22,5 @@ namespace storm { stream << "label \"" << label.getName() << "\" = " << label.getStatePredicateExpression() << ";"; return stream; } - } -} \ No newline at end of file + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/LocatedInformation.cpp b/src/storage/prism/LocatedInformation.cpp index a5a493319..a3862d57a 100644 --- a/src/storage/prism/LocatedInformation.cpp +++ b/src/storage/prism/LocatedInformation.cpp @@ -21,5 +21,5 @@ namespace storm { void LocatedInformation::setLineNumber(uint_fast64_t lineNumber) { this->lineNumber = lineNumber; } - } -} \ No newline at end of file + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index d7b3fb572..6f4becb0a 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -182,7 +182,6 @@ namespace storm { stream << "endmodule" << std::endl; return stream; } - - } // namespace ir + } // namespace prism } // namespace storm diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 5e024cd53..c29001b16 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -6,13 +6,41 @@ #include "exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/InvalidTypeException.h" namespace storm { namespace prism { - Program::Program(ModelType modelType, std::vector const& constants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::vector const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector