sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Compiling version of PrismParser.

tempestpy_adaptions
gereon 12 years ago
parent
840a9b6e07
commit
bb37bc49f2
13 changed files with 745 additions and 372 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 429
      src/parser/PrismParser.cpp
  2. 111
      src/parser/PrismParser.h
  3. 55
      src/parser/PrismParser/BooleanExpressionGrammar.cpp
  4. 66
      src/parser/PrismParser/BooleanExpressionGrammar.h
  5. 32
      src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp
  6. 49
      src/parser/PrismParser/ConstBooleanExpressionGrammar.h
  7. 30
      src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp
  8. 38
      src/parser/PrismParser/ConstIntegerExpressionGrammar.h
  9. 35
      src/parser/PrismParser/Includes.h
  10. 46
      src/parser/PrismParser/IntegerExpressionGrammar.cpp
  11. 61
      src/parser/PrismParser/IntegerExpressionGrammar.h
  12. 69
      src/parser/PrismParser/UtilityGrammars.h
  13. 96
      src/parser/PrismParser/VariableState.h

429
src/parser/PrismParser.cpp
View File

@ -7,6 +7,11 @@
#include "PrismParser.h"
#include "src/utility/OsDetection.h"
#include "src/parser/PrismParser/VariableState.h"
#include "src/parser/PrismParser/IntegerExpressionGrammar.h"
#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h"
#include "src/parser/PrismParser/BooleanExpressionGrammar.h"
#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h"
// If the parser fails due to ill-formed data, this exception is thrown.
#include "src/exceptions/WrongFileFormatException.h"
@ -35,41 +40,25 @@ namespace storm {
namespace parser {
using namespace storm::ir;
using namespace storm::ir::expressions;
// The Boost spirit grammar used for parsing the input.
template<typename Iterator, typename Skipper>
struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<std::map<std::string, std::shared_ptr<BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>, std::map<std::string, RewardModel>, std::map<std::string, std::shared_ptr<BaseExpression>>>, 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), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) {
PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type(start) {
this->state = std::shared_ptr<storm::parser::prism::VariableState>(new storm::parser::prism::VariableState());
storm::parser::prism::IntegerExpressionGrammar intExpr(this->state);
storm::parser::prism::ConstIntegerExpressionGrammar constIntExpr(this->state);
storm::parser::prism::BooleanExpressionGrammar boolExpr(this->state);
storm::parser::prism::ConstBooleanExpressionGrammar constBoolExpr(this->state);
// This rule defines all identifiers that have not been previously used.
identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&PrismGrammar<Iterator,Skipper>::isIdentifier, this, qi::_1) ];
identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isIdentifier, this->state.get(), qi::_1) ];
identifierName.name("identifier");
freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&PrismGrammar<Iterator,Skipper>::isFreeIdentifier, this, qi::_1) ];
freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isFreeIdentifier, this->state.get(), qi::_1) ];
freeIdentifierName.name("unused identifier");
// This block defines all literal expressions.
booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BooleanLiteral>(qi::_1))];
booleanLiteralExpression.name("boolean literal");
integerLiteralExpression = qi::int_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<IntegerLiteral>(qi::_1))];
integerLiteralExpression.name("integer literal");
doubleLiteralExpression = qi::double_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<DoubleLiteral>(qi::_1))];
doubleLiteralExpression.name("double literal");
literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression);
literalExpression.name("literal");
// This block defines all expressions that are variables.
@ -80,38 +69,11 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
booleanVariableExpression = identifierName[qi::_val = boolvarexpr];
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 %= (this->state->booleanConstants_ | booleanLiteralExpression);
booleanConstantExpression.name("boolean constant or literal");
integerConstantExpression %= (integerConstants_ | integerLiteralExpression);
integerConstantExpression.name("integer constant or literal");
doubleConstantExpression %= (doubleConstants_ | doubleLiteralExpression);
doubleConstantExpression %= (this->state->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<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::TIMES))];
integerMultExpression.name("integer expression");
integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::MINUS))]];
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<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::TIMES))];
constantIntegerMultExpression.name("constant integer expression");
constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::MINUS))]];
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);
@ -123,48 +85,16 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
constantDoubleExpression %= constantDoublePlusExpression;
constantDoubleExpression.name("constant double expression");
// This block defines all expressions of type boolean.
relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryRelationExpression>(qi::_1, qi::_3, qi::_2))];
relativeExpression.name("relative 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<std::shared_ptr<UnaryBooleanFunctionExpression>>(phoenix::new_<UnaryBooleanFunctionExpression>(qi::_1, UnaryBooleanFunctionExpression::NOT))];
notExpression.name("boolean expression");
andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryBooleanFunctionExpression>(qi::_val, qi::_1, BinaryBooleanFunctionExpression::AND))];
andExpression.name("boolean expression");
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryBooleanFunctionExpression>(qi::_val, qi::_1, 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<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryRelationExpression>(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<std::shared_ptr<UnaryBooleanFunctionExpression>>(phoenix::new_<UnaryBooleanFunctionExpression>(qi::_1, UnaryBooleanFunctionExpression::NOT))];
constantNotExpression.name("constant boolean expression");
constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryBooleanFunctionExpression>(qi::_val, qi::_1, BinaryBooleanFunctionExpression::AND))];
constantAndExpression.name("constant boolean expression");
constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryBooleanFunctionExpression>(qi::_val, qi::_1, 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<std::pair<std::string, std::shared_ptr<BaseExpression>>>(qi::_1, qi::_2)), phoenix::bind(labelNames_.add, qi::_1, qi::_1)];
labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> boolExpr >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<BaseExpression>>>(qi::_1, qi::_2)), phoenix::bind(this->state->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<StateReward>(qi::_1, qi::_2)];
stateRewardDefinition = (boolExpr > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct<StateReward>(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<TransitionReward>(qi::_a, qi::_2, qi::_3)];
transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > boolExpr > qi::lit(":") > constantDoubleExpression > qi::lit(";"))[qi::_val = phoenix::construct<TransitionReward>(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<std::pair<std::string, RewardModel>>(qi::_1, phoenix::construct<RewardModel>(qi::_1, qi::_a, qi::_b)))];
rewardDefinition.name("reward definition");
@ -172,50 +102,45 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
rewardDefinitionList.name("reward definition list");
// This block defines auxiliary entities that are used to check whether a certain variable exist.
booleanVariableName %= booleanVariableNames_;
booleanVariableName %= this->state->booleanVariableNames_;
booleanVariableName.name("boolean variable");
integerVariableName %= integerVariableNames_;
integerVariableName %= this->state->integerVariableNames_;
integerVariableName.name("integer variable");
commandName %= commandNames_;
commandName %= this->state->commandNames_;
commandName.name("command name");
unassignedLocalBooleanVariableName %= localBooleanVariables_ - assignedLocalBooleanVariables_;
unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_;
unassignedLocalBooleanVariableName.name("unassigned local boolean variable");
unassignedLocalIntegerVariableName %= localIntegerVariables_ - assignedLocalIntegerVariables_;
unassignedLocalIntegerVariableName %= this->state->localIntegerVariables_ - this->state->assignedLocalIntegerVariables_;
unassignedLocalIntegerVariableName.name("unassigned local integer variable");
// This block defines all entities that are needed for parsing a single command.
assignmentDefinition = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[phoenix::bind(assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, Assignment>>(qi::_1, phoenix::construct<Assignment>(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[phoenix::bind(assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, Assignment>>(qi::_1, phoenix::construct<Assignment>(qi::_1, qi::_2)))];
assignmentDefinition = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > intExpr > qi::lit(")"))[phoenix::bind(this->state->assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, Assignment>>(qi::_1, phoenix::construct<Assignment>(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > boolExpr > qi::lit(")"))[phoenix::bind(this->state->assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, Assignment>>(qi::_1, phoenix::construct<Assignment>(qi::_1, qi::_2)))];
assignmentDefinition.name("assignment");
assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
assignmentDefinitionList.name("assignment list");
updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::construct<Update>(qi::_1, qi::_a, qi::_b)];
updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::construct<Update>(qi::_1, qi::_a, qi::_b)];
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<Command>(qi::_a, qi::_2, qi::_3)];
commandDefinition = (qi::lit("[") > -((freeIdentifierName[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]) > qi::lit("]") > boolExpr > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::construct<Command>(qi::_a, qi::_2, qi::_3)];
commandDefinition.name("command");
// This block defines all entities that are needed for parsing variable definitions.
booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constBoolExpr[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
[
phoenix::push_back(qi::_r1, phoenix::construct<BooleanVariable>(phoenix::ref(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)),
phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::ref(nextBooleanVariableIndex))),
qi::_a = phoenix::construct<std::shared_ptr<VariableExpression>>(phoenix::new_<VariableExpression>(BaseExpression::bool_, phoenix::ref(nextBooleanVariableIndex), qi::_1)),
phoenix::bind(booleanVariables_.add, qi::_1, qi::_a),
phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1),
phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1),
phoenix::ref(nextBooleanVariableIndex) = phoenix::ref(nextBooleanVariableIndex) + 1
//qi::_a = phoenix::bind(&VariableState<Iterator,Skipper>::addBooleanVariable, *this->state.get(), qi::_1),
qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addBooleanVariable, *this->state, qi::_1, qi::_b),
phoenix::push_back(qi::_r1, phoenix::construct<BooleanVariable>(qi::_a, phoenix::val(qi::_1), qi::_b)),
phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, qi::_a)),
phoenix::bind(this->state->localBooleanVariables_.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<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") > constIntExpr > qi::lit("..") > constIntExpr > qi::lit("]") > -(qi::lit("init") > constIntExpr[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
[
phoenix::push_back(qi::_r1, phoenix::construct<IntegerVariable>(phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)),
phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::ref(nextIntegerVariableIndex))),
qi::_a = phoenix::construct<std::shared_ptr<VariableExpression>>(phoenix::new_<VariableExpression>(BaseExpression::int_, phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3)),
phoenix::bind(integerVariables_.add, qi::_1, qi::_a),
phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1),
phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1),
phoenix::ref(nextIntegerVariableIndex) = phoenix::ref(nextIntegerVariableIndex) + 1
qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addIntegerVariable, *this->state, qi::_1, qi::_2, qi::_3, qi::_b),
phoenix::push_back(qi::_r1, phoenix::construct<IntegerVariable>(qi::_a, qi::_1, qi::_2, qi::_3, qi::_b)),
phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, qi::_a)),
phoenix::bind(this->state->localIntegerVariables_.add, qi::_1, qi::_1)
];
integerVariableDefinition.name("integer variable declaration");
variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4));
@ -223,42 +148,44 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
// This block defines all entities that are needed for parsing a module.
moduleDefinition = (qi::lit("module") >> freeIdentifierName
[phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))]
[phoenix::clear(phoenix::ref(this->state->localBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->localIntegerVariables_))]
>> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule"))
[
phoenix::bind(moduleNames_.add, qi::_1, qi::_1),
phoenix::bind(this->state->moduleNames_.add, qi::_1, qi::_1),
qi::_val = phoenix::construct<Module>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2),
phoenix::bind(moduleMap_.add, qi::_1, qi::_val)
phoenix::bind(this->state->moduleMap_.add, qi::_1, qi::_val)
];
Module const * (qi::symbols<char, Module>::*moduleFinder)(const std::string&) const = &qi::symbols<char, Module>::find;
moduleDefinition.name("module");
moduleRenaming = (qi::lit("module") >> freeIdentifierName >> qi::lit("=")
> moduleNames_ > qi::lit("[") > *(
> this->state->moduleNames_ > qi::lit("[") > *(
(identifierName > qi::lit("=") > identifierName >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))]
) > qi::lit("]") > qi::lit("endmodule"))
[
phoenix::bind(moduleNames_.add, qi::_1, qi::_1),
qi::_val = phoenix::construct<Module>(*phoenix::bind(moduleFinder, moduleMap_, qi::_2), qi::_1, qi::_a, VariableAdder(this)),
phoenix::bind(moduleMap_.add, qi::_1, qi::_val)
phoenix::bind(this->state->moduleNames_.add, qi::_1, qi::_1),
qi::_val = phoenix::construct<Module>(*phoenix::bind(moduleFinder, this->state->moduleMap_, qi::_2), qi::_1, qi::_a, this->state),
phoenix::bind(this->state->moduleMap_.add, qi::_1, qi::_val)
];
moduleRenaming.name("renamed module");
moduleDefinitionList %= +(moduleDefinition | moduleRenaming);
moduleDefinitionList.name("module list");
integerLiteralExpression = qi::int_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<IntegerLiteral>(qi::_1))];
integerLiteralExpression.name("integer literal");
// 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 = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") > booleanLiteralExpression > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->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 = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") > integerLiteralExpression > qi::lit(";"))[phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->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 = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > doubleLiteralExpression > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->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<std::shared_ptr<BooleanConstantExpression>>(phoenix::new_<BooleanConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<BooleanConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)];
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<BooleanConstantExpression>>(phoenix::new_<BooleanConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<BooleanConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->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<std::shared_ptr<IntegerConstantExpression>>(phoenix::new_<IntegerConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<IntegerConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(integerConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)];
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<IntegerConstantExpression>>(phoenix::new_<IntegerConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<IntegerConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->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<std::shared_ptr<DoubleConstantExpression>>(phoenix::new_<DoubleConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<DoubleConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)];
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<DoubleConstantExpression>>(phoenix::new_<DoubleConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<DoubleConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)];
undefinedDoubleConstantDefinition.name("undefined double constant declaration");
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
definedConstantDefinition.name("defined constant declaration");
@ -274,248 +201,19 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
start.name("probabilistic program declaration");
}
bool isFreeIdentifier(std::string& s) const {
if (booleanVariableNames_.find(s) != nullptr) return false;
if (integerVariableNames_.find(s) != nullptr) return false;
if (allConstantNames_.find(s) != nullptr) return false;
if (labelNames_.find(s) != nullptr) return false;
if (moduleNames_.find(s) != nullptr) return false;
if (keywords_.find(s) != nullptr) return false;
return true;
}
bool isIdentifier(std::string& s) const {
if (allConstantNames_.find(s) != nullptr) return false;
if (keywords_.find(s) != nullptr) return false;
return true;
}
struct VariableAdder : public storm::ir::VariableAdder{
VariableAdder(PrismGrammar* grammar) : grammar(grammar) {};
PrismGrammar* grammar;
uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) const {
std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, grammar->nextIntegerVariableIndex, name, lower, upper));
grammar->integerVariables_.add(name, varExpr);
grammar->integerVariableNames_.add(name, name);
grammar->nextIntegerVariableIndex++;
return grammar->nextIntegerVariableIndex-1;
}
uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) const {
std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, grammar->nextBooleanVariableIndex, name));
grammar->integerVariables_.add(name, varExpr);
grammar->integerVariableNames_.add(name, name);
grammar->nextBooleanVariableIndex++;
return grammar->nextBooleanVariableIndex-1;
}
};
void prepareForSecondRun() {
void PrismParser::PrismGrammar::prepareForSecondRun() {
// Clear constants.
integerConstants_.clear();
booleanConstants_.clear();
doubleConstants_.clear();
allConstantNames_.clear();
// Reset variable indices.
nextIntegerVariableIndex = 0;
nextBooleanVariableIndex = 0;
// Clear module names
moduleNames_.clear();
storm::parser::prism::IntegerExpressionGrammar intExpr(this->state);
storm::parser::prism::ConstIntegerExpressionGrammar constIntExpr(this->state);
this->state->prepareForSecondRun();
// Override variable expressions: only allow declared variables.
integerVariableExpression %= integerVariables_;
integerVariableExpression %= this->state->integerVariables_;
integerVariableExpression.name("integer variable");
booleanVariableExpression %= booleanVariables_;
booleanVariableExpression %= this->state->booleanVariables_;
booleanVariableExpression.name("boolean variable");
// Override variable definition: don't register variables again globally.
booleanVariableDefinition = (identifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression) > qi::lit(";"))
[
phoenix::push_back(qi::_r1, phoenix::construct<BooleanVariable>(phoenix::ref(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)),
phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::ref(nextBooleanVariableIndex))),
qi::_a = phoenix::construct<std::shared_ptr<VariableExpression>>(phoenix::new_<VariableExpression>(BaseExpression::bool_, phoenix::ref(nextBooleanVariableIndex), qi::_1)),
phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1),
phoenix::ref(nextBooleanVariableIndex) = phoenix::ref(nextBooleanVariableIndex) + 1
];
booleanVariableDefinition.name("boolean variable declaration");
integerVariableDefinition = (identifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression) > qi::lit(";"))
[
phoenix::push_back(qi::_r1, phoenix::construct<IntegerVariable>(phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)),
phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::ref(nextIntegerVariableIndex))),
qi::_a = phoenix::construct<std::shared_ptr<VariableExpression>>(phoenix::new_<VariableExpression>(BaseExpression::int_, phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3)),
phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1),
phoenix::ref(nextIntegerVariableIndex) = phoenix::ref(nextIntegerVariableIndex) + 1
];
integerVariableDefinition.name("integer variable declaration");
}
// The starting point of the grammar.
qi::rule<Iterator, Program(), qi::locals<std::map<std::string, std::shared_ptr<BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>, std::map<std::string, RewardModel>, std::map<std::string, std::shared_ptr<BaseExpression>>>, Skipper> start;
qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
// Rules for module definition.
qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
qi::rule<Iterator, Module(), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
// Rules for variable definitions.
qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<std::shared_ptr<VariableExpression>, std::shared_ptr<BaseExpression>>, Skipper> booleanVariableDefinition;
qi::rule<Iterator, qi::unused_type(std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<std::shared_ptr<VariableExpression>, std::shared_ptr<BaseExpression>>, Skipper> integerVariableDefinition;
// Rules for command definitions.
qi::rule<Iterator, Command(), qi::locals<std::string>, Skipper> commandDefinition;
qi::rule<Iterator, std::vector<Update>(), Skipper> updateListDefinition;
qi::rule<Iterator, Update(), qi::locals<std::map<std::string, Assignment>, std::map<std::string, Assignment>>, Skipper> updateDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinition;
// Rules for variable/command names.
qi::rule<Iterator, std::string(), Skipper> integerVariableName;
qi::rule<Iterator, std::string(), Skipper> booleanVariableName;
qi::rule<Iterator, std::string(), Skipper> commandName;
qi::rule<Iterator, std::string(), Skipper> unassignedLocalBooleanVariableName;
qi::rule<Iterator, std::string(), Skipper> unassignedLocalIntegerVariableName;
// Rules for reward definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), Skipper> rewardDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), qi::locals<std::vector<StateReward>, std::vector<TransitionReward>>, Skipper> rewardDefinition;
qi::rule<Iterator, StateReward(), Skipper> stateRewardDefinition;
qi::rule<Iterator, TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
// Rules for label definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinition;
// Rules for constant definitions.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&), qi::locals<std::shared_ptr<BooleanConstantExpression>>, Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&), qi::locals<std::shared_ptr<IntegerConstantExpression>>, Skipper> undefinedIntegerConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), qi::locals<std::shared_ptr<DoubleConstantExpression>>, Skipper> undefinedDoubleConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedBooleanConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition;
qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
qi::rule<Iterator, std::string(), Skipper> identifierName;
// The starting point for arbitrary expressions.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> expression;
// Rules with boolean result type.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> orExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> andExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> notExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicBooleanExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> relativeExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantBooleanExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantOrExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAndExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantNotExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicBooleanExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantRelativeExpression;
// Rules with integer result type.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerPlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerPlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicIntegerExpression;
// Rules with double result type.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDoubleExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoublePlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoubleMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicDoubleExpression;
// Rules for variable recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> variableExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableCreatorExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerVariableExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<std::shared_ptr<BaseExpression>>, Skipper> integerVariableCreatorExpression;
// Rules for constant recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleConstantExpression;
// Rules for literal recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> literalExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanLiteralExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleLiteralExpression;
// A structure defining the keywords that are not allowed to be chosen as identifiers.
struct keywordsStruct : qi::symbols<char, unsigned> {
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<char, Program::ModelType> {
modelTypeStruct() {
add
("dtmc", Program::ModelType::DTMC)
("ctmc", Program::ModelType::CTMC)
("mdp", Program::ModelType::MDP)
("ctmdp", 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<char, BinaryRelationExpression::RelationType> {
relationalOperatorStruct() {
add
("=", BinaryRelationExpression::EQUAL)
("<", BinaryRelationExpression::LESS)
("<=", BinaryRelationExpression::LESS_OR_EQUAL)
(">", BinaryRelationExpression::GREATER)
(">=", BinaryRelationExpression::GREATER_OR_EQUAL)
;
}
} relations_;
// Used for indexing the variables.
uint_fast64_t nextBooleanVariableIndex;
uint_fast64_t nextIntegerVariableIndex;
// Structures mapping variable and constant names to the corresponding expression nodes of
// the intermediate representation.
struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerVariables_, booleanVariables_;
struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerConstants_, booleanConstants_, doubleConstants_;
struct qi::symbols<char, Module> moduleMap_;
// A structure representing the identity function over identifier names.
struct variableNamesStruct : qi::symbols<char, std::string> { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_,
localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_;
};
/*!
* Opens the given file for parsing, invokes the helper function to parse the actual content and
@ -564,13 +262,14 @@ std::shared_ptr<storm::ir::Program> PrismParser::parse(std::istream& inputStream
// 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<PositionIteratorType, BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol)> grammar;
PrismGrammar grammar;
try {
// Now parse the content using phrase_parse in order to be able to supply a skipping parser.
// First run.
qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, *result);
grammar.prepareForSecondRun();
result = std::shared_ptr<storm::ir::Program>(new storm::ir::Program());
std::cout << "Now we start the second run..." << std::endl;
// Second run.
qi::phrase_parse(positionIteratorBegin2, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, *result);
std::cout << "Here is the parsed grammar: " << std::endl << result->toString() << std::endl;

111
src/parser/PrismParser.h
View File

@ -10,6 +10,9 @@
// All classes of the intermediate representation are used.
#include "src/ir/IR.h"
#include "src/parser/PrismParser/Includes.h"
#include "src/parser/PrismParser/UtilityGrammars.h"
#include "src/parser/PrismParser/VariableState.h"
// Used for file input.
#include <istream>
@ -19,6 +22,9 @@ namespace storm {
namespace parser {
using namespace storm::ir;
using namespace storm::ir::expressions;
/*!
* This class parses the format of the PRISM model checker into an intermediate representation.
*/
@ -32,6 +38,104 @@ public:
*/
std::shared_ptr<storm::ir::Program> parseFile(std::string const& filename) const;
/*!
* The Boost spirit grammar for the PRISM language. Returns the intermediate representation of
* the input that complies with the PRISM syntax.
*/
class PrismGrammar : public qi::grammar<Iterator, Program(), qi::locals<std::map<std::string, std::shared_ptr<BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>, std::map<std::string, RewardModel>, std::map<std::string, std::shared_ptr<BaseExpression>>>, Skipper> {
public:
PrismGrammar();
void prepareForSecondRun();
private:
std::shared_ptr<storm::parser::prism::VariableState> state;
// The starting point of the grammar.
qi::rule<Iterator, Program(), qi::locals<std::map<std::string, std::shared_ptr<BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>, std::map<std::string, RewardModel>, std::map<std::string, std::shared_ptr<BaseExpression>>>, Skipper> start;
qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
// Rules for module definition.
qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
qi::rule<Iterator, Module(), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
// Rules for variable definitions.
qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> booleanVariableDefinition;
qi::rule<Iterator, qi::unused_type(std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> integerVariableDefinition;
// Rules for command definitions.
qi::rule<Iterator, Command(), qi::locals<std::string>, Skipper> commandDefinition;
qi::rule<Iterator, std::vector<Update>(), Skipper> updateListDefinition;
qi::rule<Iterator, Update(), qi::locals<std::map<std::string, Assignment>, std::map<std::string, Assignment>>, Skipper> updateDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinition;
// Rules for variable/command names.
qi::rule<Iterator, std::string(), Skipper> integerVariableName;
qi::rule<Iterator, std::string(), Skipper> booleanVariableName;
qi::rule<Iterator, std::string(), Skipper> commandName;
qi::rule<Iterator, std::string(), Skipper> unassignedLocalBooleanVariableName;
qi::rule<Iterator, std::string(), Skipper> unassignedLocalIntegerVariableName;
// Rules for reward definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), Skipper> rewardDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), qi::locals<std::vector<StateReward>, std::vector<TransitionReward>>, Skipper> rewardDefinition;
qi::rule<Iterator, StateReward(), Skipper> stateRewardDefinition;
qi::rule<Iterator, TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
// Rules for label definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinition;
// Rules for constant definitions.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&), qi::locals<std::shared_ptr<BooleanConstantExpression>>, Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&), qi::locals<std::shared_ptr<IntegerConstantExpression>>, Skipper> undefinedIntegerConstantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), qi::locals<std::shared_ptr<DoubleConstantExpression>>, Skipper> undefinedDoubleConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedBooleanConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition;
qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
qi::rule<Iterator, std::string(), Skipper> identifierName;
// The starting point for arbitrary expressions.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> expression;
// Rules with double result type.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDoubleExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoublePlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoubleMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicDoubleExpression;
// Rules for variable recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableCreatorExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerVariableExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<std::shared_ptr<BaseExpression>>, Skipper> integerVariableCreatorExpression;
// Rules for constant recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleConstantExpression;
// Rules for literal recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> literalExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanLiteralExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleLiteralExpression;
storm::parser::prism::keywordsStruct keywords_;
storm::parser::prism::modelTypeStruct modelType_;
storm::parser::prism::relationalOperatorStruct relations_;
};
private:
/*!
* Parses the given input stream into the intermediate representation assuming it complies with
@ -41,13 +145,6 @@ private:
* @return a shared pointer to the intermediate representation of the PRISM file.
*/
std::shared_ptr<storm::ir::Program> parse(std::istream& inputStream, std::string const& filename) const;
/*!
* The Boost spirit grammar for the PRISM language. Returns the intermediate representation of
* the input that complies with the PRISM syntax.
*/
template<typename Iterator, typename Skipper>
struct PrismGrammar;
};
} // namespace parser

55
src/parser/PrismParser/BooleanExpressionGrammar.cpp
View File

@ -0,0 +1,55 @@
#include "BooleanExpressionGrammar.h"
namespace storm {
namespace parser {
namespace prism {
BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState>& state)
: BooleanExpressionGrammar::base_type(booleanExpression), state(state) {
IntegerExpressionGrammar intExpr(this->state);
// This rule defines all identifiers that have not been previously used.
identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isIdentifier, this->state.get(), qi::_1) ];
identifierName.name("identifier");
freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isFreeIdentifier, this->state.get(), qi::_1) ];
freeIdentifierName.name("unused identifier");
// This block defines all literal expressions.
booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BooleanLiteral>(qi::_1))];
booleanLiteralExpression.name("boolean literal");
// This block defines all expressions that are variables.
std::shared_ptr<BaseExpression> boolvarexpr = std::shared_ptr<BaseExpression>(new VariableExpression(BaseExpression::bool_, std::numeric_limits<uint_fast64_t>::max(), "bool", std::shared_ptr<BaseExpression>(nullptr), std::shared_ptr<BaseExpression>(nullptr)));
booleanVariableExpression = identifierName[qi::_val = boolvarexpr];
booleanVariableExpression.name("boolean variable");
// This block defines all atomic expressions that are constant, i.e. literals and constants.
booleanConstantExpression %= (this->state->booleanConstants_ | booleanLiteralExpression);
booleanConstantExpression.name("boolean constant or literal");
// This block defines all expressions of type boolean.
relativeExpression = (intExpr >> relations_ >> intExpr)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryRelationExpression>(qi::_1, qi::_3, qi::_2))];
relativeExpression.name("relative 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<std::shared_ptr<UnaryBooleanFunctionExpression>>(phoenix::new_<UnaryBooleanFunctionExpression>(qi::_1, UnaryBooleanFunctionExpression::NOT))];
notExpression.name("boolean expression");
andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryBooleanFunctionExpression>(qi::_val, qi::_1, BinaryBooleanFunctionExpression::AND))];
andExpression.name("boolean expression");
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryBooleanFunctionExpression>(qi::_val, qi::_1, BinaryBooleanFunctionExpression::OR))];
orExpression.name("boolean expression");
booleanExpression %= orExpression;
booleanExpression.name("boolean expression");
// This block defines auxiliary entities that are used to check whether a certain variable exist.
booleanVariableName %= this->state->booleanVariableNames_;
booleanVariableName.name("boolean variable");
unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_;
unassignedLocalBooleanVariableName.name("unassigned local boolean variable");
}
}
}
}

66
src/parser/PrismParser/BooleanExpressionGrammar.h
View File

@ -0,0 +1,66 @@
/*
* File: BooleanExpressionGrammar.h
* Author: nafur
*
* Created on April 10, 2013, 6:27 PM
*/
#ifndef BOOLEANEXPRESSIONGRAMMAR_H
#define BOOLEANEXPRESSIONGRAMMAR_H
#include "Includes.h"
#include "VariableState.h"
#include "IntegerExpressionGrammar.h"
namespace storm {
namespace parser {
namespace prism {
class BooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Skipper> {
public:
BooleanExpressionGrammar(std::shared_ptr<VariableState>& state);
private:
// Rules for variable/command names.
qi::rule<Iterator, std::string(), Skipper> integerVariableName;
qi::rule<Iterator, std::string(), Skipper> booleanVariableName;
qi::rule<Iterator, std::string(), Skipper> unassignedLocalBooleanVariableName;
qi::rule<Iterator, std::string(), Skipper> unassignedLocalIntegerVariableName;
qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
qi::rule<Iterator, std::string(), Skipper> identifierName;
// The starting point for arbitrary expressions.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> expression;
// Rules with boolean result type.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Skipper> booleanExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> orExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> andExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> notExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicBooleanExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> relativeExpression;
// Rules for variable recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableCreatorExpression;
// Rules for constant recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanConstantExpression;
// Rules for literal recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanLiteralExpression;
// A structure mapping the textual representation of a binary relation to the representation
// of the intermediate representation.
storm::parser::prism::relationalOperatorStruct relations_;
std::shared_ptr<storm::parser::prism::VariableState> state;
};
}
}
}
#endif /* BOOLEANEXPRESSIONGRAMMAR_H */

