From 3f3b154ce0781a082acf75211f9609b24385bbb4 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 12 Aug 2020 10:37:43 +0200 Subject: [PATCH] first progress on player parsing WIP. This does currently not compile, having troubles with the parsing of command and module names into their resp. vectors. --- src/storm-parsers/parser/PrismParser.cpp | 28 +++++++++++++++++++----- src/storm-parsers/parser/PrismParser.h | 10 +++++---- 2 files changed, 29 insertions(+), 9 deletions(-) diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 3a6be1ed2..732111bdb 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -272,20 +272,31 @@ namespace storm { // We first check for a module renaming, i.e., for this rule we certainly have to see a module definition moduleDefinition = ((qi::lit("module") > freshModuleName > *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3, qi::_r1)]; moduleDefinition.name("module definition"); - + + commandName = (qi::lit("[") >> identifier >> qi::lit("]"))[qi::_val = qi::_1]; + moduleName = identifier[qi::_val = qi::_1]; + + playerDefinition = (qi::lit("player") >> identifier[qi::_a = qi::_1] + >> +( commandName(qi::_1)[phoenix::push_back(qi::_b, qi::_1)] + | moduleName(qi::_1)[phoenix::push_back(qi::_c, qi::_1)] + ) + >> qi::lit("endplayer"))[qi::_val = phoenix::bind(&PrismParser::createPlayer, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; + playerDefinition.name("player definition"); + moduleRenaming = (qi::lit("[") > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] % ",") > qi::lit("]"))[qi::_val = phoenix::bind(&PrismParser::createModuleRenaming, phoenix::ref(*this), qi::_a)]; moduleRenaming.name("Module renaming list"); - + renamedModule = (((qi::lit("module") > freshModuleName) >> qi::lit("=")) > knownModuleName[qi::_a = qi::_1] > (moduleRenaming[qi::_b = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isValidModuleRenaming, phoenix::ref(*this), qi::_a, qi::_b, qi::_r1)] > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createRenamedModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_r1)]; renamedModule.name("module definition via renaming"); - + start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), phoenix::ref(globalProgramInformation))] > modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)] > -observablesConstruct > *( definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)] + | playerDefinition | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)] | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] | globalVariableDefinition(phoenix::ref(globalProgramInformation)) @@ -755,12 +766,19 @@ namespace storm { this->observables.insert(observables.begin(), observables.end()); // We need this list to be filled in both runs. } - + storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, boost::optional const& invariant, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const { globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size(); return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename()); } - + + storm::prism::Player PrismParser::createPlayer(std::string const& playerName, std::vector const& moduleNames, std::vector const & commandNames) const { + STORM_LOG_DEBUG("PLAYER created:" << playerName); + std::vector modules; + std::vector commands; + return storm::prism::Player(playerName, modules, commands); + } + bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const { if (!this->secondRun) { auto const& renaming = moduleRenaming.getRenaming(); diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index f3058e9d0..f25725c9d 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -62,11 +62,12 @@ namespace storm { std::vector rewardModels; std::vector labels; std::vector observationLabels; + std::vector players; bool hasInitialConstruct; storm::prism::InitialConstruct initialConstruct; boost::optional systemCompositionConstruct; - + // Counters to provide unique indexing for commands and updates. uint_fast64_t currentCommandIndex; uint_fast64_t currentUpdateIndex; @@ -263,7 +264,8 @@ namespace storm { qi::rule, Skipper> transitionRewardDefinition; // Rules for player definitions - qi::rule commandName; + qi::rule, Skipper> commandName; + qi::rule, Skipper> moduleName; qi::rule playerDefinition; // Rules for initial states expression. @@ -361,12 +363,13 @@ namespace storm { storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, boost::optional const& invariant, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; storm::prism::ModuleRenaming createModuleRenaming(std::map const& renaming) const; storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, storm::prism::ModuleRenaming const& renaming, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::Player createPlayer(std::string const& playerName, std::vector const& moduleNames, std::vector const & commandNames) const; storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; void createObservablesList(std::vector const& observables); void removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const; - + // An error handler function. phoenix::function handler; }; @@ -374,4 +377,3 @@ namespace storm { } // namespace storm #endif /* STORM_PARSER_PRISMPARSER_H_ */ -