From 3b76126f6bb5feeb0d24be253bb3a2855c5aa724 Mon Sep 17 00:00:00 2001 From: gereon Date: Tue, 30 Apr 2013 17:50:21 +0200 Subject: [PATCH] Split PrismParser and PrismGrammar in differenc object files. Added reset method for grammars, now we can parse multiple files in one program execution. Added test for mdp parsing. --- src/models/Mdp.h | 8 + src/parser/PrismParser.cpp | 236 +--------------------- src/parser/PrismParser.h | 109 ---------- src/parser/PrismParser/BaseGrammar.h | 5 +- src/parser/PrismParser/PrismGrammar.cpp | 258 ++++++++++++++++++++++++ src/parser/PrismParser/PrismGrammar.h | 142 +++++++++++++ test/parser/ParsePrismTest.cpp | 14 +- 7 files changed, 434 insertions(+), 338 deletions(-) create mode 100644 src/parser/PrismParser/PrismGrammar.cpp create mode 100644 src/parser/PrismParser/PrismGrammar.h diff --git a/src/models/Mdp.h b/src/models/Mdp.h index dc58782a2..8c06a5deb 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -89,6 +89,14 @@ public: uint_fast64_t getNumberOfStates() const { return this->probabilityMatrix->getColumnCount(); } + + /*! + * Returns the number of choices for all states of the MDP. + * @return The number of choices for all states of the MDP. + */ + uint_fast64_t getNumberOfChoices() const { + return this->probabilityMatrix->getRowCount(); + } /*! * Returns the number of (non-zero) transitions of the MDP. diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 903a02d6a..ce58bd988 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -9,14 +9,7 @@ #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" +#include "src/parser/PrismParser/PrismGrammar.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFileFormatException.h" @@ -30,234 +23,17 @@ #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; -// Some typedefs and namespace definitions to reduce code size. -typedef std::string::const_iterator BaseIteratorType; -typedef boost::spirit::classic::position_iterator2 PositionIteratorType; -namespace qi = boost::spirit::qi; -namespace phoenix = boost::phoenix; namespace storm { - namespace parser { - void dump(const std::string& s) { - std::cerr << "Dump: " << s << std::endl; - } - - std::shared_ptr PrismParser::PrismGrammar::addIntegerConstant(const std::string& name, const std::shared_ptr value) { - this->state->integerConstants_.add(name, value); - this->state->allConstantNames_.add(name, name); - return value; - } - - void PrismParser::PrismGrammar::addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping) { - this->state->labelNames_.add(name, name); - mapping[name] = value; - } - void PrismParser::PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { - //std::cout << "Adding int assignment for " << variable << std::endl; - this->state->assignedLocalIntegerVariables_.add(variable, variable); - mapping[variable] = Assignment(variable, value); - } - void PrismParser::PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { - //std::cout << "Adding bool assignment for " << variable << std::endl; - this->state->assignedLocalBooleanVariables_.add(variable, variable); - mapping[variable] = Assignment(variable, value); - } - Module PrismParser::PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map& mapping) { - this->state->moduleNames_.add(name, name); - Module* old = this->state->moduleMap_.find(oldname); - if (old == nullptr) { - LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldname << " does not exist!"); - throw "Renaming module failed"; - } - Module res(*old, name, mapping, this->state); - this->state->moduleMap_.at(name) = res; - return res; - } - Module PrismParser::PrismGrammar::createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands) { - this->state->moduleNames_.add(name, name); - Module res(name, bools, ints, boolids, intids, commands); - this->state->moduleMap_.at(name) = res; - return res; - } - - void PrismParser::PrismGrammar::createIntegerVariable(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids) { - //std::cout << "Creating int " << name << " = " << init << std::endl; - uint_fast64_t id = this->state->addIntegerVariable(name, lower, upper, init); - vars.emplace_back(id, name, lower, upper, init); - varids[name] = id; - this->state->localIntegerVariables_.add(name, name); - } - void PrismParser::PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids) { - //std::cout << "Creating bool " << name << std::endl; - uint_fast64_t id = this->state->addBooleanVariable(name, init); - vars.emplace_back(id, name, init); - varids[name] = id; - this->state->localBooleanVariables_.add(name, name); - } - - StateReward createStateReward(std::shared_ptr guard, std::shared_ptr reward) { - return StateReward(guard, reward); - } - TransitionReward createTransitionReward(std::string label, std::shared_ptr guard, std::shared_ptr reward) { - return TransitionReward(label, guard, reward); - } - void createRewardModel(std::string name, std::vector& stateRewards, std::vector& transitionRewards, std::map& mapping) { - mapping[name] = RewardModel(name, stateRewards, transitionRewards); - } - Update createUpdate(std::shared_ptr likelihood, std::map& bools, std::map ints) { - return Update(likelihood, bools, ints); - } - Command createCommand(std::string& label, std::shared_ptr guard, std::vector& updates) { - return Command(label, guard, updates); - } - Program createProgram( - Program::ModelType modelType, - std::map> undefBoolConst, - std::map> undefIntConst, - std::map> undefDoubleConst, - std::vector modules, - std::map rewards, - std::map> labels) { - return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, modules, rewards, labels); - } - -PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type(start), state(new storm::parser::prism::VariableState()) { - - 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::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::bind(&createTransitionReward, qi::_a, qi::_2, qi::_3)]; - transitionRewardDefinition.name("transition reward definition"); - 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"); - - commandName %= this->state->commandNames_; - commandName.name("command name"); - unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_; - unassignedLocalBooleanVariableName.name("unassigned local boolean variable"); - 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("=") > 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::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; - updateDefinition.name("update"); - updateListDefinition = +updateDefinition % "+"; - updateListDefinition.name("update list"); - commandDefinition = ( - qi::lit("[") > -( - (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::bind(&createCommand, qi::_a, qi::_2, qi::_3)]; - commandDefinition.name("command"); - - // This block defines all entities that are needed for parsing variable definitions. - booleanVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > prism::ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) - [ - phoenix::bind(&PrismParser::PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2) - ]; - booleanVariableDefinition.name("boolean variable declaration"); - - integerVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > prism::ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > prism::ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) - [ - phoenix::bind(&PrismParser::PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2) - ]; - integerVariableDefinition.name("integer variable declaration"); - variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4)); - variableDefinition.name("variable declaration"); - - // This block defines all entities that are needed for parsing a module. - 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")) - [qi::_val = phoenix::bind(&PrismParser::PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)]; - - moduleDefinition.name("module"); - moduleRenaming = (qi::lit("module") >> prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") - > this->state->moduleNames_ > qi::lit("[") > *( - (prism::IdentifierGrammar::instance(this->state) > qi::lit("=") > prism::IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] - ) > qi::lit("]") > qi::lit("endmodule")) - [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") >> 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") >> 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") >> 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") > prism::FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(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") > prism::FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(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") > prism::FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(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"); - undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); - undefinedConstantDefinition.name("undefined constant declaration"); - constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); - constantDefinitionList.name("constant declaration list"); - - // This block defines all entities that are needed for parsing a program. - modelTypeDefinition = modelType_; - modelTypeDefinition.name("model type"); - start = ( - modelTypeDefinition > - constantDefinitionList(qi::_a, qi::_b, qi::_c) > - moduleDefinitionList > - rewardDefinitionList(qi::_d) > - labelDefinitionList(qi::_e) - )[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; - start.name("probabilistic program declaration"); - } - - void PrismParser::PrismGrammar::prepareForSecondRun() { - LOG4CPLUS_INFO(logger, "Preparing parser for second run."); - this->state->getIntegerVariable("d1"); - this->state->getIntegerVariable("d2"); - this->state->getIntegerVariable("s1"); - this->state->getIntegerVariable("s2"); - this->state->prepareForSecondRun(); - this->state->getIntegerVariable("d1"); - this->state->getIntegerVariable("d2"); - this->state->getIntegerVariable("s1"); - this->state->getIntegerVariable("s2"); - prism::BooleanExpressionGrammar::secondRun(); - prism::ConstBooleanExpressionGrammar::secondRun(); - prism::ConstDoubleExpressionGrammar::secondRun(); - prism::ConstIntegerExpressionGrammar::secondRun(); - prism::IntegerExpressionGrammar::secondRun(); - } - /*! * Opens the given file for parsing, invokes the helper function to parse the actual content and * closes the file properly, even if an exception is thrown in the parser. In this case, the * exception is passed on to the caller. */ storm::ir::Program PrismParser::parseFile(std::string const& filename) const { + std::cerr << "parseFile( " << filename << " )" << std::endl; // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); storm::ir::Program result; @@ -266,6 +42,7 @@ storm::ir::Program PrismParser::parseFile(std::string const& filename) const { try { result = parse(inputFileStream, filename); } catch(std::exception& e) { + std::cerr << "Exception: " << e.what() << std::endl; // In case of an exception properly close the file before passing exception. inputFileStream.close(); throw e; @@ -299,7 +76,7 @@ storm::ir::Program PrismParser::parse(std::istream& inputStream, std::string con // 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 grammar; + prism::PrismGrammar grammar; try { // Now parse the content using phrase_parse in order to be able to supply a skipping parser. // First run. @@ -311,7 +88,12 @@ storm::ir::Program PrismParser::parse(std::istream& inputStream, std::string con // Second run. qi::phrase_parse(positionIteratorBegin2, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); LOG4CPLUS_INFO(logger, "Finished parsing, here is the parsed program:" << std::endl << result.toString()); + // Reset grammars. + grammar.resetGrammars(); } catch(const qi::expectation_failure& e) { + // Reset grammars in any case. + grammar.resetGrammars(); + // If the parser expected content different than the one provided, display information // about the location of the error. const boost::spirit::classic::file_position_base& pos = e.first.get_position(); diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 32a797adf..48326713f 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -9,15 +9,6 @@ // All classes of the intermediate representation are used. #include "src/ir/IR.h" -#include "src/parser/PrismParser/Includes.h" -#include "src/parser/PrismParser/Tokens.h" -#include "src/parser/PrismParser/IdentifierGrammars.h" -#include "src/parser/PrismParser/VariableState.h" -#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" -#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" -#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" -#include "src/parser/PrismParser/BooleanExpressionGrammar.h" -#include "src/parser/PrismParser/IntegerExpressionGrammar.h" // Used for file input. #include @@ -42,106 +33,6 @@ public: * @return a shared pointer to the intermediate representation of the PRISM file. */ 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::map>, - std::map>, - std::map, - std::map> - >, - Skipper> { - public: - PrismGrammar(); - void prepareForSecondRun(); - - private: - - std::shared_ptr state; - - // The starting point of the grammar. - qi::rule< - Iterator, - Program(), - qi::locals< - std::map>, - std::map>, - std::map>, - std::map, - std::map> - >, - Skipper> start; - qi::rule modelTypeDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; - qi::rule(), Skipper> moduleDefinitionList; - - // Rules for module definition. - qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; - qi::rule>, Skipper> moduleRenaming; - - // Rules for variable definitions. - qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; - qi::rule&, std::map&), qi::locals>, Skipper> booleanVariableDefinition; - qi::rule&, std::map&), qi::locals>, Skipper> integerVariableDefinition; - - // Rules for command definitions. - qi::rule, Skipper> commandDefinition; - qi::rule(), Skipper> updateListDefinition; - qi::rule, std::map>, Skipper> updateDefinition; - qi::rule&, std::map&), Skipper> assignmentDefinitionList; - qi::rule&, std::map&), Skipper> assignmentDefinition; - - // Rules for variable/command names. - qi::rule commandName; - qi::rule unassignedLocalBooleanVariableName; - qi::rule unassignedLocalIntegerVariableName; - - // Rules for reward definitions. - qi::rule&), Skipper> rewardDefinitionList; - qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; - qi::rule stateRewardDefinition; - qi::rule, Skipper> transitionRewardDefinition; - - // Rules for label definitions. - qi::rule>&), Skipper> labelDefinitionList; - qi::rule>&), Skipper> labelDefinition; - - // Rules for constant definitions. - qi::rule(), Skipper> constantDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; - qi::rule(), Skipper> definedConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; - qi::rule(), Skipper> definedBooleanConstantDefinition; - qi::rule(), Skipper> definedIntegerConstantDefinition; - qi::rule(), Skipper> definedDoubleConstantDefinition; - - // Rules for variable recognition. - qi::rule(), Skipper> booleanVariableCreatorExpression; - qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; - - storm::parser::prism::keywordsStruct keywords_; - storm::parser::prism::modelTypeStruct modelType_; - storm::parser::prism::relationalOperatorStruct relations_; - - std::shared_ptr addIntegerConstant(const std::string& name, const std::shared_ptr value); - void addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping); - void addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); - void addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); - Module renameModule(const std::string& name, const std::string& oldname, std::map& mapping); - Module createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands); - - void createIntegerVariable(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids); - void createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids); - }; private: /*! diff --git a/src/parser/PrismParser/BaseGrammar.h b/src/parser/PrismParser/BaseGrammar.h index 4bf4f3265..345a377e0 100644 --- a/src/parser/PrismParser/BaseGrammar.h +++ b/src/parser/PrismParser/BaseGrammar.h @@ -29,11 +29,14 @@ namespace prism { return *BaseGrammar::instanceObject; } + static void resetInstance() { + BaseGrammar::instanceObject = nullptr; + } + static void secondRun() { if (BaseGrammar::instanceObject != nullptr) { BaseGrammar::instanceObject->prepareSecondRun(); } - } std::shared_ptr createBoolLiteral(const bool value) { diff --git a/src/parser/PrismParser/PrismGrammar.cpp b/src/parser/PrismParser/PrismGrammar.cpp new file mode 100644 index 000000000..ac3f3dbf4 --- /dev/null +++ b/src/parser/PrismParser/PrismGrammar.cpp @@ -0,0 +1,258 @@ +/* + * PrismGrammar.cpp + * + * Created on: 11.01.2013 + * Author: chris + */ + +#include "PrismGrammar.h" + +#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" + +// Needed for file IO. +#include +#include +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +// Some typedefs and namespace definitions to reduce code size. +typedef std::string::const_iterator BaseIteratorType; +typedef boost::spirit::classic::position_iterator2 PositionIteratorType; +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + +namespace storm { +namespace parser { +namespace prism { + +void dump(const std::string& s) { + std::cerr << "Dump: " << s << std::endl; +} + +std::shared_ptr PrismGrammar::addIntegerConstant(const std::string& name, const std::shared_ptr value) { + this->state->integerConstants_.add(name, value); + this->state->allConstantNames_.add(name, name); + return value; +} + +void PrismGrammar::addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping) { + this->state->labelNames_.add(name, name); + mapping[name] = value; +} +void PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { + //std::cout << "Adding int assignment for " << variable << std::endl; + this->state->assignedLocalIntegerVariables_.add(variable, variable); + mapping[variable] = Assignment(variable, value); +} +void PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { + //std::cout << "Adding bool assignment for " << variable << std::endl; + this->state->assignedLocalBooleanVariables_.add(variable, variable); + mapping[variable] = Assignment(variable, value); +} +Module PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map& mapping) { + this->state->moduleNames_.add(name, name); + Module* old = this->state->moduleMap_.find(oldname); + if (old == nullptr) { + LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldname << " does not exist!"); + throw "Renaming module failed"; + } + Module res(*old, name, mapping, this->state); + this->state->moduleMap_.at(name) = res; + return res; +} +Module PrismGrammar::createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands) { + this->state->moduleNames_.add(name, name); + Module res(name, bools, ints, boolids, intids, commands); + this->state->moduleMap_.at(name) = res; + return res; +} + +void PrismGrammar::createIntegerVariable(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids) { + //std::cout << "Creating int " << name << " = " << init << std::endl; + uint_fast64_t id = this->state->addIntegerVariable(name, lower, upper, init); + vars.emplace_back(id, name, lower, upper, init); + varids[name] = id; + this->state->localIntegerVariables_.add(name, name); +} +void PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids) { + //std::cout << "Creating bool " << name << std::endl; + uint_fast64_t id = this->state->addBooleanVariable(name, init); + vars.emplace_back(id, name, init); + varids[name] = id; + this->state->localBooleanVariables_.add(name, name); +} + +StateReward createStateReward(std::shared_ptr guard, std::shared_ptr reward) { + return StateReward(guard, reward); +} +TransitionReward createTransitionReward(std::string label, std::shared_ptr guard, std::shared_ptr reward) { + return TransitionReward(label, guard, reward); +} +void createRewardModel(std::string name, std::vector& stateRewards, std::vector& transitionRewards, std::map& mapping) { + mapping[name] = RewardModel(name, stateRewards, transitionRewards); +} +Update createUpdate(std::shared_ptr likelihood, std::map& bools, std::map ints) { + return Update(likelihood, bools, ints); +} +Command createCommand(std::string& label, std::shared_ptr guard, std::vector& updates) { + return Command(label, guard, updates); +} +Program createProgram( + Program::ModelType modelType, + std::map> undefBoolConst, + std::map> undefIntConst, + std::map> undefDoubleConst, + std::vector modules, + std::map rewards, + std::map> labels) { + return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, modules, rewards, labels); +} + +PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) { + + labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";")) + [phoenix::bind(&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 = (BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > 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("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > 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("\"") > 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"); + + commandName %= this->state->commandNames_; + commandName.name("command name"); + unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_; + unassignedLocalBooleanVariableName.name("unassigned local boolean variable"); + 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("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntAssignment, this, qi::_1, qi::_2, qi::_r2)] | + (qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBoolAssignment, this, qi::_1, qi::_2, qi::_r1)]; + assignmentDefinition.name("assignment"); + assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; + assignmentDefinitionList.name("assignment list"); + updateDefinition = ( + 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("[") > -( + (FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1] + ) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";") + )[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 = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + [ + phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2) + ]; + booleanVariableDefinition.name("boolean variable declaration"); + + integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + [ + phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2) + ]; + integerVariableDefinition.name("integer variable declaration"); + variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4)); + variableDefinition.name("variable declaration"); + + // This block defines all entities that are needed for parsing a module. + moduleDefinition = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::startModule, *this->state)] + >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule")) + [qi::_val = phoenix::bind(&PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)]; + + moduleDefinition.name("module"); + moduleRenaming = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") + > this->state->moduleNames_ > qi::lit("[") > *( + (IdentifierGrammar::instance(this->state) > qi::lit("=") > IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] + ) > qi::lit("]") > qi::lit("endmodule")) + [qi::_val = phoenix::bind(&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") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > 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") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> + ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";") + )[ qi::_val = phoenix::bind(&PrismGrammar::addIntegerConstant, this, qi::_1, qi::_2) ]; + definedIntegerConstantDefinition.name("defined integer constant declaration"); + definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > 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") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(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") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(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") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(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"); + undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); + undefinedConstantDefinition.name("undefined constant declaration"); + constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); + constantDefinitionList.name("constant declaration list"); + + // This block defines all entities that are needed for parsing a program. + modelTypeDefinition = modelType_; + modelTypeDefinition.name("model type"); + start = ( + modelTypeDefinition > + constantDefinitionList(qi::_a, qi::_b, qi::_c) > + moduleDefinitionList > + rewardDefinitionList(qi::_d) > + labelDefinitionList(qi::_e) + )[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; + start.name("probabilistic program declaration"); +} + +void PrismGrammar::prepareForSecondRun() { + LOG4CPLUS_INFO(logger, "Preparing parser for second run."); + this->state->prepareForSecondRun(); + BooleanExpressionGrammar::secondRun(); + ConstBooleanExpressionGrammar::secondRun(); + ConstDoubleExpressionGrammar::secondRun(); + ConstIntegerExpressionGrammar::secondRun(); + IntegerExpressionGrammar::secondRun(); +} + +void PrismGrammar::resetGrammars() { + LOG4CPLUS_INFO(logger, "Resetting grammars."); + BooleanExpressionGrammar::resetInstance(); + ConstBooleanExpressionGrammar::resetInstance(); + ConstDoubleExpressionGrammar::resetInstance(); + ConstIntegerExpressionGrammar::resetInstance(); + IntegerExpressionGrammar::resetInstance(); +} + +} // namespace prism +} // namespace parser +} // namespace storm diff --git a/src/parser/PrismParser/PrismGrammar.h b/src/parser/PrismParser/PrismGrammar.h new file mode 100644 index 000000000..97033f506 --- /dev/null +++ b/src/parser/PrismParser/PrismGrammar.h @@ -0,0 +1,142 @@ +/* + * File: PrismGrammar.h + * Author: nafur + * + * Created on April 30, 2013, 5:20 PM + */ + +#ifndef PRISMGRAMMAR_H +#define PRISMGRAMMAR_H + +// All classes of the intermediate representation are used. +#include "src/ir/IR.h" +#include "src/parser/PrismParser/Includes.h" +#include "src/parser/PrismParser/Tokens.h" +#include "src/parser/PrismParser/IdentifierGrammars.h" +#include "src/parser/PrismParser/VariableState.h" +#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" +#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" +#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" +#include "src/parser/PrismParser/BooleanExpressionGrammar.h" +#include "src/parser/PrismParser/IntegerExpressionGrammar.h" + +// Used for file input. +#include +#include + +namespace storm { +namespace parser { +namespace prism { + +using namespace storm::ir; +using namespace storm::ir::expressions; + +/*! + * 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::map>, + std::map>, + std::map, + std::map> + >, + Skipper> { +public: + PrismGrammar(); + void prepareForSecondRun(); + void resetGrammars(); + +private: + + std::shared_ptr state; + + // The starting point of the grammar. + qi::rule< + Iterator, + Program(), + qi::locals< + std::map>, + std::map>, + std::map>, + std::map, + std::map> + >, + Skipper> start; + qi::rule modelTypeDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; + qi::rule(), Skipper> moduleDefinitionList; + + // Rules for module definition. + qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; + qi::rule>, Skipper> moduleRenaming; + + // Rules for variable definitions. + qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; + qi::rule&, std::map&), qi::locals>, Skipper> booleanVariableDefinition; + qi::rule&, std::map&), qi::locals>, Skipper> integerVariableDefinition; + + // Rules for command definitions. + qi::rule, Skipper> commandDefinition; + qi::rule(), Skipper> updateListDefinition; + qi::rule, std::map>, Skipper> updateDefinition; + qi::rule&, std::map&), Skipper> assignmentDefinitionList; + qi::rule&, std::map&), Skipper> assignmentDefinition; + + // Rules for variable/command names. + qi::rule commandName; + qi::rule unassignedLocalBooleanVariableName; + qi::rule unassignedLocalIntegerVariableName; + + // Rules for reward definitions. + qi::rule&), Skipper> rewardDefinitionList; + qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; + qi::rule stateRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; + + // Rules for label definitions. + qi::rule>&), Skipper> labelDefinitionList; + qi::rule>&), Skipper> labelDefinition; + + // Rules for constant definitions. + qi::rule(), Skipper> constantDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; + qi::rule(), Skipper> definedConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; + qi::rule(), Skipper> definedBooleanConstantDefinition; + qi::rule(), Skipper> definedIntegerConstantDefinition; + qi::rule(), Skipper> definedDoubleConstantDefinition; + + // Rules for variable recognition. + qi::rule(), Skipper> booleanVariableCreatorExpression; + qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; + + storm::parser::prism::keywordsStruct keywords_; + storm::parser::prism::modelTypeStruct modelType_; + storm::parser::prism::relationalOperatorStruct relations_; + + std::shared_ptr addIntegerConstant(const std::string& name, const std::shared_ptr value); + void addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping); + void addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); + void addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); + Module renameModule(const std::string& name, const std::string& oldname, std::map& mapping); + Module createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands); + + void createIntegerVariable(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids); + void createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids); +}; + + +} // namespace prism +} // namespace parser +} // namespace storm + + +#endif /* PRISMGRAMMAR_H */ + diff --git a/test/parser/ParsePrismTest.cpp b/test/parser/ParsePrismTest.cpp index 4f59be220..b4155edfd 100644 --- a/test/parser/ParsePrismTest.cpp +++ b/test/parser/ParsePrismTest.cpp @@ -4,8 +4,9 @@ #include "src/utility/IoUtility.h" #include "src/ir/Program.h" #include "src/adapters/ExplicitModelAdapter.h" +#include "src/models/Mdp.h" -TEST(ParsePrismTest, parseAndOutput) { +TEST(ParsePrismTest, parseCrowds5_5) { storm::parser::PrismParser parser; storm::ir::Program program; ASSERT_NO_THROW(program = parser.parseFile("examples/dtmc/crowds/crowds5_5.pm")); @@ -17,4 +18,15 @@ TEST(ParsePrismTest, parseAndOutput) { ASSERT_EQ(model->getNumberOfTransitions(), (uint_fast64_t)15113); } +TEST(ParsePrismTest, parseTwoDice) { + storm::parser::PrismParser parser; + storm::ir::Program program; + ASSERT_NO_THROW(program = parser.parseFile("examples/mdp/two_dice/two_dice.nm")); + storm::adapters::ExplicitModelAdapter adapter(program); + std::shared_ptr> model = adapter.getModel()->as>(); + + ASSERT_EQ(model->getNumberOfStates(), (uint_fast64_t)169); + ASSERT_EQ(model->getNumberOfChoices(), (uint_fast64_t)254); + ASSERT_EQ(model->getNumberOfTransitions(), (uint_fast64_t)436); +}