32
src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp
View File

@ -0,0 +1,32 @@
#include "ConstBooleanExpressionGrammar.h"
namespace storm {
namespace parser {
namespace prism {
ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state)
: ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), state(state) {
ConstIntegerExpressionGrammar constIntExpr(this->state);
booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BooleanLiteral>(qi::_1))];
booleanLiteralExpression.name("boolean literal");
booleanConstantExpression %= (this->state->booleanConstants_ | booleanLiteralExpression);
booleanConstantExpression.name("boolean constant or literal");
constantRelativeExpression = (constIntExpr >> relations_ >> constIntExpr)[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryRelationExpression>(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<std::shared_ptr<UnaryBooleanFunctionExpression>>(phoenix::new_<UnaryBooleanFunctionExpression>(qi::_1, UnaryBooleanFunctionExpression::NOT))];
constantNotExpression.name("constant boolean expression");
constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryBooleanFunctionExpression>(qi::_val, qi::_1, BinaryBooleanFunctionExpression::AND))];
constantAndExpression.name("constant boolean expression");
constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryBooleanFunctionExpression>(qi::_val, qi::_1, BinaryBooleanFunctionExpression::OR))];
constantOrExpression.name("constant boolean expression");
constantBooleanExpression %= constantOrExpression;
constantBooleanExpression.name("constant boolean expression");
}
}
}
}

49
src/parser/PrismParser/ConstBooleanExpressionGrammar.h
View File

@ -0,0 +1,49 @@
/*
* File: ConstBooleanExpressionGrammar.h
* Author: nafur
*
* Created on April 10, 2013, 6:34 PM
*/
#ifndef CONSTBOOLEANEXPRESSIONGRAMMAR_H
#define CONSTBOOLEANEXPRESSIONGRAMMAR_H
#include "Includes.h"
#include "ConstIntegerExpressionGrammar.h"
#include "VariableState.h"
#include "UtilityGrammars.h"
namespace storm {
namespace parser {
namespace prism {
class ConstBooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Skipper> {
public:
ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state);
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanLiteralExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> relativeExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Skipper> constantBooleanExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantOrExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAndExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantNotExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicBooleanExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantRelativeExpression;
storm::parser::prism::relationalOperatorStruct relations_;
std::shared_ptr<storm::parser::prism::VariableState> state;
};
}
}
}
#endif /* CONSTBOOLEANEXPRESSIONGRAMMAR_H */

30
src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp
View File

@ -0,0 +1,30 @@
#include "ConstIntegerExpressionGrammar.h"
namespace storm {
namespace parser {
namespace prism {
ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr<VariableState>& state)
: ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), state(state) {
integerLiteralExpression = qi::int_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<IntegerLiteral>(qi::_1))];
integerLiteralExpression.name("integer literal");
integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression);
integerConstantExpression.name("integer constant or literal");
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<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::TIMES))];
constantIntegerMultExpression.name("constant integer expression");
constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::MINUS))]];
constantIntegerPlusExpression.name("constant integer expression");
constantIntegerExpression %= constantIntegerPlusExpression;
constantIntegerExpression.name("constant integer expression");
}
}
}
}

