diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp new file mode 100644 index 000000000..71843541b --- /dev/null +++ b/src/parser/PrismParser.cpp @@ -0,0 +1,636 @@ +#include "src/parser/PrismParser.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/WrongFormatException.h" + +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::PrismParser 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.moveToSecondRun(); + 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; + } + + PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), allowDoubleLiteralsFlag(true), filename(filename), annotate(first) { + // Parse simple identifier. + identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; + identifier.name("identifier"); + + 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(&PrismParser::createFloorExpression, phoenix::ref(*this), qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createCeilExpression, phoenix::ref(*this), 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(&PrismParser::createMinimumExpression, phoenix::ref(*this), qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&PrismParser::createMaximumExpression, phoenix::ref(*this), qi::_1, qi::_2)]]; + minMaxExpression.name("min/max expression"); + + identifierExpression = identifier[qi::_val = phoenix::bind(&PrismParser::getIdentifierExpression, phoenix::ref(*this), qi::_1)]; + identifierExpression.name("identifier expression"); + + literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&PrismParser::createTrueExpression, phoenix::ref(*this))] | qi::lit("false")[qi::_val = phoenix::bind(&PrismParser::createFalseExpression, phoenix::ref(*this))] | strict_double[qi::_val = phoenix::bind(&PrismParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&PrismParser::createIntegerLiteralExpression, phoenix::ref(*this), 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 = phoenix::bind(&PrismParser::createNotExpression, phoenix::ref(*this), qi::_1)] | (qi::lit("-") >> atomicExpression)[qi::_val = phoenix::bind(&PrismParser::createMinusExpression, phoenix::ref(*this), 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 = phoenix::bind(&PrismParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createDivExpression, phoenix::ref(*this), 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 = phoenix::bind(&PrismParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]]; + plusExpression.name("plus expression"); + + relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("!=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1]; + relativeExpression.name("relative expression"); + + andExpression = relativeExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> relativeExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)]; + andExpression.name("and expression"); + + orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)]; + orExpression.name("or expression"); + + iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&PrismParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; + iteExpression.name("if-then-else expression"); + + expression %= iteExpression; + expression.name("expression"); + + modelTypeDefinition %= modelType_; + modelTypeDefinition.name("model type"); + + undefinedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedBooleanConstant, phoenix::ref(*this), qi::_1)]; + undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); + + undefinedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedIntegerConstant, phoenix::ref(*this), qi::_1)]; + undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); + + undefinedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double")) > identifier > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedDoubleConstant, phoenix::ref(*this), qi::_1)]; + undefinedDoubleConstantDefinition.name("undefined double 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::_val = phoenix::bind(&PrismParser::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::_val = phoenix::bind(&PrismParser::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::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)]; + definedDoubleConstantDefinition.name("defined double constant declaration"); + + definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); + definedConstantDefinition.name("defined constant definition"); + + formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + formulaDefinition.name("formula definition"); + + booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expression) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)]; + booleanVariableDefinition.name("boolean variable definition"); + + integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expression[qi::_a = qi::_1] > qi::lit("..") > expression > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::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] + > *(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"); + + stateRewardDefinition = (expression > qi::lit(":") > plusExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)]; + stateRewardDefinition.name("state reward definition"); + + transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit(":") > plusExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3)]; + transitionRewardDefinition.name("transition reward definition"); + + 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(&PrismParser::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(&PrismParser::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(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)]; + labelDefinition.name("label definition"); + + assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)]; + assignmentDefinition.name("assignment"); + + assignmentDefinitionList %= +assignmentDefinition % "&"; + assignmentDefinitionList.name("assignment list"); + + updateDefinition = (((plusExpression > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; + updateDefinition.name("update"); + + updateListDefinition %= +updateDefinition(qi::_r1) % "+"; + updateListDefinition.name("update list"); + + commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)]; + commandDefinition.name("command definition"); + + moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::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("[") + > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] % ",") > qi::lit("]") + > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createRenamedModule, phoenix::ref(*this), qi::_1, qi::_2, qi::_a, qi::_r1)]; + moduleRenaming.name("module definition via renaming"); + + 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)] | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, qi::_a), qi::_1)]) > qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)]; + start.name("probabilistic program"); + + // Enable error reporting. + qi::on_error(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(iteExpression, 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)); + + // 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 PrismParser::moveToSecondRun() { + this->secondRun = true; + } + + void PrismParser::allowDoubleLiterals(bool flag) { + this->allowDoubleLiteralsFlag = flag; + } + + std::string const& PrismParser::getFilename() const { + return this->filename; + } + + bool PrismParser::isValidIdentifier(std::string const& identifier) { + if (this->keywords_.find(identifier) != nullptr) { + return false; + } + return true; + } + + bool PrismParser::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 PrismParser::createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1.ite(e2, e3); + } + } + + storm::expressions::Expression PrismParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 || e2; + } + } + + storm::expressions::Expression PrismParser::createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 && e2; + } + } + + storm::expressions::Expression PrismParser::createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 > e2; + } + } + + storm::expressions::Expression PrismParser::createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 >= e2; + } + } + + storm::expressions::Expression PrismParser::createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 < e2; + } + } + + storm::expressions::Expression PrismParser::createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 <= e2; + } + } + + storm::expressions::Expression PrismParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 == e2; + } + } + + storm::expressions::Expression PrismParser::createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 != e2; + } + } + + storm::expressions::Expression PrismParser::createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 + e2; + } + } + + storm::expressions::Expression PrismParser::createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 - e2; + } + } + + storm::expressions::Expression PrismParser::createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 * e2; + } + } + + storm::expressions::Expression PrismParser::createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1 / e2; + } + } + + storm::expressions::Expression PrismParser::createNotExpression(storm::expressions::Expression e1) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return !e1; + } + } + + storm::expressions::Expression PrismParser::createMinusExpression(storm::expressions::Expression e1) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return -e1; + } + } + + storm::expressions::Expression PrismParser::createTrueExpression() const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return storm::expressions::Expression::createTrue(); + } + } + + storm::expressions::Expression PrismParser::createFalseExpression() const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return storm::expressions::Expression::createFalse(); + } + } + + storm::expressions::Expression PrismParser::createDoubleLiteralExpression(double value, bool& pass) const { + // If we are not supposed to accept double expressions, we reject it by setting pass to false. + if (!this->allowDoubleLiteralsFlag) { + pass = false; + } + + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return storm::expressions::Expression::createDoubleLiteral(value); + } + } + + storm::expressions::Expression PrismParser::createIntegerLiteralExpression(int value) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return storm::expressions::Expression::createIntegerLiteral(static_cast(value)); + } + } + + storm::expressions::Expression PrismParser::createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return storm::expressions::Expression::minimum(e1, e2); + } + } + + storm::expressions::Expression PrismParser::createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return storm::expressions::Expression::maximum(e1, e2); + } + } + + storm::expressions::Expression PrismParser::createFloorExpression(storm::expressions::Expression e1) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1.floor(); + } + } + + storm::expressions::Expression PrismParser::createCeilExpression(storm::expressions::Expression e1) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + return e1.ceil(); + } + } + + storm::expressions::Expression PrismParser::getIdentifierExpression(std::string const& identifier) const { + if (!this->secondRun) { + return storm::expressions::Expression::createFalse(); + } else { + storm::expressions::Expression const* expression = this->identifiers_.find(identifier); + LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Undeclared identifier '" << identifier << "'."); + return *expression; + } + } + + storm::prism::Constant PrismParser::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 PrismParser::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 PrismParser::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 PrismParser::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 PrismParser::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 PrismParser::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 PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const { + if (this->secondRun) { + this->identifiers_.add(formulaName, expression); + } + return storm::prism::Formula(formulaName, expression, this->getFilename()); + } + + storm::prism::Label PrismParser::createLabel(std::string const& labelName, storm::expressions::Expression expression) const { + return storm::prism::Label(labelName, expression, this->getFilename()); + } + + storm::prism::RewardModel PrismParser::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 PrismParser::createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const { + return storm::prism::StateReward(statePredicateExpression, rewardValueExpression, this->getFilename()); + } + + storm::prism::TransitionReward PrismParser::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 PrismParser::createAssignment(std::string const& variableName, storm::expressions::Expression assignedExpression) const { + return storm::prism::Assignment(variableName, assignedExpression, this->getFilename()); + } + + storm::prism::Update PrismParser::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 PrismParser::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 PrismParser::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 PrismParser::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 PrismParser::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 PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const { + // Check whether the module to rename actually exists. + auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName); + LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "No module named '" << oldModuleName << "' to rename."); + storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second]; + + if (!this->secondRun) { + // Register all (renamed) variables for later use. + for (auto const& variable : moduleToRename.getBooleanVariables()) { + auto const& renamingPair = renaming.find(variable.getName()); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed."); + this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createBooleanVariable(renamingPair->second)); + } + for (auto const& variable : moduleToRename.getIntegerVariables()) { + auto const& renamingPair = renaming.find(variable.getName()); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed."); + this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createIntegerVariable(renamingPair->second)); + } + + // Return a dummy module in the first pass. + return storm::prism::Module(); + } else { + // Add a mapping from the new module name to its (future) index. + globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size(); + + // Create a mapping from identifiers to the expressions they need to be replaced with. + std::map expressionRenaming; + for (auto const& namePair : renaming) { + storm::expressions::Expression const* substitutedExpression = this->identifiers_.find(namePair.second); + // If the mapped-to-value is an expression, we need to replace it. + if (substitutedExpression != nullptr) { + expressionRenaming.emplace(namePair.first, *substitutedExpression); + } + } + + // Rename the boolean variables. + std::vector booleanVariables; + for (auto const& variable : moduleToRename.getBooleanVariables()) { + auto const& renamingPair = renaming.find(variable.getName()); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed."); + + booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + } + + // Rename the integer variables. + std::vector integerVariables; + for (auto const& variable : moduleToRename.getIntegerVariables()) { + auto const& renamingPair = renaming.find(variable.getName()); + LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed."); + + integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1))); + } + + // Rename commands. + std::vector commands; + for (auto const& command : moduleToRename.getCommands()) { + std::vector updates; + for (auto const& update : command.getUpdates()) { + std::vector assignments; + for (auto const& assignment : update.getAssignments()) { + auto const& renamingPair = renaming.find(assignment.getVariableName()); + if (renamingPair != renaming.end()) { + assignments.emplace_back(renamingPair->second, assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); + } else { + assignments.emplace_back(assignment.getVariableName(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); + } + } + updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1)); + ++globalProgramInformation.currentUpdateIndex; + } + + std::string newActionName = command.getActionName(); + auto const& renamingPair = renaming.find(command.getActionName()); + if (renamingPair != renaming.end()) { + newActionName = renamingPair->second; + } + + commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); + ++globalProgramInformation.currentCommandIndex; + } + + return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, this->getFilename()); + } + } + + storm::prism::Program PrismParser::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 parser +} // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h new file mode 100644 index 000000000..e271b2298 --- /dev/null +++ b/src/parser/PrismParser.h @@ -0,0 +1,320 @@ +#ifndef STORM_PARSER_PRISMPARSER_H_ +#define STORM_PARSER_PRISMPARSER_H_ + +// Include files for file input. +#include +#include +#include + +// Include boost spirit. +#define BOOST_SPIRIT_USE_PHOENIX_V3 +#include +#include +#include +#include +#include + +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + +typedef std::string::const_iterator BaseIteratorType; +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; + +#include "src/storage/prism/Program.h" +#include "src/storage/expressions/Expression.h" +#include "src/exceptions/ExceptionMacros.h" + +namespace storm { + namespace parser { + class GlobalProgramInformation { + public: + // Default construct the header information. + GlobalProgramInformation() = default; + + // Members for all essential information that needs to be collected. + storm::prism::Program::ModelType modelType; + 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; + }; + + class PrismParser : public qi::grammar, Skipper> { + 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); + + private: + 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) + ("min", 14) + ("max", 15) + ("floor", 16) + ("ceil", 17) + ("init", 18) + ("endinit", 19); + } + }; + + // 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; + }; + + /*! + * 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. + */ + PrismParser(std::string const& filename, Iterator first); + + /*! + * Sets an internal flag that indicates the second run is now taking place. + */ + void moveToSecondRun(); + + // A flag that stores whether the grammar is currently doing the second run. + bool secondRun; + + /*! + * 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); + + // A flag that stores wether to allow or forbid double literals in parsed expressions. + bool allowDoubleLiteralsFlag; + + // 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; + + // Rules for model type. + qi::rule modelTypeDefinition; + + // 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; + + // Rules for global variable definitions. + qi::rule globalVariableDefinition; + qi::rule globalBooleanVariableDefinition; + qi::rule globalIntegerVariableDefinition; + + // Rules for modules definition. + qi::rule(GlobalProgramInformation&), Skipper> moduleDefinitionList; + qi::rule, std::vector>, Skipper> moduleDefinition; + qi::rule>, Skipper> moduleRenaming; + + // Rules for variable definitions. + qi::rule&, std::vector&), Skipper> variableDefinition; + qi::rule booleanVariableDefinition; + qi::rule, Skipper> integerVariableDefinition; + + // Rules for command definitions. + 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 stateRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; + + // Rules for initial states expression. + qi::rule initialStatesConstruct; + + // Rules for label definitions. + qi::rule labelDefinition; + + // Rules for formula definitions. + qi::rule formulaDefinition; + + // Rules for identifier parsing. + qi::rule identifier; + + // Rules for parsing a composed expression. + qi::rule expression; + qi::rule iteExpression; + qi::rule orExpression; + qi::rule andExpression; + qi::rule relativeExpression; + qi::rule, Skipper> plusExpression; + 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::PrismParser::keywordsStruct keywords_; + storm::parser::PrismParser::modelTypeStruct modelType_; + qi::symbols identifiers_; + + // Helper methods used in the grammar. + bool isValidIdentifier(std::string const& identifier); + bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); + + storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const; + storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createNotExpression(storm::expressions::Expression e1) const; + storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1) const; + storm::expressions::Expression createTrueExpression() const; + storm::expressions::Expression createFalseExpression() const; + storm::expressions::Expression createDoubleLiteralExpression(double value, bool& pass) const; + storm::expressions::Expression createIntegerLiteralExpression(int value) const; + storm::expressions::Expression createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; + storm::expressions::Expression createFloorExpression(storm::expressions::Expression e1) const; + storm::expressions::Expression createCeilExpression(storm::expressions::Expression e1) const; + 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 parser +} // namespace storm + +#endif /* STORM_PARSER_PRISMPARSER_H_ */ + diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp deleted file mode 100644 index b8c06daa9..000000000 --- a/src/parser/prismparser/PrismGrammar.cpp +++ /dev/null @@ -1,373 +0,0 @@ -// #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(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_('_')))]]][qi::_pass = phoenix::bind(&PrismGrammar::isValidIdentifier, phoenix::ref(*this), qi::_1)]; - identifier.name("identifier"); - - setExpressionGeneration(doExpressionGeneration); - - modelTypeDefinition %= modelType_; - modelTypeDefinition.name("model type"); - - 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::_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::_val = phoenix::bind(&PrismGrammar::createUndefinedDoubleConstant, phoenix::ref(*this), qi::_1)]; - undefinedDoubleConstantDefinition.name("undefined double 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::_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::_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::_val = phoenix::bind(&PrismGrammar::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)]; - definedDoubleConstantDefinition.name("defined double constant declaration"); - - 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"); - - 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] - > *(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"); - - 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("]") > 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"); - - 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::_val = phoenix::bind(&PrismGrammar::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)]; - assignmentDefinition.name("assignment"); - - assignmentDefinitionList %= +assignmentDefinition % "&"; - assignmentDefinitionList.name("assignment list"); - - 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(qi::_r1) % "+"; - updateListDefinition.name("update list"); - - 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"); - - 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("[") - > ((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, phoenix::ref(*this), qi::_1, qi::_2, qi::_a, qi::_r1)]; - moduleRenaming.name("module definition via renaming"); - - 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 -} // namespace storm diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h deleted file mode 100644 index 29d0afb96..000000000 --- a/src/parser/prismparser/PrismGrammar.h +++ /dev/null @@ -1,282 +0,0 @@ -#ifndef STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_ -#define STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_ - -// Include files for file input. -#include -#include -#include - -// Include boost spirit. -#define BOOST_SPIRIT_USE_PHOENIX_V3 -#include -#include -#include -#include -#include - -namespace qi = boost::spirit::qi; -namespace phoenix = boost::phoenix; - -typedef std::string::const_iterator BaseIteratorType; -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; - -#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 - ("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) - ("min", 14) - ("max", 15) - ("floor", 16) - ("ceil", 17) - ("init", 18) - ("endinit", 19); - } - }; - - class GlobalProgramInformation { - public: - // Default construct the header information. - GlobalProgramInformation() = default; - - // Members for all essential information that needs to be collected. - storm::prism::Program::ModelType modelType; - 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: - /*! - * 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. - */ - 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; - - // Rules for model type. - qi::rule modelTypeDefinition; - - // 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; - - // Rules for global variable definitions. - qi::rule globalVariableDefinition; - qi::rule globalBooleanVariableDefinition; - qi::rule globalIntegerVariableDefinition; - - // Rules for modules definition. - qi::rule(GlobalProgramInformation&), Skipper> moduleDefinitionList; - qi::rule, std::vector>, Skipper> moduleDefinition; - qi::rule>, Skipper> moduleRenaming; - - // Rules for variable definitions. - qi::rule&, std::vector&), Skipper> variableDefinition; - qi::rule booleanVariableDefinition; - qi::rule, Skipper> integerVariableDefinition; - - // Rules for command definitions. - 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 stateRewardDefinition; - qi::rule, Skipper> transitionRewardDefinition; - - // Rules for initial states expression. - qi::rule initialStatesConstruct; - - // Rules for label definitions. - qi::rule labelDefinition; - - // Rules for formula definitions. - qi::rule formulaDefinition; - - // Rules for identifier parsing. - qi::rule identifier; - - // Rules for parsing a composed expression. - qi::rule expression; - qi::rule orExpression; - qi::rule andExpression; - qi::rule relativeExpression; - qi::rule, Skipper> plusExpression; - 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 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 -} // namespace storm - - -#endif /* STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_ */ - diff --git a/src/parser/prismparser/PrismParser.cpp b/src/parser/prismparser/PrismParser.cpp deleted file mode 100644 index a261ba8cc..000000000 --- a/src/parser/prismparser/PrismParser.cpp +++ /dev/null @@ -1,70 +0,0 @@ -#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 deleted file mode 100644 index 35d2404a6..000000000 --- a/src/parser/prismparser/PrismParser.h +++ /dev/null @@ -1,36 +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 { - 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/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index 200b8ac0f..f66cd7dc3 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/src/storage/expressions/BaseExpression.cpp @@ -52,6 +52,11 @@ namespace storm { return this->shared_from_this(); } + std::ostream& operator<<(std::ostream& stream, ExpressionReturnType const& enumValue) { + stream << static_cast::type>(enumValue); + return stream; + } + std::ostream& operator<<(std::ostream& stream, BaseExpression const& expression) { expression.printToStream(stream); return stream; diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h index 7ca9e63ad..4039209d3 100644 --- a/src/storage/expressions/BaseExpression.h +++ b/src/storage/expressions/BaseExpression.h @@ -17,6 +17,8 @@ namespace storm { */ enum class ExpressionReturnType {Undefined, Bool, Int, Double}; + std::ostream& operator<<(std::ostream& stream, ExpressionReturnType const& enumValue); + /*! * The base class of all expression classes. */ diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp index d72a683ac..7da4f8b37 100644 --- a/src/storage/expressions/Expression.cpp +++ b/src/storage/expressions/Expression.cpp @@ -7,6 +7,7 @@ #include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/ExceptionMacros.h" +#include "src/storage/expressions/IfThenElseExpression.h" #include "src/storage/expressions/BinaryBooleanFunctionExpression.h" #include "src/storage/expressions/BinaryNumericalFunctionExpression.h" #include "src/storage/expressions/BinaryRelationExpression.h" @@ -220,6 +221,12 @@ namespace storm { return Expression(std::shared_ptr(new BinaryNumericalFunctionExpression(lhs.getReturnType() == ExpressionReturnType::Int && rhs.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double, lhs.getBaseExpressionPointer(), rhs.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Max))); } + Expression Expression::ite(Expression const& thenExpression, Expression const& elseExpression) { + LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Condition of if-then-else operator must be of boolean type."); + LOG_THROW(thenExpression.hasBooleanReturnType() && elseExpression.hasBooleanReturnType() || thenExpression.hasNumericalReturnType() && elseExpression.hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "'then' and 'else' expression of if-then-else operator must have equal return type."); + return Expression(std::shared_ptr(new IfThenElseExpression(thenExpression.hasBooleanReturnType() && elseExpression.hasBooleanReturnType() ? ExpressionReturnType::Bool : (thenExpression.getReturnType() == ExpressionReturnType::Int && elseExpression.getReturnType() == ExpressionReturnType::Int ? ExpressionReturnType::Int : ExpressionReturnType::Double), this->getBaseExpressionPointer(), thenExpression.getBaseExpressionPointer(), elseExpression.getBaseExpressionPointer()))); + } + Expression Expression::implies(Expression const& other) const { LOG_THROW(this->hasBooleanReturnType() && other.hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Operator '&&' requires boolean operands."); return Expression(std::shared_ptr(new BinaryBooleanFunctionExpression(ExpressionReturnType::Bool, this->getBaseExpressionPointer(), other.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::Implies))); diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h index 47ca6d721..96f8ce6fd 100644 --- a/src/storage/expressions/Expression.h +++ b/src/storage/expressions/Expression.h @@ -54,6 +54,7 @@ namespace storm { Expression operator<(Expression const& other) const; Expression operator<=(Expression const& other) const; + Expression ite(Expression const& thenExpression, Expression const& elseExpression); Expression implies(Expression const& other) const; Expression iff(Expression const& other) const; diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h index 8e6dca24e..928e6297c 100644 --- a/src/storage/expressions/ExpressionVisitor.h +++ b/src/storage/expressions/ExpressionVisitor.h @@ -4,6 +4,7 @@ namespace storm { namespace expressions { // Forward-declare all expression classes. + class IfThenElseExpression; class BinaryBooleanFunctionExpression; class BinaryNumericalFunctionExpression; class BinaryRelationExpression; @@ -20,6 +21,7 @@ namespace storm { class ExpressionVisitor { public: + virtual void visit(IfThenElseExpression const* expression) = 0; virtual void visit(BinaryBooleanFunctionExpression const* expression) = 0; virtual void visit(BinaryNumericalFunctionExpression const* expression) = 0; virtual void visit(BinaryRelationExpression const* expression) = 0; diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp index e753583f9..17161775a 100644 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.cpp +++ b/src/storage/expressions/IdentifierSubstitutionVisitor.cpp @@ -3,6 +3,7 @@ #include "src/storage/expressions/IdentifierSubstitutionVisitor.h" +#include "src/storage/expressions/IfThenElseExpression.h" #include "src/storage/expressions/BinaryBooleanFunctionExpression.h" #include "src/storage/expressions/BinaryNumericalFunctionExpression.h" #include "src/storage/expressions/BinaryRelationExpression.h" @@ -29,6 +30,28 @@ namespace storm { return Expression(this->expressionStack.top()); } + template class MapType> + void IdentifierSubstitutionVisitor::visit(IfThenElseExpression const* expression) { + expression->getCondition()->accept(this); + std::shared_ptr conditionExpression = expressionStack.top(); + expressionStack.pop(); + + expression->getThenExpression()->accept(this); + std::shared_ptr thenExpression = expressionStack.top(); + expressionStack.pop(); + + expression->getElseExpression()->accept(this); + std::shared_ptr elseExpression = expressionStack.top(); + expressionStack.pop(); + + // If the arguments did not change, we simply push the expression itself. + if (conditionExpression.get() == expression->getCondition().get() && thenExpression.get() == expression->getThenExpression().get() && elseExpression.get() == expression->getElseExpression().get()) { + this->expressionStack.push(expression->getSharedPointer()); + } else { + this->expressionStack.push(std::shared_ptr(new IfThenElseExpression(expression->getReturnType(), conditionExpression, thenExpression, elseExpression))); + } + } + template class MapType> void IdentifierSubstitutionVisitor::visit(BinaryBooleanFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); diff --git a/src/storage/expressions/IdentifierSubstitutionVisitor.h b/src/storage/expressions/IdentifierSubstitutionVisitor.h index 87976122c..6be7aa9ca 100644 --- a/src/storage/expressions/IdentifierSubstitutionVisitor.h +++ b/src/storage/expressions/IdentifierSubstitutionVisitor.h @@ -28,6 +28,7 @@ namespace storm { */ Expression substitute(BaseExpression const* expression); + virtual void visit(IfThenElseExpression const* expression) override; virtual void visit(BinaryBooleanFunctionExpression const* expression) override; virtual void visit(BinaryNumericalFunctionExpression const* expression) override; virtual void visit(BinaryRelationExpression const* expression) override; diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp new file mode 100644 index 000000000..dffee088d --- /dev/null +++ b/src/storage/expressions/IfThenElseExpression.cpp @@ -0,0 +1,96 @@ +#include "src/storage/expressions/IfThenElseExpression.h" + +namespace storm { + namespace expressions { + IfThenElseExpression::IfThenElseExpression(ExpressionReturnType returnType, std::shared_ptr const& condition, std::shared_ptr const& thenExpression, std::shared_ptr const& elseExpression) : BaseExpression(returnType), condition(condition), thenExpression(thenExpression), elseExpression(elseExpression) { + // Intentionally left empty. + } + + bool IfThenElseExpression::evaluateAsBool(Valuation const& valuation) const { + bool conditionValue = this->condition->evaluateAsBool(valuation); + if (conditionValue) { + return this->thenExpression->evaluateAsBool(valuation); + } else { + return this->elseExpression->evaluateAsBool(valuation); + } + } + + int_fast64_t IfThenElseExpression::evaluateAsInt(Valuation const& valuation) const { + bool conditionValue = this->condition->evaluateAsBool(valuation); + if (conditionValue) { + return this->thenExpression->evaluateAsInt(valuation); + } else { + return this->elseExpression->evaluateAsInt(valuation); + } + } + + double IfThenElseExpression::evaluateAsDouble(Valuation const& valuation) const { + bool conditionValue = this->condition->evaluateAsBool(valuation); + if (conditionValue) { + return this->thenExpression->evaluateAsDouble(valuation); + } else { + return this->elseExpression->evaluateAsDouble(valuation); + } + } + + bool IfThenElseExpression::isConstant() const { + return this->condition->isConstant() && this->thenExpression->isConstant() && this->elseExpression->isConstant(); + } + + std::set IfThenElseExpression::getVariables() const { + std::set result = this->condition->getVariables(); + std::set tmp = this->thenExpression->getVariables(); + result.insert(tmp.begin(), tmp.end()); + tmp = this->elseExpression->getVariables(); + result.insert(tmp.begin(), tmp.end()); + return result; + } + + std::set IfThenElseExpression::getConstants() const { + std::set result = this->condition->getConstants(); + std::set tmp = this->thenExpression->getConstants(); + result.insert(tmp.begin(), tmp.end()); + tmp = this->elseExpression->getConstants(); + result.insert(tmp.begin(), tmp.end()); + return result; + } + + std::shared_ptr IfThenElseExpression::simplify() const { + std::shared_ptr conditionSimplified; + if (conditionSimplified->isTrue()) { + return this->thenExpression->simplify(); + } else if (conditionSimplified->isFalse()) { + return this->elseExpression->simplify(); + } else { + std::shared_ptr thenExpressionSimplified = this->thenExpression->simplify(); + std::shared_ptr elseExpressionSimplified = this->elseExpression->simplify(); + + if (conditionSimplified.get() == this->condition.get() && thenExpressionSimplified.get() == this->thenExpression.get() && elseExpressionSimplified.get() == this->elseExpression.get()) { + return this->shared_from_this(); + } else { + return std::shared_ptr(new IfThenElseExpression(this->getReturnType(), conditionSimplified, thenExpressionSimplified, elseExpressionSimplified)); + } + } + } + + void IfThenElseExpression::accept(ExpressionVisitor* visitor) const { + visitor->visit(this); + } + + std::shared_ptr IfThenElseExpression::getCondition() const { + return this->condition; + } + + std::shared_ptr IfThenElseExpression::getThenExpression() const { + return this->thenExpression; + } + + std::shared_ptr IfThenElseExpression::getElseExpression() const { + return this->elseExpression; + } + + void IfThenElseExpression::printToStream(std::ostream& stream) const { + stream << "(" << *this->condition << " ? " << *this->thenExpression << " : " << *this->elseExpression << ")"; + } + } +} \ No newline at end of file diff --git a/src/storage/expressions/IfThenElseExpression.h b/src/storage/expressions/IfThenElseExpression.h new file mode 100644 index 000000000..794a75bee --- /dev/null +++ b/src/storage/expressions/IfThenElseExpression.h @@ -0,0 +1,74 @@ +#ifndef STORM_STORAGE_EXPRESSIONS_IFTHENELSEEXPRESSION_H_ +#define STORM_STORAGE_EXPRESSIONS_IFTHENELSEEXPRESSION_H_ + +#include "src/storage/expressions/BaseExpression.h" + +namespace storm { + namespace expressions { + class IfThenElseExpression : public BaseExpression { + public: + /*! + * Creates an if-then-else expression with the given return type, condition and operands. + * + * @param returnType The return type of the expression. + * @param thenExpression The expression evaluated if the condition evaluates true. + * @param elseExpression The expression evaluated if the condition evaluates false. + */ + IfThenElseExpression(ExpressionReturnType returnType, std::shared_ptr const& condition, std::shared_ptr const& thenExpression, std::shared_ptr const& elseExpression); + + // Instantiate constructors and assignments with their default implementations. + IfThenElseExpression(IfThenElseExpression const& other) = default; + IfThenElseExpression& operator=(IfThenElseExpression const& other) = default; + IfThenElseExpression(IfThenElseExpression&&) = default; + IfThenElseExpression& operator=(IfThenElseExpression&&) = default; + virtual ~IfThenElseExpression() = default; + + // Override base class methods. + virtual bool evaluateAsBool(Valuation const& valuation) const override; + virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override; + virtual double evaluateAsDouble(Valuation const& valuation) const override; + virtual bool isConstant() const override; + virtual std::set getVariables() const override; + virtual std::set getConstants() const override; + virtual std::shared_ptr simplify() const override; + virtual void accept(ExpressionVisitor* visitor) const override; + + /*! + * Retrieves the condition expression of the if-then-else expression. + * + * @return The condition expression of the if-then-else expression. + */ + std::shared_ptr getCondition() const; + + /*! + * Retrieves the then expression of the if-then-else expression. + * + * @return The then expression of the if-then-else expression. + */ + std::shared_ptr getThenExpression() const; + + /*! + * Retrieves the else expression of the if-then-else expression. + * + * @return The else expression of the if-then-else expression. + */ + std::shared_ptr getElseExpression() const; + + protected: + // Override base class method. + virtual void printToStream(std::ostream& stream) const override; + + private: + // The condition of the if-then-else. + std::shared_ptr condition; + + // The return expression of the if-part. + std::shared_ptr thenExpression; + + // The return expression of the else-part. + std::shared_ptr elseExpression; + }; + } +} + +#endif /* STORM_STORAGE_EXPRESSIONS_IFTHENELSEEXPRESSION_H_ */ \ No newline at end of file diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index 878d06036..c3f2ea0a8 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -3,6 +3,7 @@ #include "src/storage/expressions/SubstitutionVisitor.h" +#include "src/storage/expressions/IfThenElseExpression.h" #include "src/storage/expressions/BinaryBooleanFunctionExpression.h" #include "src/storage/expressions/BinaryNumericalFunctionExpression.h" #include "src/storage/expressions/BinaryRelationExpression.h" @@ -29,6 +30,28 @@ namespace storm { return Expression(this->expressionStack.top()); } + template class MapType> + void SubstitutionVisitor::visit(IfThenElseExpression const* expression) { + expression->getCondition()->accept(this); + std::shared_ptr conditionExpression = expressionStack.top(); + expressionStack.pop(); + + expression->getThenExpression()->accept(this); + std::shared_ptr thenExpression = expressionStack.top(); + expressionStack.pop(); + + expression->getElseExpression()->accept(this); + std::shared_ptr elseExpression = expressionStack.top(); + expressionStack.pop(); + + // If the arguments did not change, we simply push the expression itself. + if (conditionExpression.get() == expression->getCondition().get() && thenExpression.get() == expression->getThenExpression().get() && elseExpression.get() == expression->getElseExpression().get()) { + this->expressionStack.push(expression->getSharedPointer()); + } else { + this->expressionStack.push(std::shared_ptr(new IfThenElseExpression(expression->getReturnType(), conditionExpression, thenExpression, elseExpression))); + } + } + template class MapType> void SubstitutionVisitor::visit(BinaryBooleanFunctionExpression const* expression) { expression->getFirstOperand()->accept(this); diff --git a/src/storage/expressions/SubstitutionVisitor.h b/src/storage/expressions/SubstitutionVisitor.h index 4c3abc1e7..ad29ad6ab 100644 --- a/src/storage/expressions/SubstitutionVisitor.h +++ b/src/storage/expressions/SubstitutionVisitor.h @@ -28,6 +28,7 @@ namespace storm { */ Expression substitute(BaseExpression const* expression); + virtual void visit(IfThenElseExpression const* expression) override; virtual void visit(BinaryBooleanFunctionExpression const* expression) override; virtual void visit(BinaryNumericalFunctionExpression const* expression) override; virtual void visit(BinaryRelationExpression const* expression) override; diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp index 2c639a535..d556f6332 100644 --- a/src/storage/prism/Assignment.cpp +++ b/src/storage/prism/Assignment.cpp @@ -6,13 +6,6 @@ namespace storm { // Intentionally left empty. } - Assignment::Assignment(Assignment const& oldAssignment, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(oldAssignment.getVariableName()), expression(oldAssignment.getExpression().substitute(renaming)) { - auto renamingPair = renaming.find(oldAssignment.variableName); - if (renamingPair != renaming.end()) { - this->variableName = renamingPair->second; - } - } - std::string const& Assignment::getVariableName() const { return variableName; } diff --git a/src/storage/prism/Assignment.h b/src/storage/prism/Assignment.h index 955c8417e..2d4629e31 100644 --- a/src/storage/prism/Assignment.h +++ b/src/storage/prism/Assignment.h @@ -19,17 +19,7 @@ namespace storm { * @param lineNumber The line number in which the assignment is defined. */ Assignment(std::string const& variableName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0); - - /*! - * Creates a copy of the given assignment and performs the provided renaming. - * - * @param oldAssignment The assignment to copy. - * @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 assignment is defined. - * @param lineNumber The line number in which the assignment is defined. - */ - Assignment(Assignment const& oldAssignment, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); - + // Create default implementations of constructors/assignment. Assignment() = default; Assignment(Assignment const& other) = default; diff --git a/src/storage/prism/BooleanVariable.cpp b/src/storage/prism/BooleanVariable.cpp index 0ce68d34d..c746e698d 100644 --- a/src/storage/prism/BooleanVariable.cpp +++ b/src/storage/prism/BooleanVariable.cpp @@ -10,10 +10,6 @@ namespace storm { // Nothing to do here. } - BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : Variable(oldVariable, newName, renaming, filename, lineNumber) { - // Nothing to do here. - } - std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable) { stream << variable.getName() << ": bool " << variable.getInitialValueExpression() << ";"; return stream; diff --git a/src/storage/prism/BooleanVariable.h b/src/storage/prism/BooleanVariable.h index d01ebe69d..d52b8d0aa 100644 --- a/src/storage/prism/BooleanVariable.h +++ b/src/storage/prism/BooleanVariable.h @@ -35,18 +35,6 @@ namespace storm { */ 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. - * - * @param oldVariable The variable to copy. - * @param newName New name of this variable. - * @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 variable is defined. - * @param lineNumber The line number in which the variable is defined. - */ - BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber); - friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable); }; diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index 468e0da2b..5ca424bb1 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -5,21 +5,6 @@ namespace storm { Command::Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) { // Nothing to do here. } - - 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, newGlobalUpdateIndex, renaming, filename, lineNumber); - ++newGlobalUpdateIndex; - } - } std::string const& Command::getActionName() const { return this->actionName; diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h index 0173832e8..24510bfda 100644 --- a/src/storage/prism/Command.h +++ b/src/storage/prism/Command.h @@ -24,18 +24,6 @@ namespace storm { */ Command(uint_fast64_t globalIndex, std::string const& actionName, storm::expressions::Expression const& guardExpression, std::vector const& updates, std::string const& filename = "", uint_fast64_t lineNumber = 0); - /*! - * Creates a copy of the given command and performs the provided renaming. - * - * @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, 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; Command(Command const& other) = default; diff --git a/src/storage/prism/IntegerVariable.cpp b/src/storage/prism/IntegerVariable.cpp index e025a8636..2815d5a6c 100644 --- a/src/storage/prism/IntegerVariable.cpp +++ b/src/storage/prism/IntegerVariable.cpp @@ -10,10 +10,6 @@ namespace storm { // Intentionally left empty. } - IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : Variable(oldVariable, newName, renaming, filename, lineNumber), lowerBoundExpression(oldVariable.getLowerBoundExpression().substitute(renaming)), upperBoundExpression(oldVariable.getUpperBoundExpression().substitute(renaming)) { - // Intentionally left empty. - } - storm::expressions::Expression const& IntegerVariable::getLowerBoundExpression() const { return this->lowerBoundExpression; } diff --git a/src/storage/prism/IntegerVariable.h b/src/storage/prism/IntegerVariable.h index 919bab480..817752925 100644 --- a/src/storage/prism/IntegerVariable.h +++ b/src/storage/prism/IntegerVariable.h @@ -39,17 +39,6 @@ namespace storm { */ IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); - /*! - * Creates a copy of the given integer variable and performs the provided renaming. - * - * @param oldVariable The variable to copy. - * @param newName New name of this variable. - * @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 variable is defined. - * @param lineNumber The line number in which the variable is defined. - */ - IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); - /*! * Retrieves an expression defining the lower bound for this integer variable. * diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 48544efff..2c87a2077 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -9,34 +9,7 @@ namespace storm { // Initialize the internal mappings for fast information retrieval. this->createMappings(); } - - 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()); - 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); - } - - // 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, newGlobalCommandIndex, newGlobalUpdateIndex, renaming, filename, lineNumber); - ++newGlobalCommandIndex; - newGlobalUpdateIndex += this->commands.back().getNumberOfUpdates(); - } - - // Finally, update internal mappings. - this->createMappings(); - } - + std::size_t Module::getNumberOfBooleanVariables() const { return this->booleanVariables.size(); } diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index 4a1608d22..45ccf4f8a 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -28,20 +28,6 @@ namespace storm { */ 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 - * having all identifiers renamed according to the given map. - * - * @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, 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; Module(Module const& other) = default; diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index dc609b4ad..21c204b00 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -8,21 +8,6 @@ namespace storm { this->createAssignmentMapping(); } - Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(update.getLikelihoodExpression().substitute(renaming)), assignments(), variableToAssignmentIndexMap(), globalIndex(newGlobalIndex) { - // Rename all assignments. - for (auto const& assignment : update.getAssignments()) { - auto const& namePair = renaming.find(assignment.getVariableName()); - if (namePair != renaming.end()) { - this->assignments.emplace_back(Assignment(assignment, renaming, filename, lineNumber)); - } else { - this->assignments.emplace_back(Assignment(assignment)); - } - } - - // Create the assignment mapping. - this->createAssignmentMapping(); - } - storm::expressions::Expression const& Update::getLikelihoodExpression() const { return likelihoodExpression; } diff --git a/src/storage/prism/Update.h b/src/storage/prism/Update.h index 6f85ece29..a6e53ea50 100644 --- a/src/storage/prism/Update.h +++ b/src/storage/prism/Update.h @@ -21,17 +21,6 @@ namespace storm { */ Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector const& assignments, std::string const& filename = "", uint_fast64_t lineNumber = 0); - /*! - * Creates a copy of the given update and performs the provided renaming. - * - * @param update The update that is to be copied. - * @param newGlobalIndex The global index of the resulting update. - * @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 update is defined. - * @param lineNumber The line number in which the update is defined. - */ - Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); - // Create default implementations of constructors/assignment. Update() = default; Update(Update const& other) = default; diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index 1729ba036..739d9ca5b 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/test/functional/parser/PrismParserTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/parser/prismparser/PrismParser.h" +#include "src/parser/PrismParser.h" TEST(PrismParser, SimpleParsingOnlyTest) { std::string testInput = @@ -29,6 +29,19 @@ TEST(PrismParser, StandardModelParsingTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm", false)); } +TEST(PrismParser, StandardModelFullTest) { + storm::prism::Program result; + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/coin2.nm", true)); + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/crowds5_5.pm", true)); + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/csma2_2.nm", true)); + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/die.pm", true)); + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/firewire.nm", true)); + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3.nm", true)); + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/leader3_5.pm", true)); + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/two_dice.nm", true)); + EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/parser/prism/wlan0_collide.nm", true)); +} + TEST(PrismParser, SimpleFullTest) { std::string testInput = R"(dtmc @@ -56,6 +69,7 @@ TEST(PrismParser, ComplexFullTest) { formula test = a >= 10 & (max(a,b) > floor(e)); formula test2 = a+b; + formula test3 = (a + b > 10 ? floor(a) : h) + a; global g : bool init false; global h : [0 .. b]; @@ -65,14 +79,14 @@ TEST(PrismParser, ComplexFullTest) { j : bool init c; k : [125..a] init a; - [a] test2&false -> (i'=true)&(h'=1+1) + 1 : (j'=floor(a) <= max(k, b) - 1 + k); + [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(a) <= max(k, b) - 1 + k); endmodule module mod2 [b] (k > 3) & false & (min(a, 0) < max(h, k)) -> 1-e: (j'=(1-a) * 2 + floor(f)); endmodule - module mod3 = mod2 [ x = y ] endmodule + module mod3 = mod1 [ i = i1, j = j1, k = k1 ] endmodule label "mal" = max(a, 10) > 0; @@ -92,7 +106,6 @@ TEST(PrismParser, ComplexFullTest) { storm::prism::Program result; result = storm::parser::PrismParser::parseFromString(testInput, "testfile", true); - std::cout << result << std::endl; EXPECT_EQ(storm::prism::Program::ModelType::MA, result.getModelType()); EXPECT_EQ(3, result.getNumberOfModules()); EXPECT_EQ(2, result.getNumberOfRewardModels()); diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 6563a749d..8bb2e4c04 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -138,6 +138,14 @@ TEST(Expression, OperatorTest) { storm::expressions::Expression tempExpression; + ASSERT_THROW(tempExpression = trueExpression.ite(falseExpression, piExpression), storm::exceptions::InvalidTypeException); + ASSERT_NO_THROW(tempExpression = boolConstExpression.ite(threeExpression, doubleVarExpression)); + EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Double); + ASSERT_NO_THROW(tempExpression = boolConstExpression.ite(threeExpression, intVarExpression)); + EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); + ASSERT_NO_THROW(tempExpression = boolConstExpression.ite(trueExpression, falseExpression)); + EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Bool); + ASSERT_THROW(tempExpression = trueExpression + piExpression, storm::exceptions::InvalidTypeException); ASSERT_NO_THROW(tempExpression = threeExpression + threeExpression); EXPECT_TRUE(tempExpression.getReturnType() == storm::expressions::ExpressionReturnType::Int); @@ -367,4 +375,9 @@ TEST(Expression, SimpleEvaluationTest) { EXPECT_TRUE(tempExpression.evaluateAsBool(valuation)); ASSERT_NO_THROW(valuation.setIntegerValue("y", 3)); EXPECT_FALSE(tempExpression.evaluateAsBool(valuation)); + + ASSERT_NO_THROW(tempExpression = ((intVarExpression < threeExpression).ite(trueExpression, falseExpression))); + ASSERT_THROW(tempExpression.evaluateAsDouble(valuation), storm::exceptions::InvalidTypeException); + ASSERT_THROW(tempExpression.evaluateAsInt(valuation), storm::exceptions::InvalidTypeException); + EXPECT_FALSE(tempExpression.evaluateAsBool(valuation)); } \ No newline at end of file