|
|
|
@ -9,25 +9,18 @@ |
|
|
|
|
|
|
|
#include "src/utility/OsDetection.h"
|
|
|
|
|
|
|
|
#include "src/parser/PrismParser/Includes.h"
|
|
|
|
#include "src/parser/PrismParser/BooleanExpressionGrammar.h"
|
|
|
|
#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h"
|
|
|
|
#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h"
|
|
|
|
#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h"
|
|
|
|
#include "src/parser/PrismParser/IntegerExpressionGrammar.h"
|
|
|
|
#include "src/parser/PrismParser/IdentifierGrammars.h"
|
|
|
|
#include "src/parser/PrismParser/VariableState.h"
|
|
|
|
|
|
|
|
// If the parser fails due to ill-formed data, this exception is thrown.
|
|
|
|
#include "src/exceptions/WrongFileFormatException.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>
|
|
|
|
|
|
|
|
// Needed for file IO.
|
|
|
|
#include <fstream>
|
|
|
|
#include <iomanip>
|
|
|
|
@ -46,37 +39,84 @@ namespace parser { |
|
|
|
void dump(const std::string& s) { |
|
|
|
std::cerr << "Dump: " << s << std::endl; |
|
|
|
} |
|
|
|
/*void dump(const std::string& s, ) {
|
|
|
|
std::cerr << "Dump: " << s << std::endl; |
|
|
|
}*/ |
|
|
|
|
|
|
|
std::shared_ptr<BaseExpression> addIntegerConstant(const std::string& name, const std::shared_ptr<BaseExpression> value, std::shared_ptr<prism::VariableState> state) { |
|
|
|
std::cerr << "addIntegerConstant: " << name << std::endl; |
|
|
|
state->integerConstants_.add(name, value); |
|
|
|
state->allConstantNames_.add(name, name); |
|
|
|
std::shared_ptr<BaseExpression> PrismParser::PrismGrammar::addIntegerConstant(const std::string& name, const std::shared_ptr<BaseExpression> value) { |
|
|
|
this->state->integerConstants_.add(name, value); |
|
|
|
this->state->allConstantNames_.add(name, name); |
|
|
|
return value; |
|
|
|
} |
|
|
|
|
|
|
|
PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type(start), state(new storm::parser::prism::VariableState()) { |
|
|
|
void PrismParser::PrismGrammar::addLabel(const std::string& name, std::shared_ptr<BaseExpression> value, std::map<std::string, std::shared_ptr<BaseExpression>>& mapping) { |
|
|
|
this->state->labelNames_.add(name, name); |
|
|
|
mapping[name] = value; |
|
|
|
} |
|
|
|
void PrismParser::PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping) { |
|
|
|
this->state->assignedLocalIntegerVariables_.add(variable, variable); |
|
|
|
mapping[variable] = Assignment(variable, value); |
|
|
|
} |
|
|
|
void PrismParser::PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping) { |
|
|
|
this->state->assignedLocalBooleanVariables_.add(variable, variable); |
|
|
|
mapping[variable] = Assignment(variable, value); |
|
|
|
} |
|
|
|
std::shared_ptr<Module> PrismParser::PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map<std::string, std::string>& mapping) { |
|
|
|
this->state->moduleNames_.add(name, name); |
|
|
|
std::shared_ptr<Module> old = this->state->moduleMap_.at(oldname); |
|
|
|
if (old == nullptr) { |
|
|
|
std::cerr << "Renaming module failed: module " << oldname << " does not exist!" << std::endl; |
|
|
|
return nullptr; |
|
|
|
} |
|
|
|
std::shared_ptr<Module> res = std::shared_ptr<Module>(new Module(*old, name, mapping, this->state)); |
|
|
|
this->state->moduleMap_.add(name, res); |
|
|
|
return res; |
|
|
|
} |
|
|
|
std::shared_ptr<Module> PrismParser::PrismGrammar::createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<std::shared_ptr<storm::ir::Command>> commands) { |
|
|
|
this->state->moduleNames_.add(name, name); |
|
|
|
std::shared_ptr<Module> res = std::shared_ptr<Module>(new Module(name, bools, ints, boolids, intids, commands)); |
|
|
|
this->state->moduleMap_.add(name, res); |
|
|
|
return res; |
|
|
|
} |
|
|
|
|
|
|
|
// 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, 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, qi::_1) ]; |
|
|
|
freeIdentifierName.name("unused identifier"); |
|
|
|
std::shared_ptr<StateReward> createStateReward(std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) { |
|
|
|
return std::shared_ptr<StateReward>(new StateReward(guard, reward)); |
|
|
|
} |
|
|
|
std::shared_ptr<TransitionReward> createTransitionReward(std::string label, std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) { |
|
|
|
return std::shared_ptr<TransitionReward>(new TransitionReward(label, guard, reward)); |
|
|
|
} |
|
|
|
void createRewardModel(std::string name, std::vector<std::shared_ptr<StateReward>>& stateRewards, std::vector<std::shared_ptr<TransitionReward>>& transitionRewards, std::map<std::string, std::shared_ptr<RewardModel>>& mapping) { |
|
|
|
mapping[name] = std::shared_ptr<RewardModel>(new RewardModel(name, stateRewards, transitionRewards)); |
|
|
|
} |
|
|
|
std::shared_ptr<Update> createUpdate(std::shared_ptr<BaseExpression> likelihood, std::map<std::string, Assignment>& bools, std::map<std::string, Assignment> ints) { |
|
|
|
return std::shared_ptr<Update>(new Update(likelihood, bools, ints)); |
|
|
|
} |
|
|
|
std::shared_ptr<Command> createCommand(std::string& label, std::shared_ptr<BaseExpression> guard, std::vector<std::shared_ptr<Update>>& updates) { |
|
|
|
return std::shared_ptr<Command>(new Command(label, guard, updates)); |
|
|
|
} |
|
|
|
std::shared_ptr<Program> createProgram( |
|
|
|
Program::ModelType modelType, |
|
|
|
std::map<std::string, std::shared_ptr<BooleanConstantExpression>> undefBoolConst, |
|
|
|
std::map<std::string, std::shared_ptr<IntegerConstantExpression>> undefIntConst, |
|
|
|
std::map<std::string, std::shared_ptr<DoubleConstantExpression>> undefDoubleConst, |
|
|
|
std::vector<std::shared_ptr<Module>> modules, |
|
|
|
std::map<std::string, std::shared_ptr<RewardModel>> rewards, |
|
|
|
std::map<std::string, std::shared_ptr<BaseExpression>> labels) { |
|
|
|
return std::shared_ptr<Program>(new Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, modules, rewards, labels)); |
|
|
|
} |
|
|
|
|
|
|
|
PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type(start), state(new storm::parser::prism::VariableState()) { |
|
|
|
|
|
|
|
// This block defines all entities that are needed for parsing labels.
|
|
|
|
labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> prism::BooleanExpressionGrammar::instance(this->state) >> 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 = (qi::lit("label") >> -qi::lit("\"") >> prism::FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> prism::BooleanExpressionGrammar::instance(this->state) >> qi::lit(";")) |
|
|
|
[phoenix::bind(&PrismParser::PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)]; |
|
|
|
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 = (prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::construct<StateReward>(qi::_1, qi::_2)]; |
|
|
|
stateRewardDefinition = (prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::bind(&createStateReward, qi::_1, qi::_2)]; |
|
|
|
stateRewardDefinition.name("state reward definition"); |
|
|
|
transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::construct<TransitionReward>(qi::_a, qi::_2, qi::_3)]; |
|
|
|
transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::bind(&createTransitionReward, 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 = (qi::lit("rewards") > qi::lit("\"") > prism::FreeIdentifierGrammar::instance(this->state) > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards")) |
|
|
|
[phoenix::bind(&createRewardModel, qi::_1, qi::_a, qi::_b, qi::_r1)]; |
|
|
|
rewardDefinition.name("reward definition"); |
|
|
|
rewardDefinitionList = *rewardDefinition(qi::_r1); |
|
|
|
rewardDefinitionList.name("reward definition list"); |
|
|
|
@ -89,23 +129,25 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type |
|
|
|
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("=") > prism::IntegerExpressionGrammar::instance(this->state) > 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("=") > prism::BooleanExpressionGrammar::instance(this->state) > 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 = |
|
|
|
(qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > prism::IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismParser::PrismGrammar::addIntAssignment, this, qi::_1, qi::_2, qi::_r2)] | |
|
|
|
(qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismParser::PrismGrammar::addBoolAssignment, this, qi::_1, qi::_2, qi::_r1)]; |
|
|
|
assignmentDefinition.name("assignment"); |
|
|
|
assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; |
|
|
|
assignmentDefinitionList.name("assignment list"); |
|
|
|
updateDefinition = (prism::ConstDoubleExpressionGrammar::instance(this->state) > 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 = (prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; |
|
|
|
updateDefinition.name("update"); |
|
|
|
updateListDefinition = +updateDefinition % "+"; |
|
|
|
updateListDefinition.name("update list"); |
|
|
|
commandDefinition = ( |
|
|
|
qi::lit("[") > -( |
|
|
|
(freeIdentifierName[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1] |
|
|
|
(prism::FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1] |
|
|
|
) > qi::lit("]") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";") |
|
|
|
)[qi::_val = phoenix::construct<Command>(qi::_a, qi::_2, qi::_3)]; |
|
|
|
)[qi::_val = phoenix::bind(&createCommand, 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") > prism::ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";")) |
|
|
|
booleanVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > prism::ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";")) |
|
|
|
[ |
|
|
|
//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), |
|
|
|
@ -117,7 +159,7 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type |
|
|
|
|
|
|
|
integerLiteralExpression = qi::int_[qi::_val = phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<IntegerLiteral>(qi::_1))]; |
|
|
|
integerLiteralExpression.name("integer literal"); |
|
|
|
integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") > integerLiteralExpression > qi::lit("..") > integerLiteralExpression > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";")) |
|
|
|
integerVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > integerLiteralExpression > qi::lit("..") > integerLiteralExpression > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";")) |
|
|
|
[ |
|
|
|
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)), |
|
|
|
@ -129,69 +171,53 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type |
|
|
|
variableDefinition.name("variable declaration"); |
|
|
|
|
|
|
|
// This block defines all entities that are needed for parsing a module.
|
|
|
|
moduleDefinition = (qi::lit("module") >> freeIdentifierName |
|
|
|
[phoenix::bind(&prism::VariableState::startModule, *this->state)] |
|
|
|
moduleDefinition = (qi::lit("module") >> prism::FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&prism::VariableState::startModule, *this->state)] |
|
|
|
>> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule")) |
|
|
|
[ |
|
|
|
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(this->state->moduleMap_.add, qi::_1, qi::_val) |
|
|
|
]; |
|
|
|
[phoenix::bind(&PrismParser::PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)]; |
|
|
|
|
|
|
|
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("=") |
|
|
|
moduleRenaming = (qi::lit("module") >> prism::FreeIdentifierGrammar::instance(this->state) >> 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))] |
|
|
|
(prism::IdentifierGrammar::instance(this->state) > qi::lit("=") > prism::IdentifierGrammar::instance(this->state) >> -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(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) |
|
|
|
|
|
|
|
]; |
|
|
|
[phoenix::bind(&PrismParser::PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)]; |
|
|
|
moduleRenaming.name("renamed module"); |
|
|
|
moduleDefinitionList %= +(moduleDefinition | moduleRenaming); |
|
|
|
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("=") > prism::ConstBooleanExpressionGrammar::instance(this->state) > 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 = (qi::lit("const") >> qi::lit("bool") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > prism::ConstBooleanExpressionGrammar::instance(this->state) > 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")[phoenix::bind(&dump, "const int")] >> |
|
|
|
freeIdentifierName >> |
|
|
|
qi::lit("=")[phoenix::bind(&dump, "const int <ident> = ")] >> |
|
|
|
//constIntExpr.integerLiteralExpression[phoenix::bind(&dump, "const int <ident> = <value>")] >>
|
|
|
|
prism::ConstIntegerExpressionGrammar::instance(this->state)[phoenix::bind(&dump, "const int <ident> = <value>")] >> |
|
|
|
qi::lit(";")[phoenix::bind(&dump, "const int <ident> = <value>;")] |
|
|
|
)[ qi::_val = phoenix::bind(&addIntegerConstant, qi::_1, qi::_2, this->state) ]; |
|
|
|
qi::lit("const") >> qi::lit("int") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> |
|
|
|
prism::ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";") |
|
|
|
)[ qi::_val = phoenix::bind(&PrismParser::PrismGrammar::addIntegerConstant, this, qi::_1, qi::_2) ]; |
|
|
|
definedIntegerConstantDefinition.name("defined integer constant declaration"); |
|
|
|
definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > prism::ConstDoubleExpressionGrammar::instance(this->state) > 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 = (qi::lit("const") >> qi::lit("double") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > prism::ConstDoubleExpressionGrammar::instance(this->state) > 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(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; |
|
|
|
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > prism::FreeIdentifierGrammar::instance(this->state) > 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(this->state->integerConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; |
|
|
|
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > prism::FreeIdentifierGrammar::instance(this->state) > 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(this->state->doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; |
|
|
|
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > prism::FreeIdentifierGrammar::instance(this->state) > 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[phoenix::bind(&dump, "<defBoolConst>")] | definedIntegerConstantDefinition[phoenix::bind(&dump, "<defIntConst>")] | definedDoubleConstantDefinition[phoenix::bind(&dump, "<defDoubleConst>")]); |
|
|
|
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[phoenix::bind(&dump, "<defConst>")] | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)[phoenix::bind(&dump, "<undefConst>")]); |
|
|
|
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[phoenix::bind(&dump, "<model type>")] > |
|
|
|
constantDefinitionList(qi::_a, qi::_b, qi::_c)[phoenix::bind(&dump, "<constants>")] > |
|
|
|
moduleDefinitionList[phoenix::bind(&dump, "<modules>")] > |
|
|
|
rewardDefinitionList(qi::_d)[phoenix::bind(&dump, "<rewards>")] > |
|
|
|
labelDefinitionList(qi::_e)[phoenix::bind(&dump, "<labels>")] |
|
|
|
)[qi::_val = phoenix::construct<Program>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; |
|
|
|
modelTypeDefinition > |
|
|
|
constantDefinitionList(qi::_a, qi::_b, qi::_c) > |
|
|
|
moduleDefinitionList > |
|
|
|
rewardDefinitionList(qi::_d) > |
|
|
|
labelDefinitionList(qi::_e) |
|
|
|
)[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; |
|
|
|
start.name("probabilistic program declaration"); |
|
|
|
} |
|
|
|
|
|
|
|
@ -250,12 +276,12 @@ std::shared_ptr<storm::ir::Program> PrismParser::parse(std::istream& inputStream |
|
|
|
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); |
|
|
|
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); |
|
|
|
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; |
|
|
|
} catch(const qi::expectation_failure<PositionIteratorType>& e) { |
|
|
|
// If the parser expected content different than the one provided, display information
|
|
|
|
|
gereon
12 years ago