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

PrismParser: Various improvements of error output. Support for using formulas before they were declared.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
38c7762254
commit
12ef18a239
4 changed files with 254 additions and 120 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. 317
      src/storm-parsers/parser/PrismParser.cpp
  2. 26
      src/storm-parsers/parser/PrismParser.h
  3. 6
      src/storm/storage/prism/Formula.cpp
  4. 13
      src/storm/storage/prism/Formula.h

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

@ -8,8 +8,10 @@
#include "storm/utility/macros.h" #include "storm/utility/macros.h"
#include "storm/utility/file.h" #include "storm/utility/file.h"
#include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/WrongFormatException.h"
#include "storm/exceptions/UnexpectedException.h"
#include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/VariableExpression.h"
#include "storm-parsers/parser/ExpressionParser.h" #include "storm-parsers/parser/ExpressionParser.h"
@ -83,43 +85,55 @@ namespace storm {
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");
// Fail if the identifier has been used before
freshIdentifier = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshIdentifier, phoenix::ref(*this), qi::_1)];
freshIdentifier.name("fresh identifier");
modelTypeDefinition %= modelType_; modelTypeDefinition %= modelType_;
modelTypeDefinition.name("model type"); 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 | undefinedDoubleConstantDefinition | undefinedIntegerConstantDefinition);
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)];
// Defined constants. Will be checked before undefined constants.
// ">>" before literal '=' because we can still parse an undefined constant afterwards.
definedBooleanConstantDefinition = (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier) >> (qi::lit("=") > expression_ > 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") >> identifier >> qi::lit("=")) > expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)];
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.name("defined integer constant declaration"); 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 = (((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.name("defined double constant declaration"); definedDoubleConstantDefinition.name("defined double constant declaration");
definedConstantDefinition %= (definedBooleanConstantDefinition | definedDoubleConstantDefinition | definedIntegerConstantDefinition); definedConstantDefinition %= (definedBooleanConstantDefinition | definedDoubleConstantDefinition | definedIntegerConstantDefinition);
definedConstantDefinition.name("defined constant definition"); 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)];
// Undefined constants. At this point we already checked for a defined constant, therefore a ";" is required after the identifier;
undefinedBooleanConstantDefinition = (((qi::lit("const") >> qi::lit("bool")) > freshIdentifier) > 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")) > freshIdentifier) > 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")) > freshIdentifier) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createUndefinedDoubleConstant, phoenix::ref(*this), qi::_1)];
undefinedDoubleConstantDefinition.name("undefined double constant definition");
undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedDoubleConstantDefinition | undefinedIntegerConstantDefinition); // Due to the 'const N;' syntax, it is important to have integer constants last
undefinedConstantDefinition.name("undefined constant definition");
// 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.name("formula defining expression");
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 = ((identifier >> 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") > 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.name("boolean variable definition"); booleanVariableDefinition.name("boolean variable definition");
integerVariableDefinition = ((identifier >> 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("[")) > 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.name("integer variable definition"); integerVariableDefinition.name("integer variable definition");
clockVariableDefinition = ((identifier >> 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)]);
@ -137,7 +151,10 @@ namespace storm {
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::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.name("transition reward definition"); transitionRewardDefinition.name("transition reward definition");
rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > identifier[qi::_a = qi::_1] > qi::lit("\""))
freshRewardModelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshRewardModelName, phoenix::ref(*this), qi::_1)];
freshRewardModelName.name("fresh reward model name");
rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > freshRewardModelName[qi::_a = qi::_1] > qi::lit("\""))
> +( stateRewardDefinition[phoenix::push_back(qi::_b, qi::_1)] > +( stateRewardDefinition[phoenix::push_back(qi::_b, 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)] | transitionRewardDefinition(qi::_r1)[phoenix::push_back(qi::_d, qi::_1)]
@ -154,6 +171,12 @@ namespace storm {
invariantConstruct = (qi::lit("invariant") > expression_ > qi::lit("endinvariant"))[qi::_val = qi::_1]; invariantConstruct = (qi::lit("invariant") > expression_ > 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.name("existing module name");
freshModuleName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshModuleName, phoenix::ref(*this), qi::_1)];
freshModuleName.name("fresh module name");
systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
systemCompositionConstruct.name("system composition construct"); systemCompositionConstruct.name("system composition construct");
@ -193,7 +216,10 @@ namespace storm {
moduleComposition = identifier[qi::_val = phoenix::bind(&PrismParser::createModuleComposition, phoenix::ref(*this), qi::_1)]; moduleComposition = identifier[qi::_val = phoenix::bind(&PrismParser::createModuleComposition, phoenix::ref(*this), qi::_1)];
moduleComposition.name("module composition"); moduleComposition.name("module composition");
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)];
freshLabelName = (identifier[qi::_val = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isFreshLabelName, phoenix::ref(*this), qi::_1)];
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.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)];
@ -216,16 +242,18 @@ namespace storm {
> 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");
moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3, qi::_r1)];
// We first check for a module renaming, i.e., for this rule we certainly have to see a module definition
moduleDefinition = ((qi::lit("module") > freshModuleName > *(variableDefinition(qi::_a, qi::_b, qi::_c))) > -invariantConstruct > (*commandDefinition(qi::_r1)) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_3, qi::_r1)];
moduleDefinition.name("module definition"); moduleDefinition.name("module definition");
moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[")
> ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(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");
moduleRenamingList = (qi::lit("[") > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))] % ",") > qi::lit("]"))[qi::_val = qi::_a];
moduleRenamingList.name("Module renaming list");
moduleDefinitionList %= +(moduleRenaming(qi::_r1) | moduleDefinition(qi::_r1))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, qi::_r1), qi::_1)];
moduleDefinitionList.name("module list");
moduleRenaming = (((qi::lit("module") > freshModuleName) >> qi::lit("="))
> knownModuleName[qi::_a = qi::_1]
> (moduleRenamingList[qi::_b = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isValidModuleRenamingList, phoenix::ref(*this), qi::_a, qi::_b, qi::_r1)]
> qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createRenamedModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_r1)];
moduleRenaming.name("module definition via renaming");
start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), phoenix::ref(globalProgramInformation))] start = (qi::eps[phoenix::bind(&PrismParser::removeInitialConstruct, phoenix::ref(*this), phoenix::ref(globalProgramInformation))]
> modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)] > modelTypeDefinition[phoenix::bind(&PrismParser::setModelType, phoenix::ref(*this), phoenix::ref(globalProgramInformation), qi::_1)]
@ -280,9 +308,47 @@ 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)];
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");
this->secondRun = true; this->secondRun = true;
this->expressionParser->setIdentifierMapping(&this->identifiers_); this->expressionParser->setIdentifierMapping(&this->identifiers_);
auto formulas = std::move(this->globalProgramInformation.formulas);
this->globalProgramInformation.moveToSecondRun(); this->globalProgramInformation.moveToSecondRun();
// We need to parse the formula rhs between the first run and the second run, because
// * in the first run, the type of the formula (int, bool, clock) is not known
// * in the second run, formulas might be used before they are declared
createFormulaIdentifiers(formulas);
}
void PrismParser::createFormulaIdentifiers(std::vector<storm::prism::Formula>& formulas) {
STORM_LOG_THROW(formulas.size() == this->formulaExpressions.size(), storm::exceptions::UnexpectedException, "Unexpected number of formulas and formula expressions");
auto expressionIt = formulaExpressions.begin();
for (auto& formula : formulas) {
storm::expressions::Expression expression;
try {
expression = this->expressionParser->parseFromString(*expressionIt);
} catch (storm::exceptions::WrongFormatException const& e) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Invalid expression for formula '" << formula.getName() << "' at line '" << formula.getLineNumber() << "':\n\t" << *expressionIt);
}
storm::expressions::Variable variable;
try {
if (expression.hasIntegerType()) {
variable = manager->declareIntegerVariable(formula.getName());
} else if (expression.hasBooleanType()) {
variable = manager->declareBooleanVariable(formula.getName());
} else {
STORM_LOG_ASSERT(expression.hasNumericalType(), "Unexpected type for formula expression of formula " << formula.getName());
variable = manager->declareRationalVariable(formula.getName());
}
this->identifiers_.add(formula.getName(), variable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << formula.getName() << "' at line '" << formula.getLineNumber());
}
this->expressionParser->setIdentifierMapping(&this->identifiers_);
++expressionIt;
}
} }
void PrismParser::allowDoubleLiterals(bool flag) { void PrismParser::allowDoubleLiterals(bool flag) {
@ -300,8 +366,56 @@ namespace storm {
return true; return true;
} }
bool PrismParser::isKnownModuleName(std::string const& moduleName) {
if (!this->secondRun && this->globalProgramInformation.moduleToIndexMap.count(moduleName) == 0) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Unknown module '" << moduleName << "'.");
return false;
}
return true;
}
bool PrismParser::isFreshModuleName(std::string const& moduleName) {
if (!this->secondRun && this->globalProgramInformation.moduleToIndexMap.count(moduleName) != 0) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate module name '" << moduleName << "'.");
return false;
}
return true;
}
bool PrismParser::isFreshIdentifier(std::string const& identifier) {
if (!this->secondRun && this->manager->hasVariable(identifier)) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate identifier '" << identifier << "'.");
return false;
}
return true;
}
bool PrismParser::isFreshLabelName(std::string const& labelName) {
if (!this->secondRun) {
for (auto const& existingLabel : this->globalProgramInformation.labels) {
if (labelName == existingLabel.getName()) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate label name '" << identifier << "'.");
return false;
}
}
}
return true;
}
bool PrismParser::isFreshRewardModelName(std::string const& rewardModelName) {
if (!this->secondRun) {
for (auto const& existingRewardModel : this->globalProgramInformation.rewardModels) {
if (rewardModelName == existingRewardModel.getName()) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": Duplicate reward model name '" << identifier << "'.");
return false;
}
}
}
return true;
}
bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs.");
STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Program must not define two initial constructs.");
if (globalProgramInformation.hasInitialConstruct) { if (globalProgramInformation.hasInitialConstruct) {
return false; return false;
} }
@ -316,7 +430,7 @@ namespace storm {
} }
void PrismParser::setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType) { void PrismParser::setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType) {
STORM_LOG_THROW(globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not set model type multiple times.");
STORM_LOG_THROW(globalProgramInformation.modelType == storm::prism::Program::ModelType::UNDEFINED, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Program must not set model type multiple times.");
globalProgramInformation.modelType = modelType; globalProgramInformation.modelType = modelType;
} }
@ -350,11 +464,7 @@ namespace storm {
storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant, true); storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant, true);
this->identifiers_.add(newConstant, newVariable.getExpression()); this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) { } catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
} }
} }
return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename()); return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
@ -366,11 +476,7 @@ namespace storm {
storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant, true); storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant, true);
this->identifiers_.add(newConstant, newVariable.getExpression()); this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) { } catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
} }
} }
return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename()); return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
@ -382,11 +488,7 @@ namespace storm {
storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant, true); storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant, true);
this->identifiers_.add(newConstant, newVariable.getExpression()); this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) { } catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
} }
} }
return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename()); return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
@ -398,11 +500,7 @@ namespace storm {
storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant, true); storm::expressions::Variable newVariable = manager->declareBooleanVariable(newConstant, true);
this->identifiers_.add(newConstant, newVariable.getExpression()); this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) { } catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
} }
} }
return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename()); return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
@ -414,11 +512,7 @@ namespace storm {
storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant, true); storm::expressions::Variable newVariable = manager->declareIntegerVariable(newConstant, true);
this->identifiers_.add(newConstant, newVariable.getExpression()); this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) { } catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
} }
} }
return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename()); return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
@ -430,43 +524,25 @@ namespace storm {
storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant, true); storm::expressions::Variable newVariable = manager->declareRationalVariable(newConstant, true);
this->identifiers_.add(newConstant, newVariable.getExpression()); this->identifiers_.add(newConstant, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) { } catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(newConstant)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
}
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << newConstant << "'.");
} }
} }
return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename()); return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
} }
storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) {
// Only register formula in second run.
// This is necessary because the resulting type of the formula is only known in the second run.
// This prevents the parser from accepting formulas that depend on future formulas.
if (this->secondRun) {
storm::expressions::Variable variable;
try {
if (expression.hasIntegerType()) {
variable = manager->declareIntegerVariable(formulaName);
} else if (expression.hasBooleanType()) {
variable = manager->declareBooleanVariable(formulaName);
} else {
STORM_LOG_ASSERT(expression.hasNumericalType(), "Unexpected type for formula expression of formula " << formulaName);
variable = manager->declareRationalVariable(formulaName);
}
this->identifiers_.add(formulaName, variable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(formulaName)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << formulaName << "'.");
}
}
return storm::prism::Formula(variable, expression, this->getFilename());
} else {
return storm::prism::Formula(formulaName, expression, this->getFilename());
storm::prism::Formula PrismParser::createFormulaFirstRun(std::string const& formulaName, std::string const& expression) {
// Only store the expression as a string. It will be parsed between first and second run
// This is necessary because the resulting type of the formula is only known after the first run.
STORM_LOG_ASSERT(!this->secondRun, "This constructor should have only been called during the first run.");
formulaExpressions.push_back(expression);
return storm::prism::Formula(formulaName, this->getFilename());
} }
storm::prism::Formula PrismParser::createFormulaSecondRun(std::string const& formulaName, storm::expressions::Expression const& expression) {
// This is necessary because the resulting type of the formula is only known after the first run.
STORM_LOG_ASSERT(this->secondRun, "This constructor should have only been called during the second run.");
storm::expressions::Expression lhsExpression = *this->identifiers_.find(formulaName);
return storm::prism::Formula(lhsExpression.getBaseExpression().asVariableExpression().getVariable(), expression, this->getFilename());
} }
storm::prism::Label PrismParser::createLabel(std::string const& labelName, storm::expressions::Expression expression) const { storm::prism::Label PrismParser::createLabel(std::string const& labelName, storm::expressions::Expression expression) const {
@ -490,7 +566,7 @@ namespace storm {
std::string realActionName = actionName ? actionName.get() : ""; std::string realActionName = actionName ? actionName.get() : "";
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName); auto const& nameIndexPair = globalProgramInformation.actionIndices.find(realActionName);
STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Transition reward refers to illegal action '" << realActionName << "'.");
STORM_LOG_THROW(nameIndexPair != globalProgramInformation.actionIndices.end(), storm::exceptions::WrongFormatException, "Action reward refers to illegal action '" << realActionName << "'.");
return storm::prism::StateActionReward(nameIndexPair->second, realActionName, statePredicateExpression, rewardValueExpression, this->getFilename()); return storm::prism::StateActionReward(nameIndexPair->second, realActionName, statePredicateExpression, rewardValueExpression, this->getFilename());
} else { } else {
return storm::prism::StateActionReward(); return storm::prism::StateActionReward();
@ -556,11 +632,7 @@ namespace storm {
storm::expressions::Variable newVariable = manager->declareBooleanVariable(variableName); storm::expressions::Variable newVariable = manager->declareBooleanVariable(variableName);
this->identifiers_.add(variableName, newVariable.getExpression()); this->identifiers_.add(variableName, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) { } catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(variableName)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'.");
}
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << variableName << "'.");
} }
} }
bool observable = this->observables.count(variableName) > 0; bool observable = this->observables.count(variableName) > 0;
@ -576,11 +648,7 @@ namespace storm {
storm::expressions::Variable newVariable = manager->declareIntegerVariable(variableName); storm::expressions::Variable newVariable = manager->declareIntegerVariable(variableName);
this->identifiers_.add(variableName, newVariable.getExpression()); this->identifiers_.add(variableName, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) { } catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(variableName)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'.");
}
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << variableName << "'.");
} }
} }
bool observable = this->observables.count(variableName) > 0; bool observable = this->observables.count(variableName) > 0;
@ -597,11 +665,7 @@ namespace storm {
storm::expressions::Variable newVariable = manager->declareRationalVariable(variableName); storm::expressions::Variable newVariable = manager->declareRationalVariable(variableName);
this->identifiers_.add(variableName, newVariable.getExpression()); this->identifiers_.add(variableName, newVariable.getExpression());
} catch (storm::exceptions::InvalidArgumentException const& e) { } catch (storm::exceptions::InvalidArgumentException const& e) {
if (manager->hasVariable(variableName)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'.");
}
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": illegal identifier '" << variableName << "'.");
} }
} }
bool observable = this->observables.count(variableName) > 0; bool observable = this->observables.count(variableName) > 0;
@ -622,17 +686,52 @@ namespace storm {
return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename()); return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
} }
bool PrismParser::isValidModuleRenamingList(std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation const& globalProgramInformation) const {
if (!this->secondRun) {
auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
if (moduleIndexPair == globalProgramInformation.moduleToIndexMap.end()) {
STORM_LOG_ERROR("Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename.");
return false;
}
storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
// Check whether all varialbes are renamed.
for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
if (renamingPair == renaming.end()) {
STORM_LOG_ERROR("Parsing error in renaiming of module '" << oldModuleName << "': Boolean variable '" << variable.getName() << "' was not renamed.");
return false;
}
}
for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
if (renamingPair == renaming.end()) {
STORM_LOG_ERROR("Parsing error in renaiming of module '" << oldModuleName << "': Integer variable '" << variable.getName() << "' was not renamed.");
return false;
}
}
for (auto const& variable : moduleToRename.getClockVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
if (renamingPair == renaming.end()) {
STORM_LOG_ERROR("Parsing error in renaiming of module '" << oldModuleName << "': Clock variable '" << variable.getName() << "' was not renamed.");
return false;
}
}
}
return true;
}
storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const { storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const {
// Check whether the module to rename actually exists. // Check whether the module to rename actually exists.
auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName); auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
STORM_LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": No module named '" << oldModuleName << "' to rename.");
STORM_LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": No module named '" << oldModuleName << "' to rename.");
storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second]; storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
if (!this->secondRun) { if (!this->secondRun) {
// Register all (renamed) variables for later use. // Register all (renamed) variables for later use.
// We already checked before, whether the renaiming is valid.
for (auto const& variable : moduleToRename.getBooleanVariables()) { for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Boolean variable '" << variable.getName() << " was not renamed.");
storm::expressions::Variable renamedVariable = manager->declareBooleanVariable(renamingPair->second); storm::expressions::Variable renamedVariable = manager->declareBooleanVariable(renamingPair->second);
this->identifiers_.add(renamingPair->second, renamedVariable.getExpression()); this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
if(this->observables.count(renamingPair->second) > 0) { if(this->observables.count(renamingPair->second) > 0) {
@ -641,7 +740,7 @@ namespace storm {
} }
for (auto const& variable : moduleToRename.getIntegerVariables()) { for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Integer variable '" << variable.getName() << " was not renamed.");
storm::expressions::Variable renamedVariable = manager->declareIntegerVariable(renamingPair->second); storm::expressions::Variable renamedVariable = manager->declareIntegerVariable(renamingPair->second);
this->identifiers_.add(renamingPair->second, renamedVariable.getExpression()); this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
if(this->observables.count(renamingPair->second) > 0) { if(this->observables.count(renamingPair->second) > 0) {
@ -650,7 +749,7 @@ namespace storm {
} }
for (auto const& variable : moduleToRename.getClockVariables()) { for (auto const& variable : moduleToRename.getClockVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Clock variable '" << variable.getName() << " was not renamed.");
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Clock variable '" << variable.getName() << " was not renamed.");
storm::expressions::Variable renamedVariable = manager->declareRationalVariable(renamingPair->second); storm::expressions::Variable renamedVariable = manager->declareRationalVariable(renamingPair->second);
this->identifiers_.add(renamingPair->second, renamedVariable.getExpression()); this->identifiers_.add(renamingPair->second, renamedVariable.getExpression());
if(this->observables.count(renamingPair->second) > 0) { if(this->observables.count(renamingPair->second) > 0) {
@ -693,7 +792,7 @@ namespace storm {
std::vector<storm::prism::BooleanVariable> booleanVariables; std::vector<storm::prism::BooleanVariable> booleanVariables;
for (auto const& variable : moduleToRename.getBooleanVariables()) { for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Boolean variable '" << variable.getName() << " was not renamed.");
bool observable = this->observables.count(renamingPair->second) > 0; bool observable = this->observables.count(renamingPair->second) > 0;
if(observable) { if(observable) {
this->observables.erase(renamingPair->second); this->observables.erase(renamingPair->second);
@ -705,7 +804,7 @@ namespace storm {
std::vector<storm::prism::IntegerVariable> integerVariables; std::vector<storm::prism::IntegerVariable> integerVariables;
for (auto const& variable : moduleToRename.getIntegerVariables()) { for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Integer variable '" << variable.getName() << " was not renamed.");
bool observable = this->observables.count(renamingPair->second) > 0; bool observable = this->observables.count(renamingPair->second) > 0;
if(observable) { if(observable) {
this->observables.erase(renamingPair->second); this->observables.erase(renamingPair->second);
@ -717,7 +816,7 @@ namespace storm {
std::vector<storm::prism::ClockVariable> clockVariables; std::vector<storm::prism::ClockVariable> clockVariables;
for (auto const& variable : moduleToRename.getClockVariables()) { for (auto const& variable : moduleToRename.getClockVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); auto const& renamingPair = renaming.find(variable.getName());
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Clock variable '" << variable.getName() << " was not renamed.");
STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ": Clock variable '" << variable.getName() << " was not renamed.");
bool observable = this->observables.count(renamingPair->second) > 0; bool observable = this->observables.count(renamingPair->second) > 0;
if (observable) { if (observable) {
this->observables.erase(renamingPair->second); this->observables.erase(renamingPair->second);

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

@ -164,6 +164,11 @@ namespace storm {
*/ */
void moveToSecondRun(); void moveToSecondRun();
/*!
* Parses the stored formula Expressions.
*/
void createFormulaIdentifiers(std::vector<storm::prism::Formula>& formulas);
// A flag that stores whether the grammar is currently doing the second run. // A flag that stores whether the grammar is currently doing the second run.
bool secondRun; bool secondRun;
@ -187,6 +192,7 @@ namespace storm {
std::string const& getFilename() const; std::string const& getFilename() const;
mutable std::set<std::string> observables; mutable std::set<std::string> observables;
std::vector<std::string> formulaExpressions;
// 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;
@ -216,9 +222,11 @@ namespace storm {
qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalIntegerVariableDefinition; qi::rule<Iterator, qi::unused_type(GlobalProgramInformation&), Skipper> globalIntegerVariableDefinition;
// Rules for modules definition. // Rules for modules definition.
qi::rule<Iterator, std::vector<storm::prism::Module>(GlobalProgramInformation&), Skipper> moduleDefinitionList;
qi::rule<Iterator, std::string(), Skipper> knownModuleName;
qi::rule<Iterator, std::string(), Skipper> freshModuleName;
qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::BooleanVariable>, std::vector<storm::prism::IntegerVariable>, std::vector<storm::prism::ClockVariable>>, Skipper> moduleDefinition; qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::vector<storm::prism::BooleanVariable>, std::vector<storm::prism::IntegerVariable>, std::vector<storm::prism::ClockVariable>>, Skipper> moduleDefinition;
qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
qi::rule<Iterator, std::map<std::string, std::string>, qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenamingList;
qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::string,std::map<std::string, std::string>>, Skipper> moduleRenaming;
// Rules for variable definitions. // Rules for variable definitions.
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, qi::unused_type(std::vector<storm::prism::BooleanVariable>&, std::vector<storm::prism::IntegerVariable>&, std::vector<storm::prism::ClockVariable>&), Skipper> variableDefinition;
@ -234,6 +242,7 @@ namespace storm {
qi::rule<Iterator, storm::prism::Assignment(), Skipper> assignmentDefinition; qi::rule<Iterator, storm::prism::Assignment(), Skipper> assignmentDefinition;
// Rules for reward definitions. // Rules for reward definitions.
qi::rule<Iterator, std::string(), Skipper> freshRewardModelName;
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;
@ -263,12 +272,15 @@ namespace storm {
// Rules for label definitions. // Rules for label definitions.
qi::rule<Iterator, storm::prism::Label(), Skipper> labelDefinition; qi::rule<Iterator, storm::prism::Label(), Skipper> labelDefinition;
qi::rule<Iterator, std::string(), Skipper> freshLabelName;
// Rules for formula definitions. // Rules for formula definitions.
qi::rule<Iterator, std::string(), Skipper> formulaDefinitionRhs;
qi::rule<Iterator, storm::prism::Formula(), Skipper> formulaDefinition; qi::rule<Iterator, storm::prism::Formula(), Skipper> formulaDefinition;
// Rules for identifier parsing. // Rules for identifier parsing.
qi::rule<Iterator, std::string(), Skipper> identifier; qi::rule<Iterator, std::string(), Skipper> identifier;
qi::rule<Iterator, std::string(), Skipper> freshIdentifier;
// Parsers that recognize special keywords and model types. // Parsers that recognize special keywords and model types.
storm::parser::PrismParser::keywordsStruct keywords_; storm::parser::PrismParser::keywordsStruct keywords_;
@ -277,11 +289,16 @@ namespace storm {
// Parser and manager used for recognizing expressions. // Parser and manager used for recognizing expressions.
std::shared_ptr<storm::expressions::ExpressionManager> manager; std::shared_ptr<storm::expressions::ExpressionManager> manager;
// TODO shared?
std::shared_ptr<storm::parser::ExpressionParser> expressionParser; std::shared_ptr<storm::parser::ExpressionParser> expressionParser;
// Helper methods used in the grammar. // Helper methods used in the grammar.
bool isValidIdentifier(std::string const& identifier); bool isValidIdentifier(std::string const& identifier);
bool isFreshIdentifier(std::string const& identifier);
bool isKnownModuleName(std::string const& moduleName);
bool isFreshModuleName(std::string const& moduleName);
bool isFreshLabelName(std::string const& moduleName);
bool isFreshRewardModelName(std::string const& moduleName);
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);
void setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType); void setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType);
@ -299,7 +316,8 @@ namespace storm {
storm::prism::Constant createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) 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 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::Constant createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
storm::prism::Formula createFormula(std::string const& formulaName, storm::expressions::Expression expression);
storm::prism::Formula createFormulaFirstRun(std::string const& formulaName, std::string const& expression);
storm::prism::Formula createFormulaSecondRun(std::string const& formulaName, storm::expressions::Expression const& expression);
storm::prism::Label createLabel(std::string const& labelName, 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<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::StateActionReward> const& stateActionRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const; storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::StateActionReward> const& stateActionRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const;
storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const; storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const;

6
src/storm/storage/prism/Formula.cpp
View File

@ -10,6 +10,10 @@ namespace storm {
// Intentionally left empty. // Intentionally left empty.
} }
Formula::Formula(std::string const& name, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(name) {
// Intentionally left empty.
}
std::string const& Formula::getName() const { std::string const& Formula::getName() const {
return this->name; return this->name;
} }
@ -27,11 +31,13 @@ namespace storm {
} }
storm::expressions::Type const& Formula::getType() const { storm::expressions::Type const& Formula::getType() const {
assert(this->getExpression().isInitialized());
assert(!hasExpressionVariable() || this->getExpressionVariable().getType() == this->getExpression().getType()); assert(!hasExpressionVariable() || this->getExpressionVariable().getType() == this->getExpression().getType());
return this->getExpressionVariable().getType(); return this->getExpressionVariable().getType();
} }
Formula Formula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const { Formula Formula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
assert(this->getExpression().isInitialized());
if (hasExpressionVariable()) { if (hasExpressionVariable()) {
return Formula(this->getExpressionVariable(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); return Formula(this->getExpressionVariable(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
} else { } else {

13
src/storm/storage/prism/Formula.h
View File

@ -24,7 +24,7 @@ namespace storm {
Formula(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0); Formula(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*! /*!
* Creates a formula with the given name
* Creates a formula with the given name and the assigning expression
* *
* @param name the name of the formula. * @param name the name of the formula.
* @param expression The expression associated with this formula. * @param expression The expression associated with this formula.
@ -33,6 +33,16 @@ namespace storm {
*/ */
Formula(std::string const& name, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0); Formula(std::string const& name, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a formula with the given name
*
* @param name the name of the formula.
* @param filename The filename in which the transition reward is defined.
* @param lineNumber The line number in which the transition reward is defined.
*/
Formula(std::string const& name, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment. // Create default implementations of constructors/assignment.
Formula() = default; Formula() = default;
Formula(Formula const& other) = default; Formula(Formula const& other) = default;
@ -76,6 +86,7 @@ namespace storm {
/*! /*!
* Substitutes all variables in the expression of the formula according to the given map. * Substitutes all variables in the expression of the formula according to the given map.
* Will not substitute the placeholder variable (if given).
* *
* @param substitution The substitution to perform. * @param substitution The substitution to perform.
* @return The resulting formula. * @return The resulting formula.

Write Preview
Loading…
Cancel
Save