diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 587c91dc8..98f58f208 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -1,13 +1,4 @@ -/* - * PrismParser.cpp - * - * Created on: 11.01.2013 - * Author: chris - */ - -#include "PrismParser.h" - -#include "src/utility/OsDetection.h" +#include "src/parser/PrismParser.h" #include "src/parser/prismparser/PrismGrammar.h" @@ -21,108 +12,87 @@ #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - +#include "log4cplus/consoleappender.h" +#include "log4cplus/fileappender.h" +log4cplus::Logger logger; namespace storm { -namespace parser { - -/*! - * 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 PrismParserFromFile(std::string const& filename) { - // Open file and initialize result. - std::ifstream inputFileStream(filename, std::ios::in); - storm::ir::Program result; - - // Now try to parse the contents of the file. - try { - result = PrismParser(inputFileStream, filename); - } catch(std::exception& e) { - // In case of an exception properly close the file before passing exception. - inputFileStream.close(); - throw e; - } - - // Close the stream in case everything went smoothly and return result. - inputFileStream.close(); - return result; -} - -/*! - * Passes iterators to the input stream to the Boost spirit parser and thereby parses the input. - * If the parser throws an expectation failure exception, i.e. expected input different than the one - * provided, this is caught and displayed properly before the exception is passed on. - */ -storm::ir::Program PrismParser(std::istream& inputStream, std::string const& filename) { - // Prepare iterators to input. - // TODO: Right now, this parses the whole contents of the file into a string first. - // While this is usually not necessary, because there exist adapters that make an input stream - // iterable in both directions without storing it into a string, using the corresponding - // Boost classes gives an awful output under valgrind and is thus disabled for the time being. - std::string fileContent((std::istreambuf_iterator(inputStream)), (std::istreambuf_iterator())); - BaseIteratorType stringIteratorBegin = fileContent.begin(); - BaseIteratorType stringIteratorEnd = fileContent.end(); - PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename); - PositionIteratorType positionIteratorBegin2(stringIteratorBegin, stringIteratorEnd, filename); - PositionIteratorType positionIteratorEnd; - - // Prepare resulting intermediate representation of input. - storm::ir::Program result; - - // 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. - prism::PrismGrammar grammar; - try { - // Now parse the content using phrase_parse in order to be able to supply a skipping parser. - // First run. - LOG4CPLUS_INFO(logger, "Start parsing..."); - qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); - grammar.prepareForSecondRun(); - result = storm::ir::Program(); - LOG4CPLUS_INFO(logger, "Start second parsing run..."); - // 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) { - // If the parser expected content different than the one provided, display information - // about the location of the error. - const boost::spirit::classic::file_position_base& pos = e.first.get_position(); - - // Construct the error message including a caret display of the position in the - // erroneous line. - std::stringstream msg; - std::string line = e.first.get_currentline(); - while (line.find('\t') != std::string::npos) line.replace(line.find('\t'),1," "); - msg << pos.file << ", line " << pos.line << ", column " << pos.column + namespace parser { + storm::prism::Program PrismParserFromFile(std::string const& filename) { + // Open file and initialize result. + std::ifstream inputFileStream(filename, std::ios::in); + storm::prism::Program result; + + // Now try to parse the contents of the file. + try { + result = PrismParser(inputFileStream, filename); + } catch(std::exception& e) { + // In case of an exception properly close the file before passing exception. + inputFileStream.close(); + throw e; + } + + // Close the stream in case everything went smoothly and return result. + inputFileStream.close(); + return result; + } + + storm::prism::Program PrismParser(std::istream& inputStream, std::string const& filename) { + // Prepare iterators to input. + // TODO: Right now, this parses the whole contents of the file into a string first. + // While this is usually not necessary, because there exist adapters that make an input stream + // iterable in both directions without storing it into a string, using the corresponding + // Boost classes gives an awful output under valgrind and is thus disabled for the time being. + std::string fileContent((std::istreambuf_iterator(inputStream)), (std::istreambuf_iterator())); + BaseIteratorType stringIteratorBegin = fileContent.begin(); + BaseIteratorType stringIteratorEnd = fileContent.end(); + PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename); + PositionIteratorType positionIteratorBegin2(stringIteratorBegin, stringIteratorEnd, filename); + PositionIteratorType positionIteratorEnd; + + // Prepare resulting intermediate representation of input. + storm::prism::Program result; + + // 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. + storm::parser::prism::PrismGrammar grammar; + try { + // Now parse the content using phrase_parse in order to be able to supply a skipping parser. + // First run. + LOG4CPLUS_INFO(logger, "Start parsing..."); + qi::phrase_parse(positionIteratorBegin, 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); + + } catch(const qi::expectation_failure& e) { + // If the parser expected content different than the one provided, display information + // about the location of the error. + const boost::spirit::classic::file_position_base& pos = e.first.get_position(); + + // Construct the error message including a caret display of the position in the + // erroneous line. + std::stringstream msg; + std::string line = e.first.get_currentline(); + while (line.find('\t') != std::string::npos) line.replace(line.find('\t'),1," "); + msg << pos.file << ", line " << pos.line << ", column " << pos.column << ": parse error: expected " << e.what_ << std::endl << "\t" << line << std::endl << "\t"; - int i = 0; - for (i = 1; i < pos.column; ++i) { - msg << "-"; - } - msg << "^"; - for (; i < 80; ++i) { - msg << "-"; - } - msg << std::endl; - - std::cerr << msg.str(); - - // Reset grammars in any case. - grammar.resetGrammars(); - - // Now propagate exception. - throw storm::exceptions::WrongFormatException() << msg.str(); - } - - return result; -} - -} // namespace parser - + int i = 0; + for (i = 1; i < pos.column; ++i) { + msg << "-"; + } + msg << "^"; + for (; i < 80; ++i) { + msg << "-"; + } + msg << std::endl; + + std::cerr << msg.str(); + + // Now propagate exception. + throw storm::exceptions::WrongFormatException() << msg.str(); + } + + return result; + } + } // namespace parser } // namespace storm diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index d52f2b9ae..72b7a40b8 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -46,146 +46,108 @@ namespace storm { atomicNumericalExpression %= minMaxExpression | floorCeilExpression | numericalVariableExpression | qi::lit("(") >> numericalExpression >> qi::lit(")"); atomicNumericalExpression.name("numerical expression"); - minMaxExpression %= ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(",") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::minimum, qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::maximum, qi::_1, qi::_2)]]; + minMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(",") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::minimum, qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::maximum, qi::_1, qi::_2)]]; minMaxExpression.name("min/max expression"); - floorCeilExpression %= ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::floor, qi::_1)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::ceil, qi::_1)]]; + floorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> numericalExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&storm::expressions::Expression::floor, qi::_1)] .else_ [qi::_val = phoenix::bind(&storm::expressions::Expression::ceil, qi::_1)]]; floorCeilExpression.name("integer floor/ceil expression"); numericalVariableExpression = identifier[qi::_val = phoenix::bind(&storm::expressions::Expression::createDoubleVariable, qi::_1)]; numericalVariableExpression.name("numerical variable"); - // Parse a model type. modelTypeDefinition = modelType_; modelTypeDefinition.name("model type"); + + undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r1) | undefinedDoubleConstantDefinition(qi::_r1)); + undefinedConstantDefinition.name("undefined constant definition"); - programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1] - > *( undefinedConstantDefinition(qi::_r1) - | definedConstantDefinition(qi::_r1) - | formulaDefinition(qi::_r1) - | globalVariableDefinition(qi::_r1) - ); - programHeader.name("program header"); + undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, phoenix::bind(&GlobalProgramInformation::undefinedBooleanConstants, qi::_r1), qi::_1)]; + undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - // This block defines all entities that are needed for parsing global variable definitions. - globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true))); - globalVariableDefinitionList.name("global variable declaration list"); + undefinedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int")) > identifier > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, phoenix::bind(&GlobalProgramInformation::undefinedIntegerConstants, qi::_r1), qi::_1)]; + undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); - // This block defines all entities that are needed for parsing constant definitions. - definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > 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]; + undefinedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double")) > identifier > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, phoenix::bind(&GlobalProgramInformation::undefinedDoubleConstants, qi::_r1), qi::_1)]; + undefinedDoubleConstantDefinition.name("undefined double constant definition"); + + definedConstantDefinition %= (definedBooleanConstantDefinition(qi::_r1) | definedIntegerConstantDefinition(qi::_r1) | definedDoubleConstantDefinition(qi::_r1)); + definedConstantDefinition.name("defined constant definition"); + + definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addDefinedBooleanConstant, phoenix::bind(&GlobalProgramInformation::definedBooleanConstants, qi::_r1), qi::_1, 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(";"))[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 = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expression >> qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addDefinedIntegerConstant, phoenix::bind(&GlobalProgramInformation::definedIntegerConstants, qi::_r1), 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 = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addDefinedDoubleConstant, phoenix::bind(&GlobalProgramInformation::definedDoubleConstants, qi::_r1), qi::_1, qi::_2)]; definedDoubleConstantDefinition.name("defined double constant declaration"); - undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, this, qi::_1, qi::_r1)]; - undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, this, qi::_1, qi::_r1)]; - undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); - undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, this, qi::_1, qi::_r1)]; - undefinedDoubleConstantDefinition.name("undefined double constant definition"); - definedConstantDefinition %= (definedBooleanConstantDefinition(qi::_r1) | definedIntegerConstantDefinition(qi::_r2) | definedDoubleConstantDefinition(qi::_r3)); - definedConstantDefinition.name("defined constant definition"); - undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); - undefinedConstantDefinition.name("undefined constant definition"); - // Parse the ingredients of a probabilistic program. - start = (qi::eps > - programHeader(qi::_a) > - formulaDefinitionList > - globalVariableDefinitionList(qi::_d) > - moduleDefinitionList > - rewardDefinitionList(qi::_e) > - labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)]; - start.name("probabilistic program declaration"); - + formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression > qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addFormula, phoenix::bind(&GlobalProgramInformation::formulas, qi::_r1), qi::_1, qi::_2)]; + formulaDefinition.name("formula definition"); - 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"); + globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1)) | integerVariableDefinition(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1)))); + globalVariableDefinition.name("global variable 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)]; + programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1] + > *( undefinedConstantDefinition(qi::_r1) + | definedConstantDefinition(qi::_r1) + | formulaDefinition(qi::_r1) + | globalVariableDefinition(qi::_r1) + ); + programHeader.name("program header"); + + rewardModelDefinition = (qi::lit("rewards") > qi::lit("\"") > identifier > qi::lit("\"") + > +( stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] + | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)] + ) + >> qi::lit("endrewards"))[phoenix::bind(&PrismGrammar::addRewardModel, phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_r1), qi::_1, qi::_a, qi::_b)]; + rewardModelDefinition.name("reward model definition"); + + stateRewardDefinition = (booleanExpression > qi::lit(":") > numericalExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::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 = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit(":") > numericalExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::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->globalBooleanVariables_) - this->state->assignedBooleanVariables_; - unassignedLocalBooleanVariableName.name("unassigned local/global boolean variable"); - unassignedLocalIntegerVariableName %= (this->state->localIntegerVariables_ | this->state->globalIntegerVariables_) - this->state->assignedIntegerVariables_; - unassignedLocalIntegerVariableName.name("unassigned local/global 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::addIntegerAssignment, this, qi::_1, qi::_2, qi::_r2)] | - (qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBooleanAssignment, this, qi::_1, qi::_2, qi::_r1)]; + + labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > booleanExpression >> qi::lit(";"))[qi::_pass = phoenix::bind(&PrismGrammar::addLabel, phoenix::bind(&GlobalProgramInformation::labels, qi::_r1), qi::_1, qi::_2)]; + labelDefinition.name("label definition"); + + assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression > qi::lit(")"))[qi::_pass = phoenix::bind(&PrismGrammar::addAssignment, qi::_r1, qi::_1, qi::_2)]; assignmentDefinition.name("assignment"); - assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; + assignmentDefinitionList = assignmentDefinition(qi::_r1) % "&"; assignmentDefinitionList.name("assignment list"); - updateDefinition = (((ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(":")) - | qi::attr(std::shared_ptr(new storm::ir::expressions::DoubleLiteralExpression(1))))[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] - >> assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)]; + + moduleDefinitionList %= +(moduleDefinition(qi::_r1) | moduleRenaming(qi::_r1)); + moduleDefinitionList.name("module list"); + + updateDefinition = (((numericalExpression >> qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList(qi::_a))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, qi::_1, qi::_a)]; updateDefinition.name("update"); - updateListDefinition = +updateDefinition % "+"; + + 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(&PrismGrammar::createCommand, this, 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, qi::_r3)]; - 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, qi::_r3)]; - integerVariableDefinition.name("integer variable declaration"); - variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3, false) | integerVariableDefinition(qi::_r2, qi::_r4, false)); - 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::clearLocalVariables, *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"); + commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createCommand, qi::_a, qi::_2, qi::_3)]; + commandDefinition.name("command definition"); + + booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > booleanExpression) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addBooleanVariable, qi::_r1, qi::_1, qi::_2)]; + booleanVariableDefinition.name("boolean variable definition"); + integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")) > numericalExpression[qi::_a = qi::_1] > qi::lit("..") > numericalExpression > qi::lit("]") > -(qi::lit("init") > numericalExpression[qi::_a = qi::_1]) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addIntegerVariable, qi::_r1, qi::_1, qi::_2, qi::_3, qi::_a)]; + integerVariableDefinition.name("integer variable definition"); - constantBooleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstBooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantBooleanFormulas_.add, qi::_1, qi::_2)]; - constantBooleanFormulaDefinition.name("constant boolean formula definition"); - booleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->booleanFormulas_.add, qi::_1, qi::_2)]; - booleanFormulaDefinition.name("boolean formula definition"); - constantIntegerFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantIntegerFormulas_.add, qi::_1, qi::_2)]; - constantIntegerFormulaDefinition.name("constant integer formula definition"); - integerFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> IntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerFormulas_.add, qi::_1, qi::_2)]; - integerFormulaDefinition.name("integer formula definition"); - constantDoubleFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantDoubleFormulas_.add, qi::_1, qi::_2)]; - constantDoubleFormulaDefinition.name("constant double formula definition"); - formulaDefinition = constantBooleanFormulaDefinition | booleanFormulaDefinition | constantIntegerFormulaDefinition | integerFormulaDefinition | constantDoubleFormulaDefinition; - formulaDefinition.name("formula definition"); - formulaDefinitionList = *formulaDefinition; - formulaDefinitionList.name("formula definition list"); + variableDefinition = (booleanVariableDefinition(qi::_r1) | integerVariableDefinition(qi::_r2)); + variableDefinition.name("variable declaration"); + + moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createModule, qi::_1, qi::_a, qi::_b, qi::_2)]; + moduleDefinition.name("module definition"); + + moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[") + > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] % ",") > qi::lit("]") + > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createRenamedModule, qi::_1, qi::_2, qi::_a, qi::_r1)]; + moduleRenaming.name("module definition via renaming"); + + start = (qi::eps > programHeader(qi::_a) > moduleDefinitionList(qi::_a) > *(rewardModelDefinition(qi::_a) | labelDefinition(qi::_a)))[qi::_val = phoenix::bind(&PrismGrammar::createProgram, qi::_a, qi::_1)]; + start.name("probabilistic program"); } } // namespace prism } // namespace parser diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index 785c85e9f..d51ee4f04 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -16,7 +16,6 @@ namespace qi = boost::spirit::qi; namespace phoenix = boost::phoenix; -namespace prism = storm::prism; typedef std::string::const_iterator BaseIteratorType; typedef boost::spirit::classic::position_iterator2 PositionIteratorType; @@ -25,22 +24,51 @@ typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2; typedef boost::spirit::unused_type Unused; -#include "src/parser/prismparser/Tokens.h" - #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" -using namespace storm::expressions; namespace storm { namespace parser { namespace prism { + + struct modelTypeStruct : qi::symbols { + modelTypeStruct() { + add + ("dtmc", storm::prism::Program::ModelType::DTMC) + ("ctmc", storm::prism::Program::ModelType::CTMC) + ("mdp", storm::prism::Program::ModelType::MDP) + ("ctmdp", storm::prism::Program::ModelType::CTMDP) + ("ma", storm::prism::Program::ModelType::MA); + } + }; + + struct keywordsStruct : qi::symbols { + keywordsStruct() { + add + ("dtmc", 1) + ("ctmc", 2) + ("mdp", 3) + ("ctmdp", 4) + ("ma", 5) + ("const", 6) + ("int", 7) + ("bool", 8) + ("module", 9) + ("endmodule", 10) + ("rewards", 11) + ("endrewards", 12) + ("true", 13) + ("false", 14); + } + }; + class GlobalProgramInformation { public: // Default construct the header information. GlobalProgramInformation() = default; // Members for all essential information that needs to be collected. - prism::Program::ModelType modelType; + storm::prism::Program::ModelType modelType; std::set undefinedBooleanConstants; std::set undefinedIntegerConstants; std::set undefinedDoubleConstants; @@ -48,13 +76,18 @@ namespace storm { std::map definedIntegerConstants; std::map definedDoubleConstants; std::map formulas; - std::map globalBooleanVariables; - std::map globalIntegerVariables; - std::map modules; - std::map rewardModels; + std::map globalBooleanVariables; + std::map globalIntegerVariables; + std::map modules; + std::map rewardModels; + std::map labels; + + // Counters to provide unique indexing for commands and updates. + uint_fast64_t currentCommandIndex; + uint_fast64_t currentUpdateIndex; }; - class PrismGrammar : public qi::grammar, Skipper> { + class PrismGrammar : public qi::grammar, Skipper> { public: /*! * Default constructor that creates an empty and functional grammar. @@ -63,46 +96,48 @@ namespace storm { private: // The starting point of the grammar. - qi::rule, Skipper> start; + qi::rule, Skipper> start; // Rules for model type. - qi::rule modelTypeDefinition; + qi::rule modelTypeDefinition; // Rules for parsing the program header. qi::rule programHeader; qi::rule undefinedConstantDefinition; - qi::rule definedConstantDefinition; qi::rule undefinedBooleanConstantDefinition; qi::rule undefinedIntegerConstantDefinition; qi::rule undefinedDoubleConstantDefinition; + qi::rule definedConstantDefinition; qi::rule definedBooleanConstantDefinition; qi::rule definedIntegerConstantDefinition; qi::rule definedDoubleConstantDefinition; // Rules for global variable definitions. - qi::rule globalVariableDefinition; + qi::rule globalVariableDefinition; + qi::rule globalBooleanVariableDefinition; + qi::rule globalIntegerVariableDefinition; // Rules for modules definition. - qi::rule(), Skipper> moduleDefinitionList; - qi::rule, std::map>, Skipper> moduleDefinition; - qi::rule, Skipper> moduleRenaming; + qi::rule(GlobalProgramInformation&), Skipper> moduleDefinitionList; + qi::rule, std::map>, Skipper> moduleDefinition; + qi::rule>, Skipper> moduleRenaming; // Rules for variable definitions. - qi::rule&, std::map&), Skipper> variableDefinition; - qi::rule&), Skipper> booleanVariableDefinition; - qi::rule&), Skipper> integerVariableDefinition; + qi::rule&, std::map&), Skipper> variableDefinition; + qi::rule&), Skipper> booleanVariableDefinition; + qi::rule&), qi::locals, Skipper> integerVariableDefinition; // Rules for command definitions. - qi::rule, Skipper> commandDefinition; - qi::rule(), Skipper> updateListDefinition; - qi::rule>, Skipper> updateDefinition; - qi::rule&), Skipper> assignmentDefinitionList; - qi::rule assignmentDefinition; + qi::rule, Skipper> commandDefinition; + qi::rule(), Skipper> updateListDefinition; + qi::rule>, Skipper> updateDefinition; + qi::rule&), Skipper> assignmentDefinitionList; + qi::rule&), Skipper> assignmentDefinition; // Rules for reward definitions. - qi::rule, std::vector>, Skipper> rewardModelDefinition; - qi::rule stateRewardDefinition; - qi::rule transitionRewardDefinition; + qi::rule, std::vector>, Skipper> rewardModelDefinition; + qi::rule stateRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; // Rules for label definitions. qi::rule labelDefinition; @@ -130,17 +165,35 @@ namespace storm { qi::rule, Skipper> minMaxExpression; qi::rule, Skipper> floorCeilExpression; - // Parsers that recognize special keywords and operations. + // Parsers that recognize special keywords and model types. storm::parser::prism::keywordsStruct keywords_; storm::parser::prism::modelTypeStruct modelType_; - storm::parser::prism::BinaryRelationOperatorStruct relationOperator_; - storm::parser::prism::BinaryBooleanOperatorStruct binaryBooleanOperator_; - storm::parser::prism::UnaryBooleanOperatorStruct unaryBooleanOperator_; - storm::parser::prism::BinaryNumericalOperatorStruct binaryNumericalOperator_; - storm::parser::prism::UnaryNumericalOperatorStruct unaryNumericalOperator_; // Helper methods that add data to data structures. + static bool addUndefinedBooleanConstant(std::set& undefinedBooleanConstants, std::string const& newUndefinedBooleanConstant); + static bool addUndefinedIntegerConstant(std::set& undefinedIntegerConstants, std::string const& newUndefinedIntegerConstant); + static bool addUndefinedDoubleConstant(std::set& undefinedDoubleConstants, std::string const& newUndefinedDoubleConstant); + static bool addDefinedBooleanConstant(std::map& definedBooleanConstants, std::string const& newDefinedBooleanConstant, storm::expressions::Expression expression); + static bool addDefinedIntegerConstant(std::map& definedIntegerConstants, std::string const& newDefinedIntegerConstant, storm::expressions::Expression expression); + static bool addDefinedDoubleConstant(std::map& definedDoubleConstants, std::string const& newDefinedDoubleConstant, storm::expressions::Expression expression); + + static bool addFormula(std::map& formulas, std::string const& formulaName, storm::expressions::Expression expression); + + static storm::prism::RewardModel addRewardModel(std::map& rewardModels, std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards); + static storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression); + static storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression); + + static bool addLabel(std::map& labels, std::string const& labelName, storm::expressions::Expression expression); + + static bool addAssignment(std::map& assignments, std::string const& variableName, storm::expressions::Expression assignedExpression); + static storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::map& assignments); + static storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector const& updates); + static bool addBooleanVariable(std::map& booleanVariables, std::string const& variableName, storm::expressions::Expression initialValueExpression); + static bool addIntegerVariable(std::map& integerVariables, std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression); + static storm::prism::Module createModule(std::string const& moduleName, std::map const& booleanVariables, std::map const& integerVariables, std::vector const& commands); + static storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation const& globalProgramInformation); + static storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation, std::vector const& modules); }; } // namespace prism } // namespace parser diff --git a/src/parser/prismparser/Tokens.h b/src/parser/prismparser/Tokens.h deleted file mode 100644 index 866bbbf24..000000000 --- a/src/parser/prismparser/Tokens.h +++ /dev/null @@ -1,113 +0,0 @@ -#ifndef STORM_PARSER_PRISMPARSER_TOKENS_H_ -#define STORM_PARSER_PRISMPARSER_TOKENS_H_ - -#include "src/storage/prism/Program.h" -#include "src/storage/expressions/Expressions.h" - -namespace storm { - namespace parser { - namespace prism { - /*! - * A structure mapping the textual representation of a model type to the model type - * representation of the intermediate representation. - */ - struct modelTypeStruct : qi::symbols { - modelTypeStruct() { - add - ("dtmc", storm::prism::Program::ModelType::DTMC) - ("ctmc", storm::prism::Program::ModelType::CTMC) - ("mdp", storm::prism::Program::ModelType::MDP) - ("ctmdp", storm::prism::Program::ModelType::CTMDP) - ("ma", storm::prism::Program::ModelType::MA); - } - }; - - /*! - * A structure defining the keywords that are not allowed to be chosen as identifiers. - */ - struct keywordsStruct : qi::symbols { - keywordsStruct() { - add - ("dtmc", 1) - ("ctmc", 2) - ("mdp", 3) - ("ctmdp", 4) - ("ma", 5) - ("const", 6) - ("int", 7) - ("bool", 8) - ("module", 9) - ("endmodule", 10) - ("rewards", 11) - ("endrewards", 12) - ("true", 13) - ("false", 14); - } - }; - - /*! - * A structure mapping the textual representation of binary relations to the corresponding enum values. - */ - struct BinaryRelationOperatorStruct : qi::symbols { - BinaryRelationOperatorStruct() { - add - ("=", storm::expressions::BinaryRelationExpression::RelationType::Equal) - ("!=", storm::expressions::BinaryRelationExpression::RelationType::NotEqual) - ("<", storm::expressions::BinaryRelationExpression::RelationType::Less) - ("<=", storm::expressions::BinaryRelationExpression::RelationType::LessOrEqual) - (">", storm::expressions::BinaryRelationExpression::RelationType::Greater) - (">=", storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual); - } - }; - - /*! - * A structure mapping the textual representation of binary operators to the corresponding enum values. - */ - struct BinaryBooleanOperatorStruct : qi::symbols { - BinaryBooleanOperatorStruct() { - add - ("&", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And) - ("|", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or) - ("=>", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies) - ("<=>", storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff); - } - }; - - /*! - * A structure mapping the textual representation of binary operators to the corresponding enum values. - */ - struct UnaryBooleanOperatorStruct : qi::symbols { - UnaryBooleanOperatorStruct() { - add - ("!", storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not); - } - }; - - /*! - * A structure mapping the textual representation of binary boolean operators to the corresponding enum values. - */ - struct BinaryNumericalOperatorStruct : qi::symbols { - BinaryNumericalOperatorStruct() { - add - ("+", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus) - ("-", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Minus) - ("*", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times) - ("/", storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide); - } - }; - - /*! - * A structure mapping the textual representation of binary operators to the corresponding enum values. - */ - struct UnaryNumericalOperatorStruct : qi::symbols { - UnaryNumericalOperatorStruct() { - add - ("!", storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus); - } - }; - } - } -} - -#endif /* STORM_PARSER_PRISMPARSER_TOKENS_H_ */ - diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp new file mode 100644 index 000000000..9791d9890 --- /dev/null +++ b/src/storage/prism/Constant.cpp @@ -0,0 +1,43 @@ +#include "src/storage/prism/Constant.h" + +namespace storm { + namespace prism { + Constant::Constant(ConstantType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(true), expression(expression) { + // Intentionally left empty. + } + + Constant::Constant(ConstantType constantType, std::string const& constantName, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(false), expression() { + // Intentionally left empty. + } + + std::string const& Constant::getConstantName() const { + return this->constantName; + } + + Constant::ConstantType Constant::getConstantType() const { + return this->constantType; + } + + bool Constant::isDefined() const { + return this->defined; + } + + storm::expressions::Expression const& Constant::getExpression() const { + return this->expression; + } + + std::ostream& operator<<(std::ostream& stream, Constant const& constant) { + stream << "const "; + switch (constant.getConstantType()) { + case Constant::ConstantType::Bool: stream << "bool "; break; + case Constant::ConstantType::Integer: stream << "int "; break; + case Constant::ConstantType::Double: stream << "double "; break; + } + stream << constant.getConstantName(); + if (constant.isDefined()) { + stream << " = " << constant.getExpression() << ";"; + } + return stream; + } + } +} \ No newline at end of file diff --git a/src/storage/prism/Constant.h b/src/storage/prism/Constant.h new file mode 100644 index 000000000..ad1736ffd --- /dev/null +++ b/src/storage/prism/Constant.h @@ -0,0 +1,91 @@ +#ifndef STORM_STORAGE_PRISM_CONSTANT_H_ +#define STORM_STORAGE_PRISM_CONSTANT_H_ + +#include "src/storage/prism/LocatedInformation.h" +#include "src/storage/expressions/Expression.h" + +namespace storm { + namespace prism { + class Constant : public LocatedInformation { + public: + /*! + * The possible constant types. + */ + enum class ConstantType {Bool, Integer, Double}; + + /*! + * Creates a constant with the given type, name and defining expression. + * + * @param constantType The type of the constant. + * @param constantName The name of the constant. + * @param expression The expression that defines the constant. + * @param filename The filename in which the transition reward is defined. + * @param lineNumber The line number in which the transition reward is defined. + */ + Constant(ConstantType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + /*! + * Creates an undefined constant with the given type and name. + * + * @param constantType The type of the constant. + * @param constantName The name of the constant. + * @param filename The filename in which the transition reward is defined. + * @param lineNumber The line number in which the transition reward is defined. + */ + Constant(ConstantType constantType, std::string const& constantName, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + // Create default implementations of constructors/assignment. + Constant() = default; + Constant(Constant const& other) = default; + Constant& operator=(Constant const& other)= default; + Constant(Constant&& other) = default; + Constant& operator=(Constant&& other) = default; + + /*! + * Retrieves the name of the constant. + * + * @return The name of the constant. + */ + std::string const& getConstantName() const; + + /*! + * Retrieves the type of the constant. + * + * @return The type of the constant; + */ + ConstantType getConstantType() const; + + /*! + * Retrieves whether the constant is defined, i.e., whether there is an expression defining its value. + * + * @return True iff the constant is defined. + */ + bool isDefined() const; + + /*! + * Retrieves the expression that defines the constant. This may only be called if the object is a defined + * constant. + * + * @return The expression that defines the constant. + */ + storm::expressions::Expression const& getExpression() const; + + friend std::ostream& operator<<(std::ostream& stream, Constant const& constant); + + private: + // The type of the constant. + ConstantType constantType; + + // The name of the constant. + std::string constantName; + + // A flag that stores whether or not the constant is defined. + bool defined; + + // The expression that defines the constant (in case it is defined). + storm::expressions::Expression expression; + }; + } // namespace prism +} // namespace storm + +#endif /* STORM_STORAGE_PRISM_CONSTANT_H_ */ diff --git a/src/storage/prism/Formula.cpp b/src/storage/prism/Formula.cpp new file mode 100644 index 000000000..e665f22f7 --- /dev/null +++ b/src/storage/prism/Formula.cpp @@ -0,0 +1,26 @@ +#include "src/storage/prism/Formula.h" + +namespace storm { + namespace prism { + Formula::Formula(std::string const& formulaName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), formulaName(formulaName), expression(expression) { + // Intentionally left empty. + } + + std::string const& Formula::getFormulaName() const { + return this->formulaName; + } + + storm::expressions::Expression const& Formula::getExpression() const { + return this->expression; + } + + storm::expressions::ExpressionReturnType Formula::getReturnType() const { + return this->getExpression().getReturnType(); + } + + std::ostream& operator<<(std::ostream& stream, Formula const& formula) { + stream << "formula " << formula.getFormulaName() << " = " << formula.getExpression() << ";"; + return stream; + } + } +} \ No newline at end of file diff --git a/src/storage/prism/Formula.h b/src/storage/prism/Formula.h new file mode 100644 index 000000000..4ae67b9dd --- /dev/null +++ b/src/storage/prism/Formula.h @@ -0,0 +1,62 @@ +#ifndef STORM_STORAGE_PRISM_FORMULA_H_ +#define STORM_STORAGE_PRISM_FORMULA_H_ + +#include "src/storage/prism/LocatedInformation.h" +#include "src/storage/expressions/Expression.h" + +namespace storm { + namespace prism { + class Formula : public LocatedInformation { + public: + /*! + * Creates a formula with the given name and expression. + * + * @param formulaName The name of the label. + * @param expression The predicate that needs to hold before taking a transition with the previously + * specified name in order to obtain the reward. + * @param filename The filename in which the transition reward is defined. + * @param lineNumber The line number in which the transition reward is defined. + */ + Formula(std::string const& formulaName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + // Create default implementations of constructors/assignment. + Formula() = default; + Formula(Formula const& other) = default; + Formula& operator=(Formula const& other)= default; + Formula(Formula&& other) = default; + Formula& operator=(Formula&& other) = default; + + /*! + * Retrieves the name that is associated with this formula. + * + * @return The name that is associated with this formula. + */ + std::string const& getFormulaName() const; + + /*! + * Retrieves the expression that is associated with this formula. + * + * @return The expression that is associated with this formula. + */ + storm::expressions::Expression const& getExpression() const; + + /*! + * Retrieves the return type of the formula, i.e., the return-type of the defining expression. + * + * @return The return type of the formula. + */ + storm::expressions::ExpressionReturnType getReturnType() const; + + friend std::ostream& operator<<(std::ostream& stream, Formula const& formula); + + private: + // The name of the formula. + std::string formulaName; + + // A predicate that needs to be satisfied by states for the label to be attached. + storm::expressions::Expression expression; + }; + } // namespace prism +} // namespace storm + +#endif /* STORM_STORAGE_PRISM_FORMULA_H_ */ diff --git a/src/storage/prism/Label.cpp b/src/storage/prism/Label.cpp new file mode 100644 index 000000000..297d8691e --- /dev/null +++ b/src/storage/prism/Label.cpp @@ -0,0 +1,22 @@ +#include "src/storage/prism/Label.h" + +namespace storm { + namespace prism { + Label::Label(std::string const& labelName, storm::expressions::Expression const& statePredicateExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), labelName(labelName), statePredicateExpression(statePredicateExpression) { + // Intentionally left empty. + } + + std::string const& Label::getLabelName() const { + return this->labelName; + } + + storm::expressions::Expression const& Label::getStatePredicateExpression() const { + return this->statePredicateExpression; + } + + std::ostream& operator<<(std::ostream& stream, Label const& label) { + stream << "label \"" << label.getLabelName() << "\" = " << label.getStatePredicateExpression() << ";"; + return stream; + } + } +} \ No newline at end of file diff --git a/src/storage/prism/Label.h b/src/storage/prism/Label.h new file mode 100644 index 000000000..d1ae6e0fd --- /dev/null +++ b/src/storage/prism/Label.h @@ -0,0 +1,55 @@ +#ifndef STORM_STORAGE_PRISM_LABEL_H_ +#define STORM_STORAGE_PRISM_LABEL_H_ + +#include "src/storage/prism/LocatedInformation.h" +#include "src/storage/expressions/Expression.h" + +namespace storm { + namespace prism { + class Label : public LocatedInformation { + public: + /*! + * Creates a label with the given name and state predicate expression. + * + * @param labelName The name of the label. + * @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously + * specified name in order to obtain the reward. + * @param filename The filename in which the transition reward is defined. + * @param lineNumber The line number in which the transition reward is defined. + */ + Label(std::string const& labelName, storm::expressions::Expression const& statePredicateExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + // Create default implementations of constructors/assignment. + Label() = default; + Label(Label const& other) = default; + Label& operator=(Label const& other)= default; + Label(Label&& other) = default; + Label& operator=(Label&& other) = default; + + /*! + * Retrieves the name that is associated with this label. + * + * @return The name that is associated with this label. + */ + std::string const& getLabelName() const; + + /*! + * Retrieves the state predicate expression that is associated with this label. + * + * @return The state predicate expression that is associated with this label. + */ + storm::expressions::Expression const& getStatePredicateExpression() const; + + friend std::ostream& operator<<(std::ostream& stream, Label const& label); + + private: + // The name of the label. + std::string labelName; + + // A predicate that needs to be satisfied by states for the label to be attached. + storm::expressions::Expression statePredicateExpression; + }; + } // namespace prism +} // namespace storm + +#endif /* STORM_STORAGE_PRISM_LABEL_H_ */ diff --git a/src/storage/prism/LocatedInformation.h b/src/storage/prism/LocatedInformation.h index f86060958..638734f9f 100644 --- a/src/storage/prism/LocatedInformation.h +++ b/src/storage/prism/LocatedInformation.h @@ -16,6 +16,7 @@ namespace storm { LocatedInformation(std::string const& filename, uint_fast64_t lineNumber); // Create default implementations of constructors/assignment. + LocatedInformation() = default; LocatedInformation(LocatedInformation const& other) = default; LocatedInformation& operator=(LocatedInformation const& other)= default; LocatedInformation(LocatedInformation&& other) = default; diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 78f561734..69abaa2b6 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -5,26 +5,29 @@ namespace storm { namespace prism { - Module::Module(std::string const& moduleName, std::map const& booleanVariables, std::map const& integerVariables, std::vector const& commands, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands), actions(), actionsToCommandIndexMap() { + Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap() { + // FIXME: construct mappings from variable names to their indices. // Initialize the internal mappings for fast information retrieval. this->collectActions(); } Module::Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(newModuleName), booleanVariables(), integerVariables(), commands(), actions(), actionsToCommandIndexMap() { // Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception is thrown. - for (auto const& nameVariablePair : oldModule.getBooleanVariables()) { - auto renamingPair = renaming.find(nameVariablePair.first); - LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Boolean variable " << moduleName << "." << nameVariablePair.first << " was not renamed."); - this->booleanVariables.emplace(nameVariablePair.first, BooleanVariable(nameVariablePair.second, renamingPair->second, renaming, filename, lineNumber)); + for (auto const& booleanVariable : oldModule.getBooleanVariables()) { + auto const& renamingPair = renaming.find(booleanVariable.getName()); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::InvalidArgumentException, "Boolean variable '" << booleanVariable.getName() << " was not renamed."); + this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, renaming, filename, lineNumber); } // Now do the same for the integer variables. - for (auto const& nameVariablePair : oldModule.getIntegerVariables()) { - auto renamingPair = renaming.find(nameVariablePair.first); - LOG_THROW(renamingPair == renaming.end(), storm::exceptions::InvalidArgumentException, "Integer variable " << moduleName << "." << nameVariablePair.first << " was not renamed."); - this->integerVariables.emplace(nameVariablePair.first, IntegerVariable(nameVariablePair.second, renamingPair->second, renaming, filename, lineNumber)); + for (auto const& integerVariable : oldModule.getIntegerVariables()) { + auto const& renamingPair = renaming.find(integerVariable.getName()); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::InvalidArgumentException, "Integer variable '" << integerVariable.getName() << " was not renamed."); + this->integerVariables.emplace_back(integerVariable, renamingPair->second, renaming, filename, lineNumber); } + // FIXME: construct mappings from variable names to their indices. + // Now we are ready to clone all commands and rename them if requested. this->commands.reserve(oldModule.getNumberOfCommands()); for (Command const& command : oldModule.getCommands()) { @@ -44,22 +47,22 @@ namespace storm { } storm::prism::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const { - auto const& nameVariablePair = this->getBooleanVariables().find(variableName); - LOG_THROW(nameVariablePair == this->getBooleanVariables().end(), storm::exceptions::InvalidArgumentException, "Unknown boolean variable '" << variableName << "'."); - return nameVariablePair->second; + auto const& nameIndexPair = this->booleanVariableToIndexMap.find(variableName); + LOG_THROW(nameIndexPair != this->booleanVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown boolean variable '" << variableName << "'."); + return this->getBooleanVariables()[nameIndexPair->second]; } - std::map const& Module::getBooleanVariables() const { + std::vector const& Module::getBooleanVariables() const { return this->booleanVariables; } storm::prism::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const { - auto const& nameVariablePair = this->getIntegerVariables().find(variableName); - LOG_THROW(nameVariablePair == this->getIntegerVariables().end(), storm::exceptions::InvalidArgumentException, "Unknown integer variable '" << variableName << "'."); - return nameVariablePair->second; + auto const& nameIndexPair = this->integerVariableToIndexMap.find(variableName); + LOG_THROW(nameIndexPair != this->integerVariableToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown integer variable '" << variableName << "'."); + return this->getIntegerVariables()[nameIndexPair->second]; } - std::map const& Module::getIntegerVariables() const { + std::vector const& Module::getIntegerVariables() const { return this->integerVariables; } @@ -67,6 +70,14 @@ namespace storm { return this->commands.size(); } + std::size_t Module::getNumberOfUpdates() const { + std::size_t result = 0; + for (auto const& command : this->getCommands()) { + result += command.getNumberOfUpdates(); + } + return result; + } + storm::prism::Command const& Module::getCommand(uint_fast64_t index) const { return this->commands[index]; } @@ -136,11 +147,11 @@ namespace storm { std::ostream& operator<<(std::ostream& stream, Module const& module) { stream << "module " << module.getName() << std::endl; - for (auto const& nameVariablePair : module.getBooleanVariables()) { - stream << "\t" << nameVariablePair.second << std::endl; + for (auto const& booleanVariable : module.getBooleanVariables()) { + stream << "\t" << booleanVariable << std::endl; } - for (auto const& nameVariablePair : module.getIntegerVariables()) { - stream << "\t" << nameVariablePair.second << std::endl; + for (auto const& integerVariable : module.getIntegerVariables()) { + stream << "\t" << integerVariable << std::endl; } for (auto const& command : module.getCommands()) { stream << "\t" << command << std::endl; diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index d8f75d13b..cb62bc626 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -26,7 +26,7 @@ namespace storm { * @param filename The filename in which the module is defined. * @param lineNumber The line number in which the module is defined. */ - Module(std::string const& moduleName, std::map const& booleanVariables, std::map const& integerVariables, std::vector const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Special copy constructor, implementing the module renaming functionality. This will create a new module @@ -74,7 +74,7 @@ namespace storm { * * @return The boolean variables of the module. */ - std::map const& getBooleanVariables() const; + std::vector const& getBooleanVariables() const; /*! * Retrieves a reference to the integer variable with the given name. @@ -89,15 +89,22 @@ namespace storm { * * @return The integer variables of the module. */ - std::map const& getIntegerVariables() const; + std::vector const& getIntegerVariables() const; /*! * Retrieves the number of commands of this module. * - * @return the number of commands of this module. + * @return The number of commands of this module. */ std::size_t getNumberOfCommands() const; + /*! + * Retrieves the total number of updates of this module. + * + * @return The total number of updates of this module. + */ + std::size_t getNumberOfUpdates() const; + /*! * Retrieves a reference to the command with the given index. * @@ -163,11 +170,17 @@ namespace storm { std::string moduleName; // A list of boolean variables. - std::map booleanVariables; + std::vector booleanVariables; - // A list of integer variables. - std::map integerVariables; + // A mapping from boolean variables to the corresponding indices in the vector. + std::map booleanVariableToIndexMap; + // A list of integer variables. + std::vector integerVariables; + + // A mapping from integer variables to the corresponding indices in the vector. + std::map integerVariableToIndexMap; + // The commands associated with the module. std::vector commands; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 97daf8142..281be2531 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -5,7 +5,8 @@ namespace storm { namespace prism { - Program::Program(ModelType modelType, std::set const& undefinedBooleanConstants, std::map const& definedBooleanConstants, std::set const& undefinedIntegerConstants, std::map const& definedIntegerConstants, std::set const& undefinedDoubleConstants, std::map const& definedDoubleConstants, std::map const& globalBooleanVariables, std::map const& globalIntegerVariables, std::mapconst& formulas, std::vector const& modules, std::map const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::map const& labels, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), modelType(modelType), undefinedBooleanConstants(undefinedBooleanConstants), definedBooleanConstants(definedBooleanConstants), undefinedIntegerConstants(undefinedIntegerConstants), definedIntegerConstants(definedIntegerConstants), undefinedDoubleConstants(undefinedDoubleConstants), definedDoubleConstants(definedDoubleConstants), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), formulas(formulas), modules(modules), rewardModels(rewardModels), hasInitialStatesExpression(hasInitialStatesExpression), initialStatesExpression(initialStatesExpression), labels(labels), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() { + Program::Program(ModelType modelType, std::vector const& undefinedConstants, std::vector const& definedConstants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::vector const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector