diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp deleted file mode 100644 index 98f58f208..000000000 --- a/src/parser/PrismParser.cpp +++ /dev/null @@ -1,98 +0,0 @@ -#include "src/parser/PrismParser.h" - -#include "src/parser/prismparser/PrismGrammar.h" - -// If the parser fails due to ill-formed data, this exception is thrown. -#include "src/exceptions/WrongFormatException.h" - -// Needed for file IO. -#include -#include -#include - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -#include "log4cplus/consoleappender.h" -#include "log4cplus/fileappender.h" -log4cplus::Logger logger; - -namespace storm { - 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(); - - // Now propagate exception. - throw storm::exceptions::WrongFormatException() << msg.str(); - } - - return result; - } - } // namespace parser -} // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h deleted file mode 100644 index 49bdd20c5..000000000 --- a/src/parser/PrismParser.h +++ /dev/null @@ -1,35 +0,0 @@ -#ifndef STORM_PARSER_PRISMPARSER_H_ -#define STORM_PARSER_PRISMPARSER_H_ - -// All classes of the intermediate representation are used. -#include "src/storage/prism/Program.h" - -// Used for file input. -#include - -namespace storm { - namespace parser { - using namespace storm::prism; - using namespace storm::expressions; - - /*! - * Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax. - * - * @param filename the name of the file to parse. - * @return The resulting PRISM program. - */ - storm::prism::Program PrismParserFromFile(std::string const& filename); - - /*! - * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax. - * - * @param inputStream The input stream to parse. - * @param filename The name of the file the input stream belongs to. - * @return The resulting PRISM program. - */ - storm::prism::Program PrismParser(std::istream& inputStream, std::string const& filename); - - } // namespace parser -} // namespace storm - -#endif /* STORM_PARSER_PRISMPARSER_H_ */ diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 72b7a40b8..b8c06daa9 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -1,153 +1,372 @@ +// #define BOOST_SPIRIT_DEBUG #include "src/parser/prismparser/PrismGrammar.h" #include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/WrongFormatException.h" namespace storm { namespace parser { namespace prism { - PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start) { + PrismGrammar::PrismGrammar(std::string const& filename, Iterator first) : PrismGrammar::base_type(start), doExpressionGeneration(false), filename(filename), annotate(first) { // Parse simple identifier. - identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]] - keywords_; + identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismGrammar::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); - // Parse a composed expression. - expression %= (booleanExpression | numericalExpression); - expression.name("expression"); + setExpressionGeneration(doExpressionGeneration); - booleanExpression %= orExpression; - expression.name("boolean expression"); - - orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = qi::_val * qi::_1]; - orExpression.name("boolean expression"); - - andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = qi::_val * qi::_1]; - andExpression.name("boolean expression"); - - notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = !qi::_1]; - notExpression.name("boolean expression"); - - atomicBooleanExpression %= relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")"); - atomicBooleanExpression.name("boolean expression"); - - relativeExpression = ((numericalExpression >> ">") > numericalExpression)[qi::_val = qi::_1 > qi::_2] | ((numericalExpression >> ">=") > numericalExpression)[qi::_val = qi::_1 >= qi::_2] | ((numericalExpression >> "<") > numericalExpression)[qi::_val = qi::_1 < qi::_2] | ((numericalExpression >> "<=") > numericalExpression)[qi::_val = qi::_1 <= qi::_2]; - relativeExpression.name("relative expression"); - - booleanVariableExpression = identifier[qi::_val = phoenix::bind(&storm::expressions::Expression::createBooleanVariable, qi::_1)]; - booleanVariableExpression.name("boolean variable"); - - numericalExpression %= plusExpression; - numericalExpression.name("numerical expression"); - - plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = qi::_val + qi::_1] .else_ [qi::_val = qi::_val - qi::_1]]; - plusExpression.name("numerical expression"); - - multiplicationExpression = atomicNumericalExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicNumericalExpression[qi::_val = qi::_val * qi::_1]); - multiplicationExpression.name("numerical expression"); - - 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.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.name("integer floor/ceil expression"); - - numericalVariableExpression = identifier[qi::_val = phoenix::bind(&storm::expressions::Expression::createDoubleVariable, qi::_1)]; - numericalVariableExpression.name("numerical variable"); - - modelTypeDefinition = modelType_; + modelTypeDefinition %= modelType_; modelTypeDefinition.name("model type"); - - undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r1) | undefinedDoubleConstantDefinition(qi::_r1)); - undefinedConstantDefinition.name("undefined constant definition"); - 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 = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)]; undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - 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 = ((qi::lit("const") >> qi::lit("int")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createUndefinedIntegerConstant, phoenix::ref(*this), qi::_1)]; undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); - 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 = ((qi::lit("const") >> qi::lit("double")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createUndefinedDoubleConstant, phoenix::ref(*this), qi::_1)]; undefinedDoubleConstantDefinition.name("undefined double constant definition"); - definedConstantDefinition %= (definedBooleanConstantDefinition(qi::_r1) | definedIntegerConstantDefinition(qi::_r1) | definedDoubleConstantDefinition(qi::_r1)); - definedConstantDefinition.name("defined constant definition"); + undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition); + undefinedConstantDefinition.name("undefined 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 = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)]; definedBooleanConstantDefinition.name("defined boolean constant declaration"); - 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 = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)]; definedIntegerConstantDefinition.name("defined integer constant declaration"); - 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 = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)]; definedDoubleConstantDefinition.name("defined double constant 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)]; + definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); + definedConstantDefinition.name("defined constant definition"); + + formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createFormula, phoenix::ref(*this), qi::_1, qi::_2)]; formulaDefinition.name("formula definition"); - globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1)) | integerVariableDefinition(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1)))); + booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expression) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)]; + booleanVariableDefinition.name("boolean variable definition"); + + integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismGrammar::allowDoubleLiterals, phoenix::ref(*this), false)]) > expression[qi::_a = qi::_1] > qi::lit("..") > expression > qi::lit("]")[phoenix::bind(&PrismGrammar::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; + integerVariableDefinition.name("integer variable definition"); + + variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]); + variableDefinition.name("variable declaration"); + + globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)])); globalVariableDefinition.name("global variable declaration list"); - programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1] - > *( undefinedConstantDefinition(qi::_r1) - | definedConstantDefinition(qi::_r1) - | formulaDefinition(qi::_r1) - | globalVariableDefinition(qi::_r1) - ); + programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1] + > *(definedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)] | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, qi::_r1), qi::_1)]) + > *(formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_r1), qi::_1)]) + > *(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 = (expression > qi::lit(":") > plusExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)]; stateRewardDefinition.name("state reward definition"); - 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 = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit(":") > plusExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3)]; transitionRewardDefinition.name("transition reward definition"); - 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)]; + 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"))[qi::_val = phoenix::bind(&PrismGrammar::createRewardModel, phoenix::ref(*this), qi::_1, qi::_a, qi::_b)]; + rewardModelDefinition.name("reward model definition"); + + initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismGrammar::addInitialStatesExpression, phoenix::ref(*this), qi::_1, qi::_r1)]; + initialStatesConstruct.name("initial construct"); + + labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createLabel, phoenix::ref(*this), 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 = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&PrismGrammar::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)]; assignmentDefinition.name("assignment"); - assignmentDefinitionList = assignmentDefinition(qi::_r1) % "&"; - assignmentDefinitionList.name("assignment list"); - moduleDefinitionList %= +(moduleDefinition(qi::_r1) | moduleRenaming(qi::_r1)); - moduleDefinitionList.name("module list"); + assignmentDefinitionList %= +assignmentDefinition % "&"; + assignmentDefinitionList.name("assignment 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 = (((plusExpression > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; updateDefinition.name("update"); - updateListDefinition %= +updateDefinition % "+"; + updateListDefinition %= +updateDefinition(qi::_r1) % "+"; updateListDefinition.name("update 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 = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismGrammar::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)]; 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"); - - 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 = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)]; moduleDefinition.name("module definition"); - moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[") + 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)]; + > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismGrammar::createRenamedModule, phoenix::ref(*this), 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)]; + moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)]; + moduleDefinitionList.name("module list"); + + start = (qi::eps > programHeader(qi::_a) > moduleDefinitionList(qi::_a) > *(initialStatesConstruct(qi::_a) | rewardModelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, qi::_a), qi::_1)] | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, qi::_a), qi::_1)]) > qi::eoi)[qi::_val = phoenix::bind(&PrismGrammar::createProgram, phoenix::ref(*this), qi::_a)]; start.name("probabilistic program"); + + // Enable location tracking for important entities. + auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3); + qi::on_success(undefinedBooleanConstantDefinition, setLocationInfoFunction); + qi::on_success(undefinedIntegerConstantDefinition, setLocationInfoFunction); + qi::on_success(undefinedDoubleConstantDefinition, setLocationInfoFunction); + qi::on_success(definedBooleanConstantDefinition, setLocationInfoFunction); + qi::on_success(definedIntegerConstantDefinition, setLocationInfoFunction); + qi::on_success(definedDoubleConstantDefinition, setLocationInfoFunction); + qi::on_success(booleanVariableDefinition, setLocationInfoFunction); + qi::on_success(integerVariableDefinition, setLocationInfoFunction); + qi::on_success(moduleDefinition, setLocationInfoFunction); + qi::on_success(moduleRenaming, setLocationInfoFunction); + qi::on_success(formulaDefinition, setLocationInfoFunction); + qi::on_success(rewardModelDefinition, setLocationInfoFunction); + qi::on_success(labelDefinition, setLocationInfoFunction); + qi::on_success(commandDefinition, setLocationInfoFunction); + qi::on_success(updateDefinition, setLocationInfoFunction); + qi::on_success(assignmentDefinition, setLocationInfoFunction); + } + + void PrismGrammar::setExpressionGeneration(bool doExpressionGeneration) { + if (doExpressionGeneration) { + floorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> 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("floor/ceil expression"); + + minMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(",") >> plusExpression >> 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"); + + identifierExpression = identifier[qi::_val = phoenix::bind(&PrismGrammar::getIdentifierExpression, phoenix::ref(*this), qi::_1)]; + identifierExpression.name("identifier expression"); + + literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&storm::expressions::Expression::createTrue)] | qi::lit("false")[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)] | strict_double[qi::_val = phoenix::bind(&storm::expressions::Expression::createDoubleLiteral, qi::_1)] | qi::int_[qi::_val = phoenix::bind(&storm::expressions::Expression::createIntegerLiteral, qi::_1)]; + literalExpression.name("literal expression"); + + atomicExpression = minMaxExpression | floorCeilExpression | qi::lit("(") >> expression >> qi::lit(")") | literalExpression | identifierExpression; + atomicExpression.name("atomic expression"); + + unaryExpression = atomicExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicExpression)[qi::_val = !qi::_1] | (qi::lit("-") >> atomicExpression)[qi::_val = -qi::_1]; + unaryExpression.name("unary expression"); + + multiplicationExpression = unaryExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> unaryExpression[phoenix::if_(qi::_a) [qi::_val = qi::_val * qi::_1] .else_ [qi::_val = qi::_val / qi::_1]]); + multiplicationExpression.name("multiplication expression"); + + plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = qi::_val + qi::_1] .else_ [qi::_val = qi::_val - qi::_1]]; + plusExpression.name("plus expression"); + + relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = qi::_1 >= qi::_1] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = qi::_1 > qi::_2] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = qi::_1 <= qi::_2] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = qi::_1 < qi::_2] | (plusExpression >> qi::lit("=") >> plusExpression)[qi::_val = qi::_1 == qi::_2] | (plusExpression >> qi::lit("!=") >> plusExpression)[qi::_val = qi::_1 != qi::_2] | plusExpression[qi::_val = qi::_1]; + relativeExpression.name("relative expression"); + + andExpression = relativeExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> relativeExpression)[qi::_val = qi::_val && qi::_1]; + andExpression.name("and expression"); + + orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = qi::_val || qi::_1]; + orExpression.name("or expression"); + + expression %= orExpression; + expression.name("expression"); + } else { + floorCeilExpression = ((qi::lit("floor") | qi::lit("ceil")) >> qi::lit("(") >> plusExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + floorCeilExpression.name("floor/ceil expression"); + + minMaxExpression = ((qi::lit("min") | qi::lit("max")) >> qi::lit("(") >> plusExpression >> qi::lit(",") >> plusExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + minMaxExpression.name("min/max expression"); + + identifierExpression = identifier[qi::_val = phoenix::construct(), qi::_pass = phoenix::bind(&PrismGrammar::isValidIdentifier, phoenix::ref(*this), qi::_1)]; + identifierExpression.name("identifier expression"); + + literalExpression = (qi::lit("true") | qi::lit("false") | strict_double | qi::int_)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + literalExpression.name("literal expression"); + + atomicExpression = (minMaxExpression | floorCeilExpression | qi::lit("(") >> expression >> qi::lit(")") | literalExpression | identifierExpression)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + atomicExpression.name("atomic expression"); + + unaryExpression = (atomicExpression | (qi::lit("!") >> atomicExpression) | (qi::lit("-") >> atomicExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + unaryExpression.name("unary expression"); + + multiplicationExpression = (unaryExpression >> *((qi::lit("*") | qi::lit("/")) >> unaryExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + multiplicationExpression.name("multiplication expression"); + + plusExpression = (multiplicationExpression >> *((qi::lit("+") | qi::lit("-")) >> multiplicationExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + plusExpression.name("plus expression"); + + relativeExpression = ((plusExpression >> qi::lit(">=") >> plusExpression) | (plusExpression >> qi::lit(">") >> plusExpression) | (plusExpression >> qi::lit("<=") >> plusExpression) | (plusExpression >> qi::lit("<") >> plusExpression) | (plusExpression >> qi::lit("=") >> plusExpression) | (plusExpression >> qi::lit("!=") >> plusExpression) | plusExpression)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + relativeExpression.name("relative expression"); + + andExpression = (relativeExpression >> *(qi::lit("&") >> relativeExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + andExpression.name("and expression"); + + orExpression = (andExpression >> *(qi::lit("|") >> andExpression))[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + orExpression.name("or expression"); + + expression %= orExpression; + expression.name("expression"); + } + + // Enable error reporting. + qi::on_error(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + + // Finally toggle the internal flag. + this->doExpressionGeneration = doExpressionGeneration; + } + + void PrismGrammar::toggleExpressionGeneration() { + setExpressionGeneration(!doExpressionGeneration); + } + + void PrismGrammar::allowDoubleLiterals(bool flag) { + if (flag) { + if (this->doExpressionGeneration) { + literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&storm::expressions::Expression::createTrue)] | qi::lit("false")[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)] | strict_double[qi::_val = phoenix::bind(&storm::expressions::Expression::createDoubleLiteral, qi::_1)] | qi::int_[qi::_val = phoenix::bind(&storm::expressions::Expression::createIntegerLiteral, qi::_1)]; + literalExpression.name("literal expression"); + } else { + literalExpression = (qi::lit("true") | qi::lit("false") | strict_double | qi::int_)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + literalExpression.name("literal expression"); + } + } else { + if (this->doExpressionGeneration) { + literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&storm::expressions::Expression::createTrue)] | qi::lit("false")[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)] | qi::int_[qi::_val = phoenix::bind(&storm::expressions::Expression::createIntegerLiteral, qi::_1)]; + literalExpression.name("literal expression"); + } else { + literalExpression = (qi::lit("true") | qi::lit("false") | qi::int_)[qi::_val = phoenix::bind(&storm::expressions::Expression::createFalse)]; + literalExpression.name("literal expression"); + } + } + } + + std::string const& PrismGrammar::getFilename() const { + return this->filename; + } + + bool PrismGrammar::isValidIdentifier(std::string const& identifier) { + if (this->keywords_.find(identifier) != nullptr) { + return false; + } + return true; + } + + bool PrismGrammar::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { + LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::InvalidArgumentException, "Program must not define two initial constructs."); + if (globalProgramInformation.hasInitialStatesExpression) { + return false; + } + globalProgramInformation.hasInitialStatesExpression = true; + globalProgramInformation.initialStatesExpression = initialStatesExpression; + return true; + } + + storm::expressions::Expression PrismGrammar::getIdentifierExpression(std::string const& identifier) const { + storm::expressions::Expression const* expression = this->identifiers_.find(identifier); + LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Undeclared identifier '" << identifier << "'."); + return *expression; + } + + storm::prism::Constant PrismGrammar::createUndefinedBooleanConstant(std::string const& newConstant) const { + this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + return storm::prism::Constant(storm::prism::Constant::ConstantType::Bool, newConstant, this->getFilename()); + } + + storm::prism::Constant PrismGrammar::createUndefinedIntegerConstant(std::string const& newConstant) const { + this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + return storm::prism::Constant(storm::prism::Constant::ConstantType::Integer, newConstant, this->getFilename()); + } + + storm::prism::Constant PrismGrammar::createUndefinedDoubleConstant(std::string const& newConstant) const { + this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + return storm::prism::Constant(storm::prism::Constant::ConstantType::Double, newConstant, this->getFilename()); + } + + storm::prism::Constant PrismGrammar::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const { + this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant)); + return storm::prism::Constant(storm::prism::Constant::ConstantType::Bool, newConstant, expression, this->getFilename()); + } + + storm::prism::Constant PrismGrammar::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const { + this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant)); + return storm::prism::Constant(storm::prism::Constant::ConstantType::Integer, newConstant, expression, this->getFilename()); + } + + storm::prism::Constant PrismGrammar::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const { + this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant)); + return storm::prism::Constant(storm::prism::Constant::ConstantType::Double, newConstant, expression, this->getFilename()); + } + + storm::prism::Formula PrismGrammar::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const { + this->identifiers_.add(formulaName, expression); + return storm::prism::Formula(formulaName, expression, this->getFilename()); + } + + storm::prism::Label PrismGrammar::createLabel(std::string const& labelName, storm::expressions::Expression expression) const { + return storm::prism::Label(labelName, expression, this->getFilename()); + } + + storm::prism::RewardModel PrismGrammar::createRewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards) const { + return storm::prism::RewardModel(rewardModelName, stateRewards, transitionRewards, this->getFilename()); + } + + storm::prism::StateReward PrismGrammar::createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const { + return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename()); + } + + storm::prism::TransitionReward PrismGrammar::createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const { + return storm::prism::TransitionReward(actionName, statePredicateExpression, rewardValueExpression, this->getFilename()); + } + + storm::prism::Assignment PrismGrammar::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const { + return storm::prism::Assignment(variableName, assignedExpression, this->getFilename()); + } + + storm::prism::Update PrismGrammar::createUpdate(storm::expressions::Expression likelihoodExpression, std::vector const& assignments, GlobalProgramInformation& globalProgramInformation) const { + ++globalProgramInformation.currentUpdateIndex; + return storm::prism::Update(globalProgramInformation.currentUpdateIndex - 1, likelihoodExpression, assignments, this->getFilename()); + } + + storm::prism::Command PrismGrammar::createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector const& updates, GlobalProgramInformation& globalProgramInformation) const { + ++globalProgramInformation.currentCommandIndex; + return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, actionName, guardExpression, updates, this->getFilename()); + } + + storm::prism::BooleanVariable PrismGrammar::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const { + this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName)); + return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename()); + } + + storm::prism::IntegerVariable PrismGrammar::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const { + this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName)); + return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename()); + } + + storm::prism::Module PrismGrammar::createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const { + globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size(); + return storm::prism::Module(moduleName, booleanVariables, integerVariables, commands, this->getFilename()); + } + + storm::prism::Module PrismGrammar::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const { + auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName); + LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "No module named '" << oldModuleName << "' to rename."); + globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size(); + uint_fast64_t commandBaseIndex = globalProgramInformation.currentCommandIndex; + uint_fast64_t updateBaseIndex = globalProgramInformation.currentUpdateIndex; + storm::prism::Module const& moduleToClone = globalProgramInformation.modules[moduleIndexPair->second]; + globalProgramInformation.currentCommandIndex += moduleToClone.getNumberOfCommands(); + globalProgramInformation.currentUpdateIndex += moduleToClone.getNumberOfUpdates(); + return storm::prism::Module(moduleToClone, newModuleName, commandBaseIndex, updateBaseIndex, renaming, this->getFilename()); + } + + storm::prism::Program PrismGrammar::createProgram(GlobalProgramInformation const& globalProgramInformation) const { + return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, globalProgramInformation.hasInitialStatesExpression, globalProgramInformation.initialStatesExpression, globalProgramInformation.labels, this->getFilename()); } } // namespace prism } // namespace parser diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index d51ee4f04..29d0afb96 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -4,33 +4,32 @@ // Include files for file input. #include #include +#include // Include boost spirit. +#define BOOST_SPIRIT_USE_PHOENIX_V3 #include #include #include - -// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. -#include -#include +#include +#include namespace qi = boost::spirit::qi; namespace phoenix = boost::phoenix; typedef std::string::const_iterator BaseIteratorType; -typedef boost::spirit::classic::position_iterator2 PositionIteratorType; +typedef boost::spirit::line_pos_iterator PositionIteratorType; typedef PositionIteratorType Iterator; typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper; typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2; -typedef boost::spirit::unused_type Unused; #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" +#include "src/exceptions/ExceptionMacros.h" namespace storm { namespace parser { namespace prism { - struct modelTypeStruct : qi::symbols { modelTypeStruct() { add @@ -42,7 +41,7 @@ namespace storm { } }; - struct keywordsStruct : qi::symbols { + struct keywordsStruct : qi::symbols { keywordsStruct() { add ("dtmc", 1) @@ -58,7 +57,12 @@ namespace storm { ("rewards", 11) ("endrewards", 12) ("true", 13) - ("false", 14); + ("min", 14) + ("max", 15) + ("floor", 16) + ("ceil", 17) + ("init", 18) + ("endinit", 19); } }; @@ -69,32 +73,104 @@ namespace storm { // Members for all essential information that needs to be collected. storm::prism::Program::ModelType modelType; - std::set undefinedBooleanConstants; - std::set undefinedIntegerConstants; - std::set undefinedDoubleConstants; - std::map definedBooleanConstants; - std::map definedIntegerConstants; - std::map definedDoubleConstants; - std::map formulas; - std::map globalBooleanVariables; - std::map globalIntegerVariables; - std::map modules; - std::map rewardModels; - std::map labels; + std::vector constants; + std::vector formulas; + std::vector globalBooleanVariables; + std::vector globalIntegerVariables; + std::map moduleToIndexMap; + std::vector modules; + std::vector rewardModels; + std::vector labels; + storm::expressions::Expression initialStatesExpression; + bool hasInitialStatesExpression; // Counters to provide unique indexing for commands and updates. uint_fast64_t currentCommandIndex; uint_fast64_t currentUpdateIndex; }; + // Functor used for displaying error information. + struct ErrorHandler { + typedef qi::error_handler_result result_type; + + template + qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { +// LOG4CPLUS_ERROR(logger, "Error: expecting " << what << " in line " << get_line(where) << " at column " << get_column(b, where, 4) << "."); + std::cerr << "Error: expecting " << what << " in line " << get_line(where) << "." << std::endl; + T3 end(where); + while (end != e && *end != '\r' && *end != '\n') { + ++end; + } + std::cerr << "Error: expecting " << what << " in line " << get_line(where) << ": \n" << std::string(get_line_start(b, where), end) << " ... \n" << std::setw(std::distance(b, where)) << '^' << "---- here\n"; + return qi::fail; + } + }; + + // Functor used for annotating entities with line number information. + class PositionAnnotation { + public: + typedef void result_type; + + PositionAnnotation(Iterator first) : first(first) { + // Intentionally left empty. + } + + template + result_type operator()(Entity& entity, First f, Last l) const { + entity.setLineNumber(get_line(f)); + } + private: + std::string filename; + Iterator const first; + }; + class PrismGrammar : public qi::grammar, Skipper> { public: /*! - * Default constructor that creates an empty and functional grammar. + * Creates a grammar for the given filename and the iterator to the first input to parse. + * + * @param filename The filename that is to be read. This is used for proper error reporting. + * @param first The iterator to the beginning of the input. + */ + PrismGrammar(std::string const& filename, Iterator first); + + /*! + * Toggles whether or not expressions are generated. */ - PrismGrammar(); + void toggleExpressionGeneration(); private: + // A flag that stores whether the grammar currently generates expressions or not. + bool doExpressionGeneration; + + /*! + * Sets the expression generation to the desired value. + * + * @param doExpressionGeneration A flag that sets whether or not expressions are generated. + */ + void setExpressionGeneration(bool doExpressionGeneration); + + /*! + * Sets whether doubles literals are allowed in the parsed expression. + * + * @param flag Indicates whether to allow or forbid double literals in the parsed expression. + */ + void allowDoubleLiterals(bool flag); + + // The name of the file being parsed. + std::string filename; + + /*! + * Retrieves the name of the file currently being parsed. + * + * @return The name of the file currently being parsed. + */ + std::string const& getFilename() const; + + // A function used for annotating the entities with their position. + phoenix::function handler; + phoenix::function annotate; + // The starting point of the grammar. qi::rule, Skipper> start; @@ -103,14 +179,14 @@ namespace storm { // Rules for parsing the program header. qi::rule programHeader; - qi::rule undefinedConstantDefinition; - qi::rule undefinedBooleanConstantDefinition; - qi::rule undefinedIntegerConstantDefinition; - qi::rule undefinedDoubleConstantDefinition; - qi::rule definedConstantDefinition; - qi::rule definedBooleanConstantDefinition; - qi::rule definedIntegerConstantDefinition; - qi::rule definedDoubleConstantDefinition; + qi::rule undefinedConstantDefinition; + 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; @@ -119,81 +195,83 @@ namespace storm { // Rules for modules definition. qi::rule(GlobalProgramInformation&), Skipper> moduleDefinitionList; - qi::rule, std::map>, Skipper> moduleDefinition; + qi::rule, std::vector>, Skipper> moduleDefinition; qi::rule>, Skipper> moduleRenaming; // Rules for variable definitions. - qi::rule&, std::map&), Skipper> variableDefinition; - qi::rule&), Skipper> booleanVariableDefinition; - qi::rule&), qi::locals, Skipper> integerVariableDefinition; + qi::rule&, std::vector&), Skipper> variableDefinition; + qi::rule booleanVariableDefinition; + qi::rule, Skipper> integerVariableDefinition; // Rules for command definitions. - qi::rule, Skipper> commandDefinition; - qi::rule(), Skipper> updateListDefinition; - qi::rule>, Skipper> updateDefinition; - qi::rule&), Skipper> assignmentDefinitionList; - qi::rule&), Skipper> assignmentDefinition; + qi::rule, Skipper> commandDefinition; + qi::rule(GlobalProgramInformation&), Skipper> updateListDefinition; + qi::rule updateDefinition; + qi::rule(), Skipper> assignmentDefinitionList; + qi::rule assignmentDefinition; // Rules for reward definitions. - qi::rule, std::vector>, Skipper> rewardModelDefinition; + qi::rule, std::vector>, Skipper> rewardModelDefinition; qi::rule stateRewardDefinition; qi::rule, Skipper> transitionRewardDefinition; + // Rules for initial states expression. + qi::rule initialStatesConstruct; + // Rules for label definitions. - qi::rule labelDefinition; + qi::rule labelDefinition; // Rules for formula definitions. - qi::rule formulaDefinition; + qi::rule formulaDefinition; // Rules for identifier parsing. qi::rule identifier; // Rules for parsing a composed expression. qi::rule expression; - qi::rule booleanExpression; qi::rule orExpression; qi::rule andExpression; - qi::rule notExpression; - qi::rule atomicBooleanExpression; qi::rule relativeExpression; - qi::rule booleanVariableExpression; - qi::rule numericalExpression; qi::rule, Skipper> plusExpression; - qi::rule multiplicationExpression; - qi::rule atomicNumericalExpression; - qi::rule numericalVariableExpression; + qi::rule, Skipper> multiplicationExpression; + qi::rule unaryExpression; + qi::rule atomicExpression; + qi::rule literalExpression; + qi::rule identifierExpression; qi::rule, Skipper> minMaxExpression; qi::rule, Skipper> floorCeilExpression; + // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). + boost::spirit::qi::real_parser> strict_double; + // Parsers that recognize special keywords and model types. storm::parser::prism::keywordsStruct keywords_; storm::parser::prism::modelTypeStruct modelType_; + qi::symbols identifiers_; - // 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); + // Helper methods used in the grammar. + bool isValidIdentifier(std::string const& identifier); + bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); + storm::expressions::Expression getIdentifierExpression(std::string const& identifier) const; + storm::prism::Constant createUndefinedBooleanConstant(std::string const& newConstant) const; + storm::prism::Constant createUndefinedIntegerConstant(std::string const& newConstant) const; + storm::prism::Constant createUndefinedDoubleConstant(std::string const& newConstant) const; + storm::prism::Constant createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const; + storm::prism::Constant createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const; + storm::prism::Constant createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const; + storm::prism::Formula createFormula(std::string const& formulaName, storm::expressions::Expression expression) const; + storm::prism::Label createLabel(std::string const& labelName, storm::expressions::Expression expression) const; + storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector const& stateRewards, std::vector const& transitionRewards) const; + storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const; + storm::prism::TransitionReward createTransitionReward(std::string const& actionName, storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const; + storm::prism::Assignment createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const; + storm::prism::Update createUpdate(storm::expressions::Expression likelihoodExpression, std::vector const& assignments, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::Command createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector const& updates, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::BooleanVariable createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const; + storm::prism::IntegerVariable createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const; + storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; }; } // namespace prism } // namespace parser diff --git a/src/parser/prismparser/PrismParser.cpp b/src/parser/prismparser/PrismParser.cpp new file mode 100644 index 000000000..a261ba8cc --- /dev/null +++ b/src/parser/prismparser/PrismParser.cpp @@ -0,0 +1,70 @@ +#include "src/parser/prismparser/PrismParser.h" +#include "src/parser/prismparser/PrismGrammar.h" + +// If the parser fails due to ill-formed data, this exception is thrown. +#include "src/exceptions/ExceptionMacros.h" +#include "src/exceptions/WrongFormatException.h" + +// Needed for file IO. +#include +#include +#include + +namespace storm { + namespace parser { + storm::prism::Program PrismParser::parse(std::string const& filename, bool typeCheck) { + // Open file and initialize result. + std::ifstream inputFileStream(filename, std::ios::in); + LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file " << filename << "."); + + storm::prism::Program result; + + // Now try to parse the contents of the file. + try { + std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); + result = parseFromString(fileContent, filename, typeCheck); + } 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::parseFromString(std::string const& input, std::string const& filename, bool typeCheck) { + PositionIteratorType first(input.begin()); + PositionIteratorType iter = first; + PositionIteratorType last(input.end()); + + // Create empty result; + storm::prism::Program result; + + // Create grammar. + storm::parser::prism::PrismGrammar grammar(filename, first); + try { + // Now parse the content using phrase_parse in order to be able to supply a skipping parser. + bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); + LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass."); + if (typeCheck) { + first = PositionIteratorType(input.begin()); + iter = first; + last = PositionIteratorType(input.end()); + grammar.toggleExpressionGeneration(); + succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); + LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in second pass."); + } + } catch (qi::expectation_failure const& e) { + // If the parser expected content different than the one provided, display information about the location of the error. + std::size_t lineNumber = boost::spirit::get_line(e.first); + + // Now propagate exception. + LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << "."); + } + + return result; + } + } // namespace parser +} // namespace storm diff --git a/src/parser/prismparser/PrismParser.h b/src/parser/prismparser/PrismParser.h new file mode 100644 index 000000000..35d2404a6 --- /dev/null +++ b/src/parser/prismparser/PrismParser.h @@ -0,0 +1,36 @@ +#ifndef STORM_PARSER_PRISMPARSER_H_ +#define STORM_PARSER_PRISMPARSER_H_ + +// All classes of the intermediate representation are used. +#include "src/storage/prism/Program.h" + +// Used for file input. +#include + +namespace storm { + namespace parser { + class PrismParser { + public: + /*! + * Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax. + * + * @param filename the name of the file to parse. + * @param typeCheck Sets whether the expressions are generated and therefore typechecked. + * @return The resulting PRISM program. + */ + static storm::prism::Program parse(std::string const& filename, bool typeCheck = true); + + /*! + * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax. + * + * @param input The input string to parse. + * @param filename The name of the file from which the input was read. + * @param typeCheck Sets whether the expressions are generated and therefore typechecked. + * @return The resulting PRISM program. + */ + static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool typeCheck = true); + }; + } // namespace parser +} // namespace storm + +#endif /* STORM_PARSER_PRISMPARSER_H_ */ diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp index 90ba44885..8cc30aa19 100644 --- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp @@ -86,8 +86,8 @@ namespace storm { void BinaryBooleanFunctionExpression::printToStream(std::ostream& stream) const { stream << "(" << *this->getFirstOperand(); switch (this->getOperatorType()) { - case OperatorType::And: stream << " && "; break; - case OperatorType::Or: stream << " || "; break; + case OperatorType::And: stream << " & "; break; + case OperatorType::Or: stream << " | "; break; case OperatorType::Implies: stream << " => "; break; case OperatorType::Iff: stream << " <=> "; break; } diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index b94d98db8..d72a683ac 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -124,6 +124,10 @@ namespace storm { return Expression(std::shared_ptr(new VariableExpression(ExpressionReturnType::Double, variableName))); } + Expression Expression::createUndefinedVariable(std::string const& variableName) { + return Expression(std::shared_ptr(new VariableExpression(ExpressionReturnType::Undefined, variableName))); + } + Expression Expression::createBooleanConstant(std::string const& constantName) { return Expression(std::shared_ptr(new BooleanConstantExpression(constantName))); } diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index e7768432d..47ca6d721 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -33,6 +33,7 @@ namespace storm { static Expression createBooleanVariable(std::string const& variableName); static Expression createIntegerVariable(std::string const& variableName); static Expression createDoubleVariable(std::string const& variableName); + static Expression createUndefinedVariable(std::string const& variableName); static Expression createBooleanConstant(std::string const& constantName); static Expression createIntegerConstant(std::string const& constantName); static Expression createDoubleConstant(std::string const& constantName); diff --git a/src/storage/prism/BooleanVariable.h b/src/storage/prism/BooleanVariable.h index 580a6c33a..d01ebe69d 100644 --- a/src/storage/prism/BooleanVariable.h +++ b/src/storage/prism/BooleanVariable.h @@ -23,7 +23,7 @@ namespace storm { * @param filename The filename in which the variable is defined. * @param lineNumber The line number in which the variable is defined. */ - BooleanVariable(std::string const& variableName, std::string const& filename, uint_fast64_t lineNumber); + BooleanVariable(std::string const& variableName, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a boolean variable with the given name and the given constant initial value expression. @@ -33,7 +33,7 @@ namespace storm { * @param filename The filename in which the variable is defined. * @param lineNumber The line number in which the variable is defined. */ - BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber); + BooleanVariable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); /*! * Creates a copy of the given boolean variable and performs the provided renaming. diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index 038884593..468e0da2b 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -6,14 +6,18 @@ namespace storm { // Nothing to do here. } - Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(oldCommand.getActionName()), guardExpression(oldCommand.getGuardExpression().substitute(renaming)), globalIndex(newGlobalIndex) { + Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, uint_fast64_t newGlobalUpdateIndex, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(oldCommand.getActionName()), guardExpression(oldCommand.getGuardExpression().substitute(renaming)), globalIndex(newGlobalIndex) { + // Rename the action name of the command. auto const& namePair = renaming.find(this->actionName); if (namePair != renaming.end()) { this->actionName = namePair->second; } + + // Rename the updates of the command. this->updates.reserve(oldCommand.getNumberOfUpdates()); for (Update const& update : oldCommand.getUpdates()) { - this->updates.emplace_back(update, update.getGlobalIndex(), renaming, filename, lineNumber); + this->updates.emplace_back(update, newGlobalUpdateIndex, renaming, filename, lineNumber); + ++newGlobalUpdateIndex; } } diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h index 5780c3dce..0173832e8 100644 --- a/src/storage/prism/Command.h +++ b/src/storage/prism/Command.h @@ -29,11 +29,12 @@ namespace storm { * * @param oldCommand The command to copy. * @param newGlobalIndex The global index of the copy of the command. + * @param newGlobalUpdateIndex The global starting index for the updates of the renamed command. * @param renaming A mapping from names that are to be renamed to the names they are to be replaced with. * @param filename The filename in which the command is defined. * @param lineNumber The line number in which the command is defined. */ - Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, uint_fast64_t newGlobalUpdateIndex, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. Command() = default; diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp index 9791d9890..b57bf32d3 100644 --- a/src/storage/prism/Constant.cpp +++ b/src/storage/prism/Constant.cpp @@ -35,8 +35,9 @@ namespace storm { } stream << constant.getConstantName(); if (constant.isDefined()) { - stream << " = " << constant.getExpression() << ";"; + stream << " = " << constant.getExpression(); } + stream << ";"; return stream; } } diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index 47005e6cd..e025a8636 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -23,7 +23,7 @@ namespace storm { } std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable) { - stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << variable.getInitialValueExpression() << ";"; + stream << variable.getName() << ": [" << variable.getLowerBoundExpression() << ".." << variable.getUpperBoundExpression() << "]" << " init " << variable.getInitialValueExpression() << ";"; return stream; } } // namespace prism diff --git a/src/storage/prism/LocatedInformation.cpp b/src/storage/prism/LocatedInformation.cpp index 94d965e94..a5a493319 100644 --- a/src/storage/prism/LocatedInformation.cpp +++ b/src/storage/prism/LocatedInformation.cpp @@ -10,8 +10,16 @@ namespace storm { return this->filename; } + void LocatedInformation::setFilename(std::string const& filename) { + this->filename = filename; + } + uint_fast64_t LocatedInformation::getLineNumber() const { return this->lineNumber; } + + void LocatedInformation::setLineNumber(uint_fast64_t lineNumber) { + this->lineNumber = lineNumber; + } } } \ No newline at end of file diff --git a/src/storage/prism/LocatedInformation.h b/src/storage/prism/LocatedInformation.h index 638734f9f..09921a871 100644 --- a/src/storage/prism/LocatedInformation.h +++ b/src/storage/prism/LocatedInformation.h @@ -29,12 +29,26 @@ namespace storm { */ std::string const& getFilename() const; + /*! + * Sets the filename of this information. + * + * @param filename The new filename of this information. + */ + void setFilename(std::string const& filename); + /*! * Retrieves the line number in which the information was found. * * @return The line number in which the information was found. */ uint_fast64_t getLineNumber() const; + + /*! + * Sets the line number of this information. + * + * @param lineNumber The new line number for this information. + */ + void setLineNumber(uint_fast64_t lineNumber); private: // The file in which the piece of information was found. diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 69abaa2b6..48544efff 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -6,19 +6,18 @@ namespace storm { namespace prism { 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(); + this->createMappings(); } - 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() { + Module::Module(Module const& oldModule, std::string const& newModuleName, uint_fast64_t newGlobalCommandIndex, uint_fast64_t newGlobalUpdateIndex, 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& 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& integerVariable : oldModule.getIntegerVariables()) { auto const& renamingPair = renaming.find(integerVariable.getName()); @@ -26,16 +25,16 @@ namespace storm { 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()) { - this->commands.emplace_back(command, command.getGlobalIndex(), renaming); + this->commands.emplace_back(command, newGlobalCommandIndex, newGlobalUpdateIndex, renaming, filename, lineNumber); + ++newGlobalCommandIndex; + newGlobalUpdateIndex += this->commands.back().getNumberOfUpdates(); } - // Finally, update internal mapping. - this->collectActions(); + // Finally, update internal mappings. + this->createMappings(); } std::size_t Module::getNumberOfBooleanVariables() const { @@ -108,18 +107,28 @@ namespace storm { LOG_THROW(false, storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist in module."); } - void Module::collectActions() { - // Clear the current mapping. + void Module::createMappings() { + // Clear the current mappings. this->actionsToCommandIndexMap.clear(); + this->booleanVariableToIndexMap.clear(); + this->integerVariableToIndexMap.clear(); + + // Create the mappings for the variables. + for (uint_fast64_t i = 0; i < this->booleanVariables.size(); ++i) { + this->booleanVariableToIndexMap[this->getBooleanVariables()[i].getName()] = i; + } + for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) { + this->integerVariableToIndexMap[this->getIntegerVariables()[i].getName()] = i; + } // Add the mapping for all commands. - for (unsigned int id = 0; id < this->commands.size(); id++) { - std::string const& action = this->commands[id].getActionName(); + for (uint_fast64_t i = 0; i < this->commands.size(); i++) { + std::string const& action = this->commands[i].getActionName(); if (action != "") { if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) { this->actionsToCommandIndexMap.emplace(action, std::set()); } - this->actionsToCommandIndexMap[action].insert(id); + this->actionsToCommandIndexMap[action].insert(i); this->actions.insert(action); } } diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index cb62bc626..4a1608d22 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -34,11 +34,13 @@ namespace storm { * * @param oldModule The module to be copied. * @param newModuleName The name of the new module. + * @param newGlobalCommandIndex The global starting index for commands of the renamed module. + * @param newGlobalUpdateIndex The global starting index for the updates of the renamed module. * @param renaming A mapping of identifiers to the new identifiers they are to be replaced with. * @param filename The filename in which the module is defined. * @param lineNumber The line number in which the module is defined. */ - Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Module(Module const& oldModule, std::string const& newModuleName, uint_fast64_t newGlobalCommandIndex, uint_fast64_t newGlobalUpdateIndex, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. Module() = default; @@ -164,7 +166,7 @@ namespace storm { /*! * Computes the locally maintained mappings for fast data retrieval. */ - void collectActions(); + void createMappings(); // The name of the module. std::string moduleName; diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 281be2531..98bb75a1a 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -5,29 +5,8 @@ namespace storm { namespace prism { - 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