38
src/parser/PrismParser/ConstIntegerExpressionGrammar.h
View File

@ -0,0 +1,38 @@
/*
* File: ConstIntegerExpressionGrammar.h
* Author: nafur
*
* Created on April 10, 2013, 6:02 PM
*/
#ifndef CONSTINTEGEREXPRESSIONGRAMMAR_H
#define CONSTINTEGEREXPRESSIONGRAMMAR_H
#include "Includes.h"
#include "VariableState.h"
namespace storm {
namespace parser {
namespace prism {
class ConstIntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Skipper> {
public:
ConstIntegerExpressionGrammar(std::shared_ptr<VariableState>& state);
private:
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Skipper> constantIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerPlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicIntegerExpression;
std::shared_ptr<VariableState> state;
};
}
}
}
#endif /* CONSTINTEGEREXPRESSIONGRAMMAR_H */

35
src/parser/PrismParser/Includes.h
View File

@ -0,0 +1,35 @@
/*
* File: BoostIncludes.h
* Author: nafur
*
* Created on April 10, 2013, 4:46 PM
*/
#ifndef BOOSTINCLUDES_H
#define BOOSTINCLUDES_H
// Used for Boost spirit.
#include <boost/typeof/typeof.hpp>
#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix.hpp>
// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
#include <boost/spirit/include/classic_position_iterator.hpp>
#include <boost/spirit/include/support_multi_pass.hpp>
namespace qi = boost::spirit::qi;
namespace phoenix = boost::phoenix;
typedef std::string::const_iterator BaseIteratorType;
typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
typedef PositionIteratorType Iterator;
typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
#include "src/ir/IR.h"
using namespace storm::ir;
using namespace storm::ir::expressions;
#include "UtilityGrammars.h"
#endif /* BOOSTINCLUDES_H */

46
src/parser/PrismParser/IntegerExpressionGrammar.cpp
View File

@ -0,0 +1,46 @@
#include "IntegerExpressionGrammar.h"
namespace storm {
namespace parser {
namespace prism {
IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr<VariableState>& state)
: IntegerExpressionGrammar::base_type(integerExpression), state(state) {
// This rule defines all identifiers that have not been previously used.
identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ];
identifierName.name("identifier");
// This block defines all literal expressions.
integerLiteralExpression = qi::int_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<IntegerLiteral>(qi::_1))];
integerLiteralExpression.name("integer literal");
// This block defines all expressions that are variables.
std::shared_ptr<BaseExpression> intvarexpr = std::shared_ptr<BaseExpression>(new VariableExpression(BaseExpression::int_, std::numeric_limits<uint_fast64_t>::max(), "int", std::shared_ptr<BaseExpression>(nullptr), std::shared_ptr<BaseExpression>(nullptr)));
integerVariableExpression = identifierName[qi::_val = intvarexpr];
integerVariableExpression.name("integer variable");
// This block defines all atomic expressions that are constant, i.e. literals and constants.
integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression);
integerConstantExpression.name("integer 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<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::TIMES))];
integerMultExpression.name("integer expression");
integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<BinaryNumericalFunctionExpression>(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::MINUS))]];
integerPlusExpression.name("integer expression");
integerExpression %= integerPlusExpression;
integerExpression.name("integer expression");
}
void IntegerExpressionGrammar::prepareForSecondRun() {
// Override variable expressions: only allow declared variables.
integerVariableExpression %= this->state->integerVariables_;
integerVariableExpression.name("integer variable");
}
}
}
}

61
src/parser/PrismParser/IntegerExpressionGrammar.h
View File

@ -0,0 +1,61 @@
/*
* File: IntegerExpressionGrammar.h
* Author: nafur
*
* Created on April 10, 2013, 4:39 PM
*/
#ifndef INTEGEREXPRESSIONGRAMMAR_H
#define INTEGEREXPRESSIONGRAMMAR_H
#include "src/ir/IR.h"
#include "VariableState.h"
#include "Includes.h"
#include <memory>
namespace storm {
namespace parser {
namespace prism {
class IntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Skipper> {
public:
IntegerExpressionGrammar(std::shared_ptr<VariableState>& state);
void prepareForSecondRun();
private:
qi::rule<Iterator, std::string(), Skipper> identifierName;
// The starting point for arbitrary expressions.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> expression;
// Rules with integer result type.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Skipper> integerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerPlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerPlusExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerMultExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicIntegerExpression;
// Rules for variable recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerVariableExpression;
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<std::shared_ptr<BaseExpression>>, Skipper> integerVariableCreatorExpression;
// Rules for constant recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression;
// Rules for literal recognition.
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
std::shared_ptr<VariableState> state;
};
}
}
}
#endif /* INTEGEREXPRESSIONGRAMMAR_H */

69
src/parser/PrismParser/UtilityGrammars.h
View File

@ -0,0 +1,69 @@
/*
* File: Keywords.h
* Author: nafur
*
* Created on April 10, 2013, 6:03 PM
*/
#ifndef KEYWORDS_H
#define KEYWORDS_H
#include "Includes.h"
namespace storm {
namespace parser {
namespace prism {
// A structure defining the keywords that are not allowed to be chosen as identifiers.
struct keywordsStruct : qi::symbols<char, unsigned> {
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)
;
}
};
// A structure mapping the textual representation of a model type to the model type
// representation of the intermediate representation.
struct modelTypeStruct : qi::symbols<char, Program::ModelType> {
modelTypeStruct() {
add
("dtmc", Program::ModelType::DTMC)
("ctmc", Program::ModelType::CTMC)
("mdp", Program::ModelType::MDP)
("ctmdp", Program::ModelType::CTMDP)
;
}
};
// A structure mapping the textual representation of a binary relation to the representation
// of the intermediate representation.
struct relationalOperatorStruct : qi::symbols<char, BinaryRelationExpression::RelationType> {
relationalOperatorStruct() {
add
("=", BinaryRelationExpression::EQUAL)
("<", BinaryRelationExpression::LESS)
("<=", BinaryRelationExpression::LESS_OR_EQUAL)
(">", BinaryRelationExpression::GREATER)
(">=", BinaryRelationExpression::GREATER_OR_EQUAL)
;
}
};
}
}
}
#endif /* KEYWORDS_H */

96
src/parser/PrismParser/VariableState.h
View File

@ -0,0 +1,96 @@
/*
* File: VariableState.h
* Author: nafur
*
* Created on April 10, 2013, 4:43 PM
*/
#ifndef VARIABLESTATE_H
#define VARIABLESTATE_H
#include "src/ir/IR.h"
#include "Includes.h"
namespace storm {
namespace parser {
namespace prism {
using namespace storm::ir;
using namespace storm::ir::expressions;
struct VariableState : public storm::ir::VariableAdder {
public:
VariableState()
: keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0)
{
}
keywordsStruct keywords;
// Used for indexing the variables.
uint_fast64_t nextBooleanVariableIndex;
uint_fast64_t nextIntegerVariableIndex;
// Structures mapping variable and constant names to the corresponding expression nodes of
// the intermediate representation.
struct qi::symbols<char, std::shared_ptr<VariableExpression>> integerVariables_, booleanVariables_;
struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerConstants_, booleanConstants_, doubleConstants_;
struct qi::symbols<char, Module> moduleMap_;
// A structure representing the identity function over identifier names.
struct variableNamesStruct : qi::symbols<char, std::string> { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_,
localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_;
uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) {
std::shared_ptr<VariableExpression> res = this->booleanVariables_.at(name);
if (res != nullptr) {
return res->getVariableIndex();
}
std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name));
this->booleanVariables_.add(name, varExpr);
this->booleanVariableNames_.add(name, name);
this->nextBooleanVariableIndex++;
return this->nextBooleanVariableIndex-1;
}
uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) {
std::shared_ptr<VariableExpression> res = this->integerVariables_.at(name);
if (res != nullptr) {
return res->getVariableIndex();
}
std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextIntegerVariableIndex, name, lower, upper));
this->integerVariables_.add(name, varExpr);
this->integerVariableNames_.add(name, name);
this->nextIntegerVariableIndex++;
return this->nextIntegerVariableIndex-1;
}
bool isFreeIdentifier(std::string& s) const {
if (this->integerVariableNames_.find(s) != nullptr) return false;
if (this->allConstantNames_.find(s) != nullptr) return false;
if (this->labelNames_.find(s) != nullptr) return false;
if (this->moduleNames_.find(s) != nullptr) return false;
if (this->keywords.find(s) != nullptr) return false;
return true;
}
bool isIdentifier(std::string& s) const {
if (this->allConstantNames_.find(s) != nullptr) return false;
if (this->keywords.find(s) != nullptr) return false;
return true;
}
void prepareForSecondRun() {
integerConstants_.clear();
booleanConstants_.clear();
doubleConstants_.clear();
allConstantNames_.clear();
}
};
}
}
}
#endif /* VARIABLESTATE_H */
Write Preview
Loading…
Cancel
Save