diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 36a01f05f..771578f17 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -151,7 +151,13 @@ namespace storm { booleanVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("bool")) > -((qi::lit("init") > boolExpression[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)]; booleanVariableDefinition.name("boolean variable definition"); - integerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; + boundedIntegerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("[")) > intExpression > qi::lit("..") > intExpression > qi::lit("]") > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)]; + boundedIntegerVariableDefinition.name("bounded integer variable definition"); + + unboundedIntegerVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("int")) > -(qi::lit("init") > intExpression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, storm::expressions::Expression(), storm::expressions::Expression(), qi::_a)]; + unboundedIntegerVariableDefinition.name("unbounded integer variable definition"); + + integerVariableDefinition = boundedIntegerVariableDefinition | unboundedIntegerVariableDefinition; integerVariableDefinition.name("integer variable definition"); clockVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)]; diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index 2a1d5beeb..0554d088f 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -240,8 +240,6 @@ namespace storm { // Rules for global variable definitions. qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalVariableDefinition; - qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalBooleanVariableDefinition; - qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalIntegerVariableDefinition; // Rules for modules definition. qi::rule<Iterator, std::string(), Skipper> knownModuleName; @@ -254,6 +252,8 @@ namespace storm { qi::rule<Iterator, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&, std::vector<storm::prism::ClockVariable>&), Skipper> variableDefinition; qi::rule<Iterator, storm::prism::BooleanVariable(), qi::locals<storm::expressions::Expression>, Skipper> booleanVariableDefinition; qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> integerVariableDefinition; + qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> boundedIntegerVariableDefinition; + qi::rule<Iterator, storm::prism::IntegerVariable(), qi::locals<storm::expressions::Expression>, Skipper> unboundedIntegerVariableDefinition; qi::rule<Iterator, storm::prism::ClockVariable(), qi::locals<storm::expressions::Expression>, Skipper> clockVariableDefinition; // Rules for command definitions.