diff --git a/src/ir/Command.h b/src/ir/Command.h index c5bfee6d5..fa881cb52 100644 --- a/src/ir/Command.h +++ b/src/ir/Command.h @@ -11,6 +11,8 @@ #include "expressions/BaseExpression.h" #include "Update.h" +#include + namespace storm { namespace ir { diff --git a/src/ir/Module.h b/src/ir/Module.h index bb3142328..4b673a757 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -12,6 +12,8 @@ #include "IntegerVariable.h" #include "Command.h" +#include + namespace storm { namespace ir { @@ -22,7 +24,7 @@ public: } - Module(std::string moduleName, std::vector booleanVariables, std::vector integerVariables, std::vector commands) + Module(std::string moduleName, std::map booleanVariables, std::map integerVariables, std::vector commands) : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands) { } @@ -34,10 +36,10 @@ public: std::string toString() { std::string result = "module " + moduleName + "\n"; for (auto variable : booleanVariables) { - result += "\t" + variable.toString() + "\n"; + result += "\t" + variable.second.toString() + "\n"; } for (auto variable : integerVariables) { - result += "\t" + variable.toString() + "\n"; + result += "\t" + variable.second.toString() + "\n"; } for (auto command : commands) { result += "\t" + command.toString() + "\n"; @@ -48,11 +50,9 @@ public: private: std::string moduleName; - - std::vector booleanVariables; - std::vector integerVariables; + std::map booleanVariables; + std::map integerVariables; std::vector commands; - }; } diff --git a/src/ir/Update.h b/src/ir/Update.h index 1ea4b0dc1..6f2d3535f 100644 --- a/src/ir/Update.h +++ b/src/ir/Update.h @@ -9,6 +9,7 @@ #define UPDATE_H_ #include "expressions/BaseExpression.h" +#include namespace storm { @@ -20,25 +21,28 @@ public: } - Update(std::shared_ptr likelihoodExpression, std::vector assignments) + Update(std::shared_ptr likelihoodExpression, std::map assignments) : likelihoodExpression(likelihoodExpression), assignments(assignments) { } std::string toString() { std::string result = likelihoodExpression->toString() + " : "; - for (uint_fast64_t i = 0; i < assignments.size(); ++i) { - result += assignments[i].toString(); + uint_fast64_t i = 0; + for (auto assignment : assignments) { + result += assignment.second.toString(); + ++i; if (i < assignments.size() - 1) { result += " & "; } + } return result; } private: std::shared_ptr likelihoodExpression; - std::vector assignments; + std::map assignments; }; } diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h index 9d6c93db2..f2d848fb7 100644 --- a/src/ir/expressions/BaseExpression.h +++ b/src/ir/expressions/BaseExpression.h @@ -8,6 +8,8 @@ #ifndef EXPRESSION_H_ #define EXPRESSION_H_ +#include + namespace storm { namespace ir { diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index f3348cb19..83380003e 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -11,6 +11,11 @@ // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFileFormatException.h" +// Used for Boost spirit. +#include +#include +#include + // Include headers for spirit iterators. Needed for diagnostics and input stream iteration. #include #include @@ -30,6 +35,351 @@ namespace storm { namespace parser { +// The Boost spirit grammar used for parsing the input. +template +struct PrismParser::PrismGrammar : qi::grammar>, std::map>, std::map>, std::map, std::map>>, Skipper> { + + /* + * The constructor of the grammar. It defines all rules of the grammar and the corresponding + * semantic actions that take care of constructing the intermediate representation during + * parsing. + * + * Note: The grammar takes care of some semantic checks already. For example, in places + * where we necessarily require a constant expression, this is enforced by not allowing + * variables as subexpressions. Also, variable names are by definition unique and it is + * ensured that variables and constants are properly declared. + * TODO: It should be ensured that updates of a command only refer to variables of the + * current module. + */ + PrismGrammar() : PrismGrammar::base_type(start) { + // This rule defines all identifiers that have not been previously used. + freeIdentifierName %= qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_'))) - booleanVariableNames_ - integerVariableNames_ - allConstantNames_ - labelNames_ - moduleNames_ - keywords_]]; + freeIdentifierName.name("unused identifier"); + + // This block defines all literal expressions. + booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + booleanLiteralExpression.name("boolean literal"); + integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + integerLiteralExpression.name("integer literal"); + doubleLiteralExpression = qi::double_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + doubleLiteralExpression.name("double literal"); + literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression); + literalExpression.name("literal"); + + // This block defines all expressions that are variables. + integerVariableExpression %= integerVariables_; + integerVariableExpression.name("integer variable"); + booleanVariableExpression %= booleanVariables_; + booleanVariableExpression.name("boolean variable"); + variableExpression %= (integerVariableExpression | booleanVariableExpression); + variableExpression.name("variable"); + + // This block defines all atomic expressions that are constant, i.e. literals and constants. + booleanConstantExpression %= (booleanConstants_ | booleanLiteralExpression); + booleanConstantExpression.name("boolean constant or literal"); + integerConstantExpression %= (integerConstants_ | integerLiteralExpression); + integerConstantExpression.name("integer constant or literal"); + doubleConstantExpression %= (doubleConstants_ | doubleLiteralExpression); + doubleConstantExpression.name("double constant or literal"); + constantExpression %= (booleanConstantExpression | integerConstantExpression | doubleConstantExpression); + constantExpression.name("constant or literal"); + + // This block defines all expressions of integral type. + atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression); + atomicIntegerExpression.name("integer expression"); + integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + integerMultExpression.name("integer expression"); + integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + integerPlusExpression.name("integer expression"); + integerExpression %= integerPlusExpression; + integerExpression.name("integer expression"); + + // This block defines all expressions of integral type that are by syntax constant. That is, they are evaluable given the values for all constants. + constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); + constantAtomicIntegerExpression.name("constant integer expression"); + constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + constantIntegerMultExpression.name("constant integer expression"); + constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantIntegerPlusExpression.name("constant integer expression"); + constantIntegerExpression %= constantIntegerPlusExpression; + constantIntegerExpression.name("constant integer expression"); + + // This block defines all expressions of type double that are by syntax constant. That is, they are evaluable given the values for all constants. + constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); + constantAtomicDoubleExpression.name("constant double expression"); + constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + constantDoubleMultExpression.name("constant double expression"); + constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantDoublePlusExpression.name("constant double expression"); + constantDoubleExpression %= constantDoublePlusExpression; + constantDoubleExpression.name("constant double expression"); + + // This block defines all expressions of type boolean. + relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; + relativeExpression.name("boolean expression"); + atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression); + atomicBooleanExpression.name("boolean expression"); + notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; + notExpression.name("boolean expression"); + andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; + andExpression.name("boolean expression"); + orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))]; + orExpression.name("boolean expression"); + booleanExpression %= orExpression; + booleanExpression.name("boolean expression"); + + // This block defines all expressions of type boolean that are by syntax constant. That is, they are evaluable given the values for all constants. + constantRelativeExpression = (constantIntegerExpression >> relations_ >> constantIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; + constantRelativeExpression.name("constant boolean expression"); + constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); + constantAtomicBooleanExpression.name("constant boolean expression"); + constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; + constantNotExpression.name("constant boolean expression"); + constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; + constantAndExpression.name("constant boolean expression"); + constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))]; + constantOrExpression.name("constant boolean expression"); + constantBooleanExpression %= constantOrExpression; + constantBooleanExpression.name("constant boolean expression"); + + // This block defines the general root of all expressions. Most of the time, however, you may want to start with a more specialized rule. + expression %= (booleanExpression | integerExpression | constantDoubleExpression); + expression.name("expression"); + + // This block defines all entities that are needed for parsing labels. + labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> booleanExpression >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_2)), phoenix::bind(labelNames_.add, qi::_1, qi::_1)]; + labelDefinition.name("label declaration"); + labelDefinitionList %= *labelDefinition(qi::_r1); + labelDefinitionList.name("label declaration list"); + + // This block defines all entities that are needed for parsing a reward model. + stateRewardDefinition = (booleanExpression > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; + stateRewardDefinition.name("state reward definition"); + transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit(":") > constantDoubleExpression > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; + transitionRewardDefinition.name("transition reward definition"); + rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > freeIdentifierName > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_a, qi::_b)))]; + rewardDefinition.name("reward definition"); + rewardDefinitionList = *rewardDefinition(qi::_r1); + rewardDefinitionList.name("reward definition list"); + + // This block defines auxiliary entities that are used to check whether a certain variable exist. + booleanVariableName %= booleanVariableNames_; + booleanVariableName.name("boolean variable"); + integerVariableName %= integerVariableNames_; + integerVariableName.name("integer variable"); + commandName %= commandNames_; + commandName.name("command name"); + + // This block defines all entities that are needed for parsing a single command. + assignmentDefinition = (qi::lit("(") >> integerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))] | (qi::lit("(") > booleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))]; + assignmentDefinition.name("assignment"); + assignmentDefinitionList = assignmentDefinition(qi::_r1) % "&"; + assignmentDefinitionList.name("assignment list"); + updateDefinition = (constantDoubleExpression > qi::lit(":") > assignmentDefinitionList(qi::_a))[qi::_val = phoenix::construct(qi::_1, qi::_a)]; + updateDefinition.name("update"); + updateListDefinition = +updateDefinition % "+"; + updateListDefinition.name("update list"); + commandDefinition = (qi::lit("[") > -((freeIdentifierName[phoenix::bind(commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; + commandDefinition.name("command"); + + // This block defines all entities that are neede for parsing variable definitions. + booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(phoenix::val(qi::_1), qi::_b))), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1)]; + booleanVariableDefinition.name("boolean variable declaration"); + integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2, qi::_3, qi::_b))), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1)]; + integerVariableDefinition.name("integer variable declaration"); + variableDefinition = (booleanVariableDefinition(qi::_r1) | integerVariableDefinition(qi::_r2)); + variableDefinition.name("variable declaration"); + + // This block defines all entities that are needed for parsing a module. + moduleDefinition = (qi::lit("module") > freeIdentifierName > *(variableDefinition(qi::_a, qi::_b)) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_2)]; + moduleDefinition.name("module"); + moduleDefinitionList %= +moduleDefinition; + moduleDefinitionList.name("module list"); + + // This block defines all entities that are needed for parsing constant definitions. + definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") > booleanLiteralExpression > qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedBooleanConstantDefinition.name("defined boolean constant declaration"); + definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") > integerLiteralExpression > qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedIntegerConstantDefinition.name("defined integer constant declaration"); + definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > doubleLiteralExpression > qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedDoubleConstantDefinition.name("defined double constant declaration"); + undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; + undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); + undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(integerConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; + undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); + undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; + undefinedDoubleConstantDefinition.name("undefined double constant declaration"); + definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); + definedConstantDefinition.name("defined constant declaration"); + undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); + undefinedConstantDefinition.name("undefined constant declaration"); + constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); + constantDefinitionList.name("constant declaration list"); + + // This block defines all entities that are needed for parsing a program. + modelTypeDefinition = modelType_; + modelTypeDefinition.name("model type"); + start = (modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > moduleDefinitionList > rewardDefinitionList(qi::_d) > labelDefinitionList(qi::_e))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; + start.name("probabilistic program declaration"); + } + + // The starting point of the grammar. + qi::rule>, std::map>, std::map>, std::map, std::map>>, Skipper> start; + qi::rule modelTypeDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; + qi::rule(), Skipper> moduleDefinitionList; + + // Rules for module definition. + qi::rule, std::map>, Skipper> moduleDefinition; + + // Rules for variable definitions. + qi::rule&, std::map&), Skipper> variableDefinition; + qi::rule&), qi::locals, std::shared_ptr>, Skipper> booleanVariableDefinition; + qi::rule&), qi::locals, std::shared_ptr>, Skipper> integerVariableDefinition; + + // Rules for command definitions. + qi::rule, Skipper> commandDefinition; + qi::rule(), Skipper> updateListDefinition; + qi::rule>, Skipper> updateDefinition; + qi::rule&), Skipper> assignmentDefinitionList; + qi::rule&), Skipper> assignmentDefinition; + + // Rules for variable/command names. + qi::rule integerVariableName; + qi::rule booleanVariableName; + qi::rule commandName; + + // Rules for reward definitions. + qi::rule&), Skipper> rewardDefinitionList; + qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; + qi::rule stateRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; + + // Rules for label definitions. + qi::rule>&), Skipper> labelDefinitionList; + qi::rule>&), Skipper> labelDefinition; + + // Rules for constant definitions. + qi::rule(), Skipper> constantDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; + qi::rule(), Skipper> definedConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; + qi::rule(), Skipper> definedBooleanConstantDefinition; + qi::rule(), Skipper> definedIntegerConstantDefinition; + qi::rule(), Skipper> definedDoubleConstantDefinition; + + qi::rule freeIdentifierName; + qi::rule identifierName; + + // The starting point for arbitrary expressions. + qi::rule(), Skipper> expression; + + // Rules with boolean result type. + qi::rule(), Skipper> booleanExpression; + qi::rule(), Skipper> orExpression; + qi::rule(), Skipper> andExpression; + qi::rule(), Skipper> notExpression; + qi::rule(), Skipper> atomicBooleanExpression; + qi::rule(), Skipper> relativeExpression; + qi::rule(), Skipper> constantBooleanExpression; + qi::rule(), Skipper> constantOrExpression; + qi::rule(), Skipper> constantAndExpression; + qi::rule(), Skipper> constantNotExpression; + qi::rule(), Skipper> constantAtomicBooleanExpression; + qi::rule(), Skipper> constantRelativeExpression; + + // Rules with integer result type. + qi::rule(), Skipper> integerExpression; + qi::rule(), Skipper> integerPlusExpression; + qi::rule(), Skipper> integerMultExpression; + qi::rule(), Skipper> atomicIntegerExpression; + qi::rule(), Skipper> constantIntegerExpression; + qi::rule(), Skipper> constantIntegerPlusExpression; + qi::rule(), Skipper> constantIntegerMultExpression; + qi::rule(), Skipper> constantAtomicIntegerExpression; + + // Rules with double result type. + qi::rule(), Skipper> constantDoubleExpression; + qi::rule(), Skipper> constantDoublePlusExpression; + qi::rule(), Skipper> constantDoubleMultExpression; + qi::rule(), Skipper> constantAtomicDoubleExpression; + + // Rules for variable recognition. + qi::rule(), Skipper> variableExpression; + qi::rule(), Skipper> booleanVariableExpression; + qi::rule(), Skipper> integerVariableExpression; + + // Rules for constant recognition. + qi::rule(), Skipper> constantExpression; + qi::rule(), Skipper> booleanConstantExpression; + qi::rule(), Skipper> integerConstantExpression; + qi::rule(), Skipper> doubleConstantExpression; + + // Rules for literal recognition. + qi::rule(), Skipper> literalExpression; + qi::rule(), Skipper> booleanLiteralExpression; + qi::rule(), Skipper> integerLiteralExpression; + qi::rule(), Skipper> doubleLiteralExpression; + + // A structure defining the keywords that are not allowed to be chosen as identifiers. + struct keywordsStruct : qi::symbols { + keywordsStruct() { + add + ("dtmc", 1) + ("ctmc", 2) + ("mdp", 3) + ("ctmdp", 4) + ("const", 5) + ("int", 6) + ("bool", 7) + ("module", 8) + ("endmodule", 9) + ("rewards", 10) + ("endrewards", 11) + ("true", 12) + ("false", 13) + ; + } + } keywords_; + + // A structure mapping the textual representation of a model type to the model type + // representation of the intermediate representation. + struct modelTypeStruct : qi::symbols { + modelTypeStruct() { + add + ("dtmc", storm::ir::Program::ModelType::DTMC) + ("ctmc", storm::ir::Program::ModelType::CTMC) + ("mdp", storm::ir::Program::ModelType::MDP) + ("ctmdp", storm::ir::Program::ModelType::CTMDP) + ; + } + } modelType_; + + // A structure mapping the textual representation of a binary relation to the representation + // of the intermediate representation. + struct relationalOperatorStruct : qi::symbols { + relationalOperatorStruct() { + add + ("=", storm::ir::expressions::BinaryRelationExpression::EQUAL) + ("<", storm::ir::expressions::BinaryRelationExpression::LESS) + ("<=", storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL) + (">", storm::ir::expressions::BinaryRelationExpression::GREATER) + (">=", storm::ir::expressions::BinaryRelationExpression::GREATER_OR_EQUAL) + ; + } + } relations_; + + // Structures mapping variable and constant names to the corresponding expression nodes of + // the intermediate representation. + struct qi::symbols> integerVariables_, booleanVariables_; + struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; + + // A structure representing the identity function over identifier names. + struct qi::symbols integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_; +}; + /*! * Opens the given file for parsing, invokes the helper function to parse the actual content and * closes the file properly, even if an exception is thrown in the parser. In this case, the @@ -60,56 +410,56 @@ std::shared_ptr PrismParser::parseFile(std::string const& fi * provided, this is caught and displayed properly before the exception is passed on. */ std::shared_ptr PrismParser::parse(std::istream& inputStream, std::string const& filename) const { - // Prepare iterators to input. - base_iterator_type in_begin(inputStream); - forward_iterator_type fwd_begin = boost::spirit::make_default_multi_pass(in_begin); - forward_iterator_type fwd_end; - pos_iterator_type position_begin(fwd_begin, fwd_end, filename); - pos_iterator_type position_end; - - // Prepare resulting intermediate representation of input. - std::shared_ptr result(new storm::ir::Program()); - - // In order to instantiate the grammar, we have to pass the type of the skipping parser. - // As this is more complex, we let Boost figure out the actual type for us. - prismGrammar> *(qi::char_ - qi::eol) >> qi::eol)> grammar; - try { - // Now parse the content using phrase_parse in order to be able to supply a skipping - // parser. - phrase_parse(position_begin, position_end, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, *result); - } catch(const qi::expectation_failure& e) { - // If the parser expected content different than the one provided, display information - // about the location of the error. - const boost::spirit::classic::file_position_base& pos = e.first.get_position(); - - // Construct the error message including a caret display of the position in the - // erroneous line. - std::stringstream msg; - msg << pos.file << ", line " << pos.line << ", column " << pos.column - << ": parse error: expected " << e.what_ << std::endl << "\t" - << e.first.get_currentline() << std::endl << "\t"; - int i = 0; - for (i = 0; i < pos.column; ++i) { - msg << "-"; - } - msg << "^"; - for (; i < 80; ++i) { - msg << "-"; - } - msg << std::endl; + // Prepare iterators to input. + base_iterator_type in_begin(inputStream); + forward_iterator_type fwd_begin = boost::spirit::make_default_multi_pass(in_begin); + forward_iterator_type fwd_end; + pos_iterator_type position_begin(fwd_begin, fwd_end, filename); + pos_iterator_type position_end; + + // Prepare resulting intermediate representation of input. + std::shared_ptr result(new storm::ir::Program()); + + // In order to instantiate the grammar, we have to pass the type of the skipping parser. + // As this is more complex, we let Boost figure out the actual type for us. + PrismGrammar> *(qi::char_ - qi::eol) >> qi::eol)> grammar; + try { + // Now parse the content using phrase_parse in order to be able to supply a skipping + // parser. + qi::phrase_parse(position_begin, position_end, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, *result); + } catch(const qi::expectation_failure& e) { + // If the parser expected content different than the one provided, display information + // about the location of the error. + const boost::spirit::classic::file_position_base& pos = e.first.get_position(); + + // Construct the error message including a caret display of the position in the + // erroneous line. + std::stringstream msg; + msg << pos.file << ", line " << pos.line << ", column " << pos.column + << ": parse error: expected " << e.what_ << std::endl << "\t" + << e.first.get_currentline() << std::endl << "\t"; + int i = 0; + for (i = 0; i < pos.column; ++i) { + msg << "-"; + } + msg << "^"; + for (; i < 80; ++i) { + msg << "-"; + } + msg << std::endl; // On Mac OS, exception messages are not displayed in case an exception is propagated to the // operating system, so we need to display the message ourselves. #if defined(MACOSX) - std::cout << msg.str(); + std::cout << msg.str(); #endif - // Now propagate exception. - throw storm::exceptions::WrongFileFormatException() << msg.str(); - } - - return result; + // Now propagate exception. + throw storm::exceptions::WrongFileFormatException() << msg.str(); } + return result; +} + } // namespace parser } // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index a06c26dea..f4a563e37 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -8,11 +8,6 @@ #ifndef STORM_PARSER_PRISMPARSER_H_ #define STORM_PARSER_PRISMPARSER_H_ -// Used for Boost spirit. -#include -#include -#include - // All classes of the intermediate representation are used. #include "src/ir/IR.h" @@ -23,10 +18,6 @@ namespace storm { namespace parser { -// Use some namespace shortcuts, to reduce code size. -namespace qi = boost::spirit::qi; -namespace phoenix = boost::phoenix; - /*! * This class parses the format of the PRISM model checker into an intermediate representation. */ @@ -55,348 +46,7 @@ private: * the input that complies with the PRISM syntax. */ template - struct prismGrammar : qi::grammar>, std::map>, std::map>, std::map, std::map>>, Skipper> { - - /* - * The constructor of the grammar. It defines all rules of the grammar and the corresponding - * semantic actions that take care of constructing the intermediate representation during - * parsing. - * - * Note: The grammar takes care of some semantic checks already. For example, in places - * where we necessarily require a constant expression, this is enforced by not allowing - * variables as subexpressions. Also, variable names are by definition unique and it is - * ensured that variables and constants are properly declared. - * TODO: It should be ensured that updates of a command only refer to variables of the - * current module. - */ - prismGrammar() : prismGrammar::base_type(start) { - // This rule defines all identifiers that have not been previously used. - freeIdentifierName %= qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_'))) - booleanVariableNames_ - integerVariableNames_ - allConstantNames_ - labelNames_ - moduleNames_ - keywords_]]; - freeIdentifierName.name("unused identifier"); - - // This block defines all literal expressions. - booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; - booleanLiteralExpression.name("boolean literal"); - integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; - integerLiteralExpression.name("integer literal"); - doubleLiteralExpression = qi::double_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; - doubleLiteralExpression.name("double literal"); - literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression); - literalExpression.name("literal"); - - // This block defines all expressions that are variables. - integerVariableExpression %= integerVariables_; - integerVariableExpression.name("integer variable"); - booleanVariableExpression %= booleanVariables_; - booleanVariableExpression.name("boolean variable"); - variableExpression %= (integerVariableExpression | booleanVariableExpression); - variableExpression.name("variable"); - - // This block defines all atomic expressions that are constant, i.e. literals and constants. - booleanConstantExpression %= (booleanConstants_ | booleanLiteralExpression); - booleanConstantExpression.name("boolean constant or literal"); - integerConstantExpression %= (integerConstants_ | integerLiteralExpression); - integerConstantExpression.name("integer constant or literal"); - doubleConstantExpression %= (doubleConstants_ | doubleLiteralExpression); - doubleConstantExpression.name("double constant or literal"); - constantExpression %= (booleanConstantExpression | integerConstantExpression | doubleConstantExpression); - constantExpression.name("constant or literal"); - - // This block defines all expressions of integral type. - atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression); - atomicIntegerExpression.name("integer expression"); - integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; - integerMultExpression.name("integer expression"); - integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; - integerPlusExpression.name("integer expression"); - integerExpression %= integerPlusExpression; - integerExpression.name("integer expression"); - - // This block defines all expressions of integral type that are by syntax constant. That is, they are evaluable given the values for all constants. - constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); - constantAtomicIntegerExpression.name("constant integer expression"); - constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; - constantIntegerMultExpression.name("constant integer expression"); - constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; - constantIntegerPlusExpression.name("constant integer expression"); - constantIntegerExpression %= constantIntegerPlusExpression; - constantIntegerExpression.name("constant integer expression"); - - // This block defines all expressions of type double that are by syntax constant. That is, they are evaluable given the values for all constants. - constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); - constantAtomicDoubleExpression.name("constant double expression"); - constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; - constantDoubleMultExpression.name("constant double expression"); - constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; - constantDoublePlusExpression.name("constant double expression"); - constantDoubleExpression %= constantDoublePlusExpression; - constantDoubleExpression.name("constant double expression"); - - // This block defines all expressions of type boolean. - relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; - relativeExpression.name("boolean expression"); - atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression); - atomicBooleanExpression.name("boolean expression"); - notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; - notExpression.name("boolean expression"); - andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; - andExpression.name("boolean expression"); - orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))]; - orExpression.name("boolean expression"); - booleanExpression %= orExpression; - booleanExpression.name("boolean expression"); - - // This block defines all expressions of type boolean that are by syntax constant. That is, they are evaluable given the values for all constants. - constantRelativeExpression = (constantIntegerExpression >> relations_ >> constantIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; - constantRelativeExpression.name("constant boolean expression"); - constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); - constantAtomicBooleanExpression.name("constant boolean expression"); - constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; - constantNotExpression.name("constant boolean expression"); - constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; - constantAndExpression.name("constant boolean expression"); - constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))]; - constantOrExpression.name("constant boolean expression"); - constantBooleanExpression %= constantOrExpression; - constantBooleanExpression.name("constant boolean expression"); - - // This block defines the general root of all expressions. Most of the time, however, you may want to start with a more specialized rule. - expression %= (booleanExpression | integerExpression | constantDoubleExpression); - expression.name("expression"); - - // This block defines all entities that are needed for parsing labels. - labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> booleanExpression >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_2)), phoenix::bind(labelNames_.add, qi::_1, qi::_1)]; - labelDefinition.name("label declaration"); - labelDefinitionList %= *labelDefinition(qi::_r1); - labelDefinitionList.name("label declaration list"); - - // This block defines all entities that are needed for parsing a reward model. - stateRewardDefinition = (booleanExpression > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; - stateRewardDefinition.name("state reward definition"); - transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit(":") > constantDoubleExpression > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; - transitionRewardDefinition.name("transition reward definition"); - rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > freeIdentifierName > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_a, qi::_b)))]; - rewardDefinition.name("reward definition"); - rewardDefinitionList = *rewardDefinition(qi::_r1); - rewardDefinitionList.name("reward definition list"); - - // This block defines auxiliary entities that are used to check whether a certain variable exist. - booleanVariableName %= booleanVariableNames_; - booleanVariableName.name("boolean variable"); - integerVariableName %= integerVariableNames_; - integerVariableName.name("integer variable"); - commandName %= commandNames_; - commandName.name("command name"); - - // This block defines all entities that are needed for parsing a single command. - assignmentDefinition = (qi::lit("(") >> integerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[qi::_val = phoenix::construct(qi::_1, qi::_2)] | (qi::lit("(") > booleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; - assignmentDefinition.name("assignment"); - assignmentDefinitionList %= assignmentDefinition % "&"; - assignmentDefinitionList.name("assignment list"); - updateDefinition = (constantDoubleExpression > qi::lit(":") > assignmentDefinitionList)[qi::_val = phoenix::construct(qi::_1, qi::_2)]; - updateDefinition.name("update"); - updateListDefinition = +updateDefinition % "+"; - updateListDefinition.name("update list"); - commandDefinition = (qi::lit("[") > -((freeIdentifierName[phoenix::bind(commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; - commandDefinition.name("command"); - - // This block defines all entities that are neede for parsing variable definitions. - booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct(phoenix::val("hallo"), qi::_b), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), std::cout << phoenix::val("here!"), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1)]; - booleanVariableDefinition.name("boolean variable declaration"); - integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2, qi::_3, qi::_b), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1)]; - integerVariableDefinition.name("integer variable declaration"); - variableDefinition = (booleanVariableDefinition | integerVariableDefinition); - variableDefinition.name("variable declaration"); - - // This block defines all entities that are needed for parsing a module. - moduleDefinition = (qi::lit("module") > freeIdentifierName > *(booleanVariableDefinition[phoenix::push_back(qi::_a, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_b, qi::_1)]) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_3)]; - moduleDefinition.name("module"); - moduleDefinitionList %= +moduleDefinition; - moduleDefinitionList.name("module list"); - - // This block defines all entities that are needed for parsing constant definitions. - definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") > booleanLiteralExpression > qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; - definedBooleanConstantDefinition.name("defined boolean constant declaration"); - definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") > integerLiteralExpression > qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; - definedIntegerConstantDefinition.name("defined integer constant declaration"); - definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > doubleLiteralExpression > qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; - definedDoubleConstantDefinition.name("defined double constant declaration"); - undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; - undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(integerConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; - undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); - undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; - undefinedDoubleConstantDefinition.name("undefined double constant declaration"); - definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); - definedConstantDefinition.name("defined constant declaration"); - undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); - undefinedConstantDefinition.name("undefined constant declaration"); - constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); - constantDefinitionList.name("constant declaration list"); - - // This block defines all entities that are needed for parsing a program. - modelTypeDefinition = modelType_; - modelTypeDefinition.name("model type"); - start = (modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > moduleDefinitionList > rewardDefinitionList(qi::_d) > labelDefinitionList(qi::_e))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; - start.name("probabilistic program declaration"); - } - - // The starting point of the grammar. - qi::rule>, std::map>, std::map>, std::map, std::map>>, Skipper> start; - qi::rule modelTypeDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; - qi::rule(), Skipper> moduleDefinitionList; - - // Rules for module definition. - qi::rule, std::vector>, Skipper> moduleDefinition; - - // Rules for variable definitions. - qi::rule variableDefinition; - qi::rule, std::shared_ptr>, Skipper> booleanVariableDefinition; - qi::rule, std::shared_ptr>, Skipper> integerVariableDefinition; - - // Rules for command definitions. - qi::rule, Skipper> commandDefinition; - qi::rule(), Skipper> updateListDefinition; - qi::rule updateDefinition; - qi::rule(), Skipper> assignmentDefinitionList; - qi::rule assignmentDefinition; - - // Rules for variable/command names. - qi::rule integerVariableName; - qi::rule booleanVariableName; - qi::rule commandName; - - // Rules for reward definitions. - qi::rule&), Skipper> rewardDefinitionList; - qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; - qi::rule stateRewardDefinition; - qi::rule, Skipper> transitionRewardDefinition; - - // Rules for label definitions. - qi::rule>&), Skipper> labelDefinitionList; - qi::rule>&), Skipper> labelDefinition; - - // Rules for constant definitions. - qi::rule(), Skipper> constantDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; - qi::rule(), Skipper> definedConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; - qi::rule(), Skipper> definedBooleanConstantDefinition; - qi::rule(), Skipper> definedIntegerConstantDefinition; - qi::rule(), Skipper> definedDoubleConstantDefinition; - - qi::rule freeIdentifierName; - qi::rule identifierName; - - // The starting point for arbitrary expressions. - qi::rule(), Skipper> expression; - - // Rules with boolean result type. - qi::rule(), Skipper> booleanExpression; - qi::rule(), Skipper> orExpression; - qi::rule(), Skipper> andExpression; - qi::rule(), Skipper> notExpression; - qi::rule(), Skipper> atomicBooleanExpression; - qi::rule(), Skipper> relativeExpression; - qi::rule(), Skipper> constantBooleanExpression; - qi::rule(), Skipper> constantOrExpression; - qi::rule(), Skipper> constantAndExpression; - qi::rule(), Skipper> constantNotExpression; - qi::rule(), Skipper> constantAtomicBooleanExpression; - qi::rule(), Skipper> constantRelativeExpression; - - // Rules with integer result type. - qi::rule(), Skipper> integerExpression; - qi::rule(), Skipper> integerPlusExpression; - qi::rule(), Skipper> integerMultExpression; - qi::rule(), Skipper> atomicIntegerExpression; - qi::rule(), Skipper> constantIntegerExpression; - qi::rule(), Skipper> constantIntegerPlusExpression; - qi::rule(), Skipper> constantIntegerMultExpression; - qi::rule(), Skipper> constantAtomicIntegerExpression; - - // Rules with double result type. - qi::rule(), Skipper> constantDoubleExpression; - qi::rule(), Skipper> constantDoublePlusExpression; - qi::rule(), Skipper> constantDoubleMultExpression; - qi::rule(), Skipper> constantAtomicDoubleExpression; - - // Rules for variable recognition. - qi::rule(), Skipper> variableExpression; - qi::rule(), Skipper> booleanVariableExpression; - qi::rule(), Skipper> integerVariableExpression; - - // Rules for constant recognition. - qi::rule(), Skipper> constantExpression; - qi::rule(), Skipper> booleanConstantExpression; - qi::rule(), Skipper> integerConstantExpression; - qi::rule(), Skipper> doubleConstantExpression; - - // Rules for literal recognition. - qi::rule(), Skipper> literalExpression; - qi::rule(), Skipper> booleanLiteralExpression; - qi::rule(), Skipper> integerLiteralExpression; - qi::rule(), Skipper> doubleLiteralExpression; - - // A structure defining the keywords that are not allowed to be chosen as identifiers. - struct keywordsStruct : qi::symbols { - keywordsStruct() { - add - ("dtmc", 1) - ("ctmc", 2) - ("mdp", 3) - ("ctmdp", 4) - ("const", 5) - ("int", 6) - ("bool", 7) - ("module", 8) - ("endmodule", 9) - ("rewards", 10) - ("endrewards", 11) - ("true", 12) - ("false", 13) - ; - } - } keywords_; - - // A structure mapping the textual representation of a model type to the model type - // representation of the intermediate representation. - struct modelTypeStruct : qi::symbols { - modelTypeStruct() { - add - ("dtmc", storm::ir::Program::ModelType::DTMC) - ("ctmc", storm::ir::Program::ModelType::CTMC) - ("mdp", storm::ir::Program::ModelType::MDP) - ("ctmdp", storm::ir::Program::ModelType::CTMDP) - ; - } - } modelType_; - - // A structure mapping the textual representation of a binary relation to the representation - // of the intermediate representation. - struct relationalOperatorStruct : qi::symbols { - relationalOperatorStruct() { - add - ("=", storm::ir::expressions::BinaryRelationExpression::EQUAL) - ("<", storm::ir::expressions::BinaryRelationExpression::LESS) - ("<=", storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL) - (">", storm::ir::expressions::BinaryRelationExpression::GREATER) - (">=", storm::ir::expressions::BinaryRelationExpression::GREATER_OR_EQUAL) - ; - } - } relations_; - - // Structures mapping variable and constant names to the corresponding expression nodes of - // the intermediate representation. - struct qi::symbols> integerVariables_, booleanVariables_; - struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; - - // A structure representing the identity function over identifier names. - struct qi::symbols integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_; - }; + struct PrismGrammar; }; } // namespace parser