From 3db50f570d7ad6fd2d64018b0d64658ecaa268f7 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 4 Nov 2019 12:10:13 +0100 Subject: [PATCH] PrismProgram: Correctly set line numbers for renamed modules. --- src/storm-parsers/parser/PrismParser.cpp | 14 +++++------ src/storm/storage/prism/Command.cpp | 4 ++++ src/storm/storage/prism/Command.h | 7 ++++++ src/storm/storage/prism/LocatedInformation.h | 2 +- src/storm/storage/prism/Module.cpp | 25 ++++++++++++++++++++ src/storm/storage/prism/Module.h | 8 +++++++ src/storm/storage/prism/Update.cpp | 4 ++++ src/storm/storage/prism/Update.h | 7 ++++++ 8 files changed, 63 insertions(+), 8 deletions(-) diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index dfb871194..081405a7a 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -843,7 +843,7 @@ namespace storm { if(observable) { this->observables.erase(renamingPair->second); } - booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1))); + booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename())); } // Rename the integer variables. @@ -855,7 +855,7 @@ namespace storm { if(observable) { this->observables.erase(renamingPair->second); } - integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), get_line(qi::_1))); + integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename())); } // Rename the clock variables. @@ -867,7 +867,7 @@ namespace storm { if (observable) { this->observables.erase(renamingPair->second); } - clockVariables.push_back(storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename(), get_line(qi::_1))); + clockVariables.push_back(storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename())); } // Rename invariant (if present) @@ -885,12 +885,12 @@ namespace storm { for (auto const& assignment : update.getAssignments()) { auto const& renamingPair = renaming.find(assignment.getVariableName()); if (renamingPair != renaming.end()) { - assignments.emplace_back(manager->getVariable(renamingPair->second), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); + assignments.emplace_back(manager->getVariable(renamingPair->second), assignment.getExpression().substitute(expressionRenaming), this->getFilename()); } else { - assignments.emplace_back(assignment.getVariable(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)); + assignments.emplace_back(assignment.getVariable(), assignment.getExpression().substitute(expressionRenaming), this->getFilename()); } } - updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), get_line(qi::_1)); + updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename()); ++globalProgramInformation.currentUpdateIndex; } @@ -910,7 +910,7 @@ namespace storm { actionIndex = nameIndexPair->second; } - commands.emplace_back(globalProgramInformation.currentCommandIndex, command.isMarkovian(), actionIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1)); + commands.emplace_back(globalProgramInformation.currentCommandIndex, command.isMarkovian(), actionIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename()); ++globalProgramInformation.currentCommandIndex; } diff --git a/src/storm/storage/prism/Command.cpp b/src/storm/storage/prism/Command.cpp index be40cd1eb..7ee1434d6 100644 --- a/src/storm/storage/prism/Command.cpp +++ b/src/storm/storage/prism/Command.cpp @@ -39,6 +39,10 @@ namespace storm { return this->updates; } + std::vector& Command::getUpdates() { + return this->updates; + } + uint_fast64_t Command::getGlobalIndex() const { return this->globalIndex; } diff --git a/src/storm/storage/prism/Command.h b/src/storm/storage/prism/Command.h index 983159c06..8213349ce 100644 --- a/src/storm/storage/prism/Command.h +++ b/src/storm/storage/prism/Command.h @@ -93,6 +93,13 @@ namespace storm { */ std::vector const& getUpdates() const; + /*! + * Retrieves a vector of all updates associated with this command. + * + * @return A vector of updates associated with this command. + */ + std::vector& getUpdates(); + /*! * Retrieves the global index of the command, that is, a unique index over all modules. * diff --git a/src/storm/storage/prism/LocatedInformation.h b/src/storm/storage/prism/LocatedInformation.h index 0204af130..9d0d6c179 100644 --- a/src/storm/storage/prism/LocatedInformation.h +++ b/src/storm/storage/prism/LocatedInformation.h @@ -51,7 +51,7 @@ namespace storm { * * @param lineNumber The new line number for this information. */ - void setLineNumber(uint_fast64_t lineNumber); + virtual void setLineNumber(uint_fast64_t lineNumber); private: // The file in which the piece of information was found. diff --git a/src/storm/storage/prism/Module.cpp b/src/storm/storage/prism/Module.cpp index 265fa27ec..c89d60de6 100644 --- a/src/storm/storage/prism/Module.cpp +++ b/src/storm/storage/prism/Module.cpp @@ -273,6 +273,31 @@ namespace storm { return this->invariant; } + void Module::setLineNumber(uint_fast64_t lineNumber) { + LocatedInformation::setLineNumber(lineNumber); + // Also set the line number of the components of the module, in case of a renaming. + if (isRenamedFromModule()) { + for (auto& v : booleanVariables) { + v.setLineNumber(lineNumber); + } + for (auto& v : integerVariables) { + v.setLineNumber(lineNumber); + } + for (auto& v : clockVariables) { + v.setLineNumber(lineNumber); + } + for (auto& c : commands) { + c.setLineNumber(lineNumber); + for (auto& u : c.getUpdates()) { + u.setLineNumber(lineNumber); + for (auto& a : u.getAssignments()) { + a.setLineNumber(lineNumber); + } + } + } + } + } + std::ostream& operator<<(std::ostream& stream, Module const& module) { stream << "module " << module.getName() << std::endl; for (auto const& booleanVariable : module.getBooleanVariables()) { diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h index 27d9551ac..18d730ecc 100644 --- a/src/storm/storage/prism/Module.h +++ b/src/storm/storage/prism/Module.h @@ -274,6 +274,14 @@ namespace storm { storm::expressions::Expression const& getInvariant() const; friend std::ostream& operator<<(std::ostream& stream, Module const& module); + + /*! + * Sets the line number of this module. + * If this is a renamed module, the line number of all the stored components will be set as well. + * + * @param lineNumber The new line number for this information. + */ + virtual void setLineNumber(uint_fast64_t lineNumber) override; private: /*! diff --git a/src/storm/storage/prism/Update.cpp b/src/storm/storage/prism/Update.cpp index 0d1fce1ce..832adae6f 100644 --- a/src/storm/storage/prism/Update.cpp +++ b/src/storm/storage/prism/Update.cpp @@ -33,6 +33,10 @@ namespace storm { return this->assignments; } + std::vector& Update::getAssignments() { + return this->assignments; + } + storm::prism::Assignment const& Update::getAssignment(std::string const& variableName) const { auto const& variableIndexPair = this->variableToAssignmentIndexMap.find(variableName); STORM_LOG_THROW(variableIndexPair != this->variableToAssignmentIndexMap.end(), storm::exceptions::OutOfRangeException, "Variable '" << variableName << "' is not assigned in update."); diff --git a/src/storm/storage/prism/Update.h b/src/storm/storage/prism/Update.h index b27ddfff4..8f752a207 100644 --- a/src/storm/storage/prism/Update.h +++ b/src/storm/storage/prism/Update.h @@ -50,6 +50,13 @@ namespace storm { */ std::vector const& getAssignments() const; + /*! + * Retrieves a reference to the map of variable names to their respective assignments. + * + * @return A reference to the map of variable names to their respective assignments. + */ + std::vector& getAssignments(); + /*! * Retrieves a reference to the assignment for the variable with the given name. *