sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

PrismParser: Check for expression type. Support for formulas in arbitrary order.

main
TimQu 6 years ago
parent
48e98119d5
commit
5f3065ec5a
4 changed files with 69 additions and 29 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm-parsers/parser/ExpressionParser.cpp
  2. 74
      src/storm-parsers/parser/PrismParser.cpp
  3. 14
      src/storm-parsers/parser/PrismParser.h
  4. 2
      src/storm/storage/prism/Program.cpp

4
src/storm-parsers/parser/ExpressionParser.cpp
View File

@ -225,13 +225,15 @@ namespace storm {
try { try {
// Start parsing. // Start parsing.
bool succeeded = qi::phrase_parse(iter, last, *this, storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); bool succeeded = qi::phrase_parse(iter, last, *this, storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
succeeded &= (iter == last);
if (!succeeded) { if (!succeeded) {
STORM_LOG_THROW(ignoreError, storm::exceptions::WrongFormatException, "Could not parse expression '" << expressionString << "'."); STORM_LOG_THROW(ignoreError, storm::exceptions::WrongFormatException, "Could not parse expression '" << expressionString << "'.");
return result;
return storm::expressions::Expression();
} }
STORM_LOG_DEBUG("Parsed expression successfully."); STORM_LOG_DEBUG("Parsed expression successfully.");
} catch (qi::expectation_failure<PositionIteratorType> const& e) { } catch (qi::expectation_failure<PositionIteratorType> const& e) {
STORM_LOG_THROW(ignoreError, storm::exceptions::WrongFormatException, e.what_); STORM_LOG_THROW(ignoreError, storm::exceptions::WrongFormatException, e.what_);
return storm::expressions::Expression();
} }
return result; return result;
} }

74
src/storm-parsers/parser/PrismParser.cpp
View File

@ -82,6 +82,15 @@ namespace storm {
PrismParser::PrismParser(std::string const& filename, Iterator first, bool prismCompatibility) : PrismParser::base_type(start), secondRun(false), prismCompatibility(prismCompatibility), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) { PrismParser::PrismParser(std::string const& filename, Iterator first, bool prismCompatibility) : PrismParser::base_type(start), secondRun(false), prismCompatibility(prismCompatibility), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) {
ExpressionParser& expression_ = *expressionParser; ExpressionParser& expression_ = *expressionParser;
boolExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isOfBoolType, phoenix::ref(*this), qi::_val)];
boolExpression.name("boolean expression");
intExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isOfIntType, phoenix::ref(*this), qi::_val)];
intExpression.name("integer expression");
numericalExpression = (expression_[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isOfNumericalType, phoenix::ref(*this), qi::_val)];
numericalExpression.name("numerical expression");
// Parse simple identifier. // 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 %= 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"); identifier.name("identifier");
@ -95,13 +104,19 @@ namespace storm {
// Defined constants. Will be checked before undefined constants. // Defined constants. Will be checked before undefined constants.
// ">>" before literal '=' because we can still parse an undefined constant afterwards. // ">>" before literal '=' because we can still parse an undefined constant afterwards.
definedBooleanConstantDefinition = (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier) >> (qi::lit("=") > expression_[qi::_pass = phoenix::bind(&PrismParser::isOfBoolType, phoenix::ref(*this), qi::_1)] > qi::lit(";")))[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedBooleanConstantDefinition = (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier)
>> (qi::lit("=") > boolExpression > qi::lit(";"))
)[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedBooleanConstantDefinition.name("defined boolean constant declaration"); definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = (((qi::lit("const") >> -qi::lit("int")) >> freshIdentifier) >> (qi::lit("=") > expression_ > qi::lit(";")))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)]; // '>>' before freshIdentifier because of the optional 'int'. Otherwise, undefined constant 'const bool b;' would not parse.
definedIntegerConstantDefinition = (((qi::lit("const") >> -qi::lit("int")) >> freshIdentifier)
>> (qi::lit("=") > intExpression > qi::lit(";"))
)[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)]; // '>>' before freshIdentifier because of the optional 'int'. Otherwise, undefined constant 'const bool b;' would not parse.
definedIntegerConstantDefinition.name("defined integer constant declaration"); definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = (((qi::lit("const") >> qi::lit("double")) > freshIdentifier) >> (qi::lit("=") > expression_ > qi::lit(";")))[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedDoubleConstantDefinition = (((qi::lit("const") >> qi::lit("double")) > freshIdentifier)
>> (qi::lit("=") > numericalExpression > qi::lit(";"))
)[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedDoubleConstantDefinition.name("defined double constant declaration"); definedDoubleConstantDefinition.name("defined double constant declaration");
definedConstantDefinition %= (definedBooleanConstantDefinition | definedDoubleConstantDefinition | definedIntegerConstantDefinition); definedConstantDefinition %= (definedBooleanConstantDefinition | definedDoubleConstantDefinition | definedIntegerConstantDefinition);
@ -122,19 +137,19 @@ namespace storm {
undefinedConstantDefinition.name("undefined constant definition"); undefinedConstantDefinition.name("undefined constant definition");
// formula definitions. This will be changed for the second run. // formula definitions. This will be changed for the second run.
formulaDefinitionRhs = (qi::lit("=") > qi::as_string[(+(qi::char_ - qi::lit(";")))][qi::_val = qi::_1] > qi::lit(";"));
formulaDefinitionRhs = (qi::lit("=") > qi::as_string[(+(qi::char_ - (qi::lit(";") | qi::lit("endmodule"))))][qi::_val = qi::_1] > qi::lit(";"));
formulaDefinitionRhs.name("formula defining expression"); formulaDefinitionRhs.name("formula defining expression");
formulaDefinition = (qi::lit("formula") > freshIdentifier > formulaDefinitionRhs )[qi::_val = phoenix::bind(&PrismParser::createFormulaFirstRun, phoenix::ref(*this), qi::_1, qi::_2)]; formulaDefinition = (qi::lit("formula") > freshIdentifier > formulaDefinitionRhs )[qi::_val = phoenix::bind(&PrismParser::createFormulaFirstRun, phoenix::ref(*this), qi::_1, qi::_2)];
formulaDefinition.name("formula definition"); formulaDefinition.name("formula definition");
booleanVariableDefinition = ((freshIdentifier >> qi::lit(":") >> qi::lit("bool")) > -((qi::lit("init") > expression_[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 = (((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"); booleanVariableDefinition.name("boolean variable definition");
integerVariableDefinition = ((freshIdentifier >> qi::lit(":") >> qi::lit("[")) > expression_ > qi::lit("..") > expression_ > qi::lit("]") > -(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 = (((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)];
integerVariableDefinition.name("integer variable definition"); 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)];
clockVariableDefinition = (((freshIdentifier > qi::lit(":")) >> qi::lit("clock")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createClockVariable, phoenix::ref(*this), qi::_1)];
clockVariableDefinition.name("clock variable definition"); clockVariableDefinition.name("clock variable definition");
variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)] | clockVariableDefinition[phoenix::push_back(qi::_r3, qi::_1)]); variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)] | clockVariableDefinition[phoenix::push_back(qi::_r3, qi::_1)]);
@ -143,33 +158,33 @@ namespace storm {
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 = (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"); globalVariableDefinition.name("global variable declaration list");
stateRewardDefinition = (expression_ > qi::lit(":") > expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
stateRewardDefinition = (boolExpression > qi::lit(":") > numericalExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
stateRewardDefinition.name("state reward definition"); stateRewardDefinition.name("state reward definition");
stateActionRewardDefinition = (qi::lit("[") >> -identifier >> qi::lit("]") >> expression_ >> qi::lit(":") >> expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateActionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_r1)];
stateActionRewardDefinition = (qi::lit("[") > -identifier > qi::lit("]") > boolExpression > qi::lit(":") > numericalExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateActionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_r1)];
stateActionRewardDefinition.name("state action reward definition"); stateActionRewardDefinition.name("state action reward definition");
transitionRewardDefinition = (qi::lit("[") > -identifier > qi::lit("]") > expression_ > qi::lit("->") > expression_ > qi::lit(":") > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4, qi::_r1)];
transitionRewardDefinition = ((qi::lit("[") > -identifier[qi::_a = qi::_1] > qi::lit("]") > boolExpression[qi::_b = qi::_1]) >> (qi::lit("->") > boolExpression[qi::_c = qi::_1] > qi::lit(":") > numericalExpression[qi::_d = qi::_1] > qi::lit(";")))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d, qi::_r1)];
transitionRewardDefinition.name("transition reward definition"); transitionRewardDefinition.name("transition reward definition");
freshRewardModelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshRewardModelName, phoenix::ref(*this), qi::_1)]; freshRewardModelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshRewardModelName, phoenix::ref(*this), qi::_1)];
freshRewardModelName.name("fresh reward model name"); freshRewardModelName.name("fresh reward model name");
rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > freshRewardModelName[qi::_a = qi::_1] > qi::lit("\"")) rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > freshRewardModelName[qi::_a = qi::_1] > qi::lit("\""))
> +( stateRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]
> +( transitionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_d, qi::_1)]
| stateActionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_c, qi::_1)] | stateActionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_c, qi::_1)]
| transitionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_d, qi::_1)]
| stateRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]
) )
>> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d)];
> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d)];
rewardModelDefinition.name("reward model definition"); rewardModelDefinition.name("reward model definition");
initialStatesConstruct = (qi::lit("init") > expression_ > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
initialStatesConstruct = (qi::lit("init") > boolExpression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
initialStatesConstruct.name("initial construct"); initialStatesConstruct.name("initial construct");
observablesConstruct = (qi::lit("observables") > (identifier % qi::lit(",") )> qi::lit("endobservables"))[phoenix::bind(&PrismParser::createObservablesList, phoenix::ref(*this), qi::_1)]; observablesConstruct = (qi::lit("observables") > (identifier % qi::lit(",") )> qi::lit("endobservables"))[phoenix::bind(&PrismParser::createObservablesList, phoenix::ref(*this), qi::_1)];
observablesConstruct.name("observables construct"); observablesConstruct.name("observables construct");
invariantConstruct = (qi::lit("invariant") > expression_ > qi::lit("endinvariant"))[qi::_val = qi::_1];
invariantConstruct = (qi::lit("invariant") > boolExpression > qi::lit("endinvariant"))[qi::_val = qi::_1];
invariantConstruct.name("invariant construct"); invariantConstruct.name("invariant construct");
knownModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownModuleName, phoenix::ref(*this), qi::_1)]; knownModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isKnownModuleName, phoenix::ref(*this), qi::_1)];
@ -220,16 +235,17 @@ namespace storm {
freshLabelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshLabelName, phoenix::ref(*this), qi::_1)]; freshLabelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshLabelName, phoenix::ref(*this), qi::_1)];
freshLabelName.name("fresh label name"); freshLabelName.name("fresh label name");
labelDefinition = (qi::lit("label") > -qi::lit("\"") > freshLabelName > -qi::lit("\"") > qi::lit("=") > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
labelDefinition = (qi::lit("label") > -qi::lit("\"") > freshLabelName > -qi::lit("\"") > qi::lit("=") > boolExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
labelDefinition.name("label definition"); 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 = ((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"); assignmentDefinition.name("assignment");
assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()]; assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
assignmentDefinitionList.name("assignment list"); assignmentDefinitionList.name("assignment list");
updateDefinition = (((expression_ >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
updateDefinition = (assignmentDefinitionList[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), manager->rational(1), qi::_1, qi::_r1)]
| ((numericalExpression > qi::lit(":") > assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]));
updateDefinition.name("update"); updateDefinition.name("update");
updateListDefinition %= +updateDefinition(qi::_r1) % "+"; updateListDefinition %= +updateDefinition(qi::_r1) % "+";
@ -239,7 +255,7 @@ namespace storm {
commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]")) commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]"))
| |
(qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true])) (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true]))
> +(qi::char_ - qi::lit(";"))
> +(qi::char_ - (qi::lit(";") | qi::lit("endmodule")))
> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDummyCommand, phoenix::ref(*this), qi::_1, qi::_r1)]; > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDummyCommand, phoenix::ref(*this), qi::_1, qi::_r1)];
commandDefinition.name("command definition"); commandDefinition.name("command definition");
@ -309,6 +325,9 @@ namespace storm {
> updateListDefinition(qi::_r1) > updateListDefinition(qi::_r1)
> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_1, qi::_2, qi::_3, qi::_r1)]; > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_1, qi::_2, qi::_3, qi::_r1)];
auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3);
qi::on_success(commandDefinition, setLocationInfoFunction);
formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > *expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormulaSecondRun, phoenix::ref(*this), qi::_1, qi::_2)]; formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > *expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormulaSecondRun, phoenix::ref(*this), qi::_1, qi::_2)];
formulaDefinition.name("formula definition"); formulaDefinition.name("formula definition");
this->secondRun = true; this->secondRun = true;
@ -324,7 +343,7 @@ namespace storm {
void PrismParser::createFormulaIdentifiers(std::vector<storm::prism::Formula> const& formulas) { void PrismParser::createFormulaIdentifiers(std::vector<storm::prism::Formula> const& formulas) {
STORM_LOG_THROW(formulas.size() == this->formulaExpressions.size(), storm::exceptions::UnexpectedException, "Unexpected number of formulas and formula expressions"); STORM_LOG_THROW(formulas.size() == this->formulaExpressions.size(), storm::exceptions::UnexpectedException, "Unexpected number of formulas and formula expressions");
this->formulaOrder.clear();
storm::storage::BitVector unprocessed(formulas.size(), true); storm::storage::BitVector unprocessed(formulas.size(), true);
// It might be that formulas are declared in a weird order. // It might be that formulas are declared in a weird order.
// We follow a trial-and-error approach: If we can not parse the expression for one formula, // We follow a trial-and-error approach: If we can not parse the expression for one formula,
@ -338,6 +357,7 @@ namespace storm {
if (expression.isInitialized()) { if (expression.isInitialized()) {
progress = true; progress = true;
unprocessed.set(formulaIndex, false); unprocessed.set(formulaIndex, false);
formulaOrder.push_back(formulaIndex);
storm::expressions::Variable variable; storm::expressions::Variable variable;
try { try {
if (expression.hasIntegerType()) { if (expression.hasIntegerType()) {
@ -361,7 +381,7 @@ namespace storm {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Invalid expression for formula '" << formulas[formulaIndex].getName() << "' at line '" << formulas[formulaIndex].getLineNumber() << "':\n\t" << formulaExpressions[formulaIndex]); STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Invalid expression for formula '" << formulas[formulaIndex].getName() << "' at line '" << formulas[formulaIndex].getLineNumber() << "':\n\t" << formulaExpressions[formulaIndex]);
} }
STORM_LOG_THROW(unprocessed.getNumberOfSetBits() == 1, storm::exceptions::WrongFormatException, "Unable to parse expressions for " << unprocessed.getNumberOfSetBits() << " formulas. This could be due to circular dependencies"); STORM_LOG_THROW(unprocessed.getNumberOfSetBits() == 1, storm::exceptions::WrongFormatException, "Unable to parse expressions for " << unprocessed.getNumberOfSetBits() << " formulas. This could be due to circular dependencies");
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Unable to parse expression for formula '" << formulas[unprocessed.getNextSetIndex(0)].getName() << "' formulas.");
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Unable to parse expression for formula '" << formulas[unprocessed.getNextSetIndex(0)].getName() << "'.");
} }
} }
@ -436,7 +456,7 @@ namespace storm {
return !this->secondRun || expression.hasIntegerType(); return !this->secondRun || expression.hasIntegerType();
} }
bool PrismParser::isOfDoubleType(storm::expressions::Expression const& expression) {
bool PrismParser::isOfNumericalType(storm::expressions::Expression const& expression) {
return !this->secondRun || expression.hasNumericalType(); return !this->secondRun || expression.hasNumericalType();
} }
@ -905,8 +925,16 @@ namespace storm {
finalModelType = storm::prism::Program::ModelType::MDP; finalModelType = storm::prism::Program::ModelType::MDP;
} }
// make sure formulas are stored in a proper order.
std::vector<storm::prism::Formula> orderedFormulas;
if (this->secondRun) {
orderedFormulas.reserve(globalProgramInformation.formulas.size());
for (uint64_t const& i : formulaOrder) {
orderedFormulas.push_back(std::move(globalProgramInformation.formulas[i]));
}
}
return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
return storm::prism::Program(manager, finalModelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, orderedFormulas, globalProgramInformation.modules, globalProgramInformation.actionIndices, globalProgramInformation.rewardModels, globalProgramInformation.labels, secondRun && !globalProgramInformation.hasInitialConstruct ? boost::none : boost::make_optional(globalProgramInformation.initialConstruct), globalProgramInformation.systemCompositionConstruct, prismCompatibility, this->getFilename(), 1, this->secondRun);
} }
void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const { void PrismParser::removeInitialConstruct(GlobalProgramInformation& globalProgramInformation) const {

14
src/storm-parsers/parser/PrismParser.h
View File

@ -192,7 +192,12 @@ namespace storm {
std::string const& getFilename() const; std::string const& getFilename() const;
mutable std::set<std::string> observables; mutable std::set<std::string> observables;
// Store the expressions of formulas. They have to be parsed after the first and before the second run
std::vector<std::string> formulaExpressions; std::vector<std::string> formulaExpressions;
// Stores a proper order in which formulas can be evaluated. This is necessary since formulas might depend on each other.
// E.g. for "formula x = y; formula y = z;" we have to swap the order of the two formulas.
std::vector<uint64_t> formulaOrder;
// A function used for annotating the entities with their position. // A function used for annotating the entities with their position.
phoenix::function<PositionAnnotation> annotate; phoenix::function<PositionAnnotation> annotate;
@ -206,6 +211,11 @@ namespace storm {
// Rules for model type. // Rules for model type.
qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition; qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition;
// Rules for parsing expressions of specific type
qi::rule<Iterator, storm::expressions::Expression(), Skipper> boolExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> intExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> numericalExpression;
// Rules for parsing the program header. // Rules for parsing the program header.
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedConstantDefinition; qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedBooleanConstantDefinition; qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedBooleanConstantDefinition;
@ -246,7 +256,7 @@ namespace storm {
qi::rule<Iterator, storm::prism::RewardModel(GlobalProgramInformation&), qi::locals<std::string, std::vector<storm::prism::StateReward>, std::vector<storm::prism::StateActionReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition; qi::rule<Iterator, storm::prism::RewardModel(GlobalProgramInformation&), qi::locals<std::string, std::vector<storm::prism::StateReward>, std::vector<storm::prism::StateActionReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition;
qi::rule<Iterator, storm::prism::StateReward(), Skipper> stateRewardDefinition; qi::rule<Iterator, storm::prism::StateReward(), Skipper> stateRewardDefinition;
qi::rule<Iterator, storm::prism::StateActionReward(GlobalProgramInformation&), Skipper> stateActionRewardDefinition; qi::rule<Iterator, storm::prism::StateActionReward(GlobalProgramInformation&), Skipper> stateActionRewardDefinition;
qi::rule<Iterator, storm::prism::TransitionReward(GlobalProgramInformation&), Skipper> transitionRewardDefinition;
qi::rule<Iterator, storm::prism::TransitionReward(GlobalProgramInformation&), qi::locals<std::string, storm::expressions::Expression, storm::expressions::Expression,storm::expressions::Expression>, Skipper> transitionRewardDefinition;
// Rules for initial states expression. // Rules for initial states expression.
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct; qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> initialStatesConstruct;
@ -300,7 +310,7 @@ namespace storm {
bool isFreshRewardModelName(std::string const& moduleName); bool isFreshRewardModelName(std::string const& moduleName);
bool isOfBoolType(storm::expressions::Expression const& expression); bool isOfBoolType(storm::expressions::Expression const& expression);
bool isOfIntType(storm::expressions::Expression const& expression); bool isOfIntType(storm::expressions::Expression const& expression);
bool isOfDoubleType(storm::expressions::Expression const& expression);
bool isOfNumericalType(storm::expressions::Expression const& expression);
bool isValidModuleRenamingList(std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation const& globalProgramInformation) const; bool isValidModuleRenamingList(std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation const& globalProgramInformation) const;
bool addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation); bool addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
bool addSystemCompositionConstruct(std::shared_ptr<storm::prism::Composition> const& composition, GlobalProgramInformation& globalProgramInformation); bool addSystemCompositionConstruct(std::shared_ptr<storm::prism::Composition> const& composition, GlobalProgramInformation& globalProgramInformation);

2
src/storm/storage/prism/Program.cpp
View File

@ -1123,7 +1123,7 @@ namespace storm {
for (auto const& formula : this->getFormulas()) { for (auto const& formula : this->getFormulas()) {
std::set<storm::expressions::Variable> containedVariables = formula.getExpression().getVariables(); std::set<storm::expressions::Variable> containedVariables = formula.getExpression().getVariables();
bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end()); bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": expression '"<< formula.getExpression() << "'of formula '" << formula.getName() << "' refers to unknown identifiers.");
if (formula.hasExpressionVariable()) { if (formula.hasExpressionVariable()) {
all.insert(formula.getExpressionVariable()); all.insert(formula.getExpressionVariable());
variablesAndConstants.insert(formula.getExpressionVariable()); variablesAndConstants.insert(formula.getExpressionVariable());

Write Preview
Loading…
Cancel
Save