diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 081405a7a..ecbb946c7 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -263,14 +263,14 @@ namespace storm { 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"); - moduleRenamingList = (qi::lit("[") > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] % ",") > qi::lit("]"))[qi::_val = qi::_a]; - moduleRenamingList.name("Module renaming list"); + moduleRenaming = (qi::lit("[") > ((identifier > qi::lit("=") > identifier)[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] % ",") > qi::lit("]"))[qi::_val = phoenix::bind(&PrismParser::createModuleRenaming, phoenix::ref(*this), qi::_a)]; + moduleRenaming.name("Module renaming list"); - moduleRenaming = (((qi::lit("module") > freshModuleName) >> qi::lit("=")) + renamedModule = (((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)] + > (moduleRenaming[qi::_b = qi::_1])[qi::_pass = phoenix::bind(&PrismParser::isValidModuleRenaming, 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"); + renamedModule.name("module definition via renaming"); 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)] @@ -279,7 +279,7 @@ namespace storm { | undefinedConstantDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::constants, phoenix::ref(globalProgramInformation)), qi::_1)] | formulaDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::formulas, phoenix::ref(globalProgramInformation)), qi::_1)] | globalVariableDefinition(phoenix::ref(globalProgramInformation)) - | (moduleRenaming(phoenix::ref(globalProgramInformation)) | moduleDefinition(phoenix::ref(globalProgramInformation)))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, phoenix::ref(globalProgramInformation)), qi::_1)] + | (renamedModule(phoenix::ref(globalProgramInformation)) | moduleDefinition(phoenix::ref(globalProgramInformation)))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::modules, phoenix::ref(globalProgramInformation)), qi::_1)] | initialStatesConstruct(phoenix::ref(globalProgramInformation)) | rewardModelDefinition(phoenix::ref(globalProgramInformation))[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::rewardModels, phoenix::ref(globalProgramInformation)), qi::_1)] | labelDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::labels, phoenix::ref(globalProgramInformation)), qi::_1)] @@ -301,6 +301,7 @@ namespace storm { qi::on_success(clockVariableDefinition, setLocationInfoFunction); qi::on_success(moduleDefinition, setLocationInfoFunction); qi::on_success(moduleRenaming, setLocationInfoFunction); + qi::on_success(renamedModule, setLocationInfoFunction); qi::on_success(formulaDefinition, setLocationInfoFunction); qi::on_success(rewardModelDefinition, setLocationInfoFunction); qi::on_success(labelDefinition, setLocationInfoFunction); @@ -732,8 +733,9 @@ namespace storm { 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 const& renaming, GlobalProgramInformation const& globalProgramInformation) const { + bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const { if (!this->secondRun) { + auto const& renaming = moduleRenaming.getRenaming(); 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."); @@ -766,11 +768,16 @@ namespace storm { return true; } - storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const { + storm::prism::ModuleRenaming PrismParser::createModuleRenaming(std::map const& renaming) const { + return storm::prism::ModuleRenaming(renaming); + } + + storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation& globalProgramInformation) const { // Check whether the module to rename actually exists. auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName); 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]; + auto const& renaming = moduleRenaming.getRenaming(); if (!this->secondRun) { // Register all (renamed) variables for later use. @@ -843,7 +850,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())); + booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.hasInitialValue() ? variable.getInitialValueExpression().substitute(expressionRenaming) : variable.getInitialValueExpression(), observable, this->getFilename(), moduleRenaming.getLineNumber())); } // Rename the integer variables. @@ -855,7 +862,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())); + 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(), moduleRenaming.getLineNumber())); } // Rename the clock variables. @@ -867,7 +874,7 @@ namespace storm { if (observable) { this->observables.erase(renamingPair->second); } - clockVariables.push_back(storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename())); + clockVariables.push_back(storm::prism::ClockVariable(manager->getVariable(renamingPair->second), observable, this->getFilename(), moduleRenaming.getLineNumber())); } // Rename invariant (if present) @@ -885,12 +892,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()); + assignments.emplace_back(manager->getVariable(renamingPair->second), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), moduleRenaming.getLineNumber()); } else { - assignments.emplace_back(assignment.getVariable(), assignment.getExpression().substitute(expressionRenaming), this->getFilename()); + assignments.emplace_back(assignment.getVariable(), assignment.getExpression().substitute(expressionRenaming), this->getFilename(), moduleRenaming.getLineNumber()); } } - updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename()); + updates.emplace_back(globalProgramInformation.currentUpdateIndex, update.getLikelihoodExpression().substitute(expressionRenaming), assignments, this->getFilename(), moduleRenaming.getLineNumber()); ++globalProgramInformation.currentUpdateIndex; } @@ -910,7 +917,7 @@ namespace storm { actionIndex = nameIndexPair->second; } - commands.emplace_back(globalProgramInformation.currentCommandIndex, command.isMarkovian(), actionIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename()); + commands.emplace_back(globalProgramInformation.currentCommandIndex, command.isMarkovian(), actionIndex, newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), moduleRenaming.getLineNumber()); ++globalProgramInformation.currentCommandIndex; } diff --git a/src/storm-parsers/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h index cfadb9321..eecac5b2b 100644 --- a/src/storm-parsers/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -235,8 +235,8 @@ namespace storm { qi::rule knownModuleName; qi::rule freshModuleName; qi::rule, std::vector, std::vector>, Skipper> moduleDefinition; - qi::rule, qi::locals>, Skipper> moduleRenamingList; - qi::rule>, Skipper> moduleRenaming; + qi::rule>, Skipper> moduleRenaming; + qi::rule, Skipper> renamedModule; // Rules for variable definitions. qi::rule&, std::vector&, std::vector&), Skipper> variableDefinition; @@ -311,7 +311,7 @@ namespace storm { bool isOfBoolType(storm::expressions::Expression const& expression); bool isOfIntType(storm::expressions::Expression const& expression); bool isOfNumericalType(storm::expressions::Expression const& expression); - bool isValidModuleRenamingList(std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation const& globalProgramInformation) const; + bool isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& renaming, GlobalProgramInformation const& globalProgramInformation) const; bool addInitialStatesConstruct(storm::expressions::Expression const& initialStatesExpression, GlobalProgramInformation& globalProgramInformation); bool addSystemCompositionConstruct(std::shared_ptr const& composition, GlobalProgramInformation& globalProgramInformation); void setModelType(GlobalProgramInformation& globalProgramInformation, storm::prism::Program::ModelType const& modelType); @@ -344,7 +344,8 @@ namespace storm { storm::prism::IntegerVariable createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const; storm::prism::ClockVariable createClockVariable(std::string const& variableName) const; storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, boost::optional const& invariant, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; - storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const; + storm::prism::ModuleRenaming createModuleRenaming(std::map const& renaming) const; + storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, storm::prism::ModuleRenaming const& renaming, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; void createObservablesList(std::vector const& observables); diff --git a/src/storm/storage/prism/LocatedInformation.h b/src/storm/storage/prism/LocatedInformation.h index 9d0d6c179..0204af130 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. */ - virtual void setLineNumber(uint_fast64_t lineNumber); + 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 c89d60de6..1c11addd2 100644 --- a/src/storm/storage/prism/Module.cpp +++ b/src/storm/storage/prism/Module.cpp @@ -10,7 +10,7 @@ namespace storm { // Intentionally left empty. } - Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, storm::expressions::Expression const& invariant, std::vector const& commands, std::string const& renamedFromModule, std::map const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), clockVariables(clockVariables), clockVariableToIndexMap(), invariant(invariant), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) { + Module::Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, storm::expressions::Expression const& invariant, std::vector const& commands, std::string const& renamedFromModule, storm::prism::ModuleRenaming const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), clockVariables(clockVariables), clockVariableToIndexMap(), invariant(invariant), commands(commands), synchronizingActionIndices(), actionIndicesToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) { // Initialize the internal mappings for fast information retrieval. this->createMappings(); } @@ -126,7 +126,7 @@ namespace storm { std::map const& Module::getRenaming() const { STORM_LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve renaming of module that was not created by renaming."); - return this->renaming; + return this->renaming.getRenaming(); } std::set const& Module::getCommandIndicesByActionIndex(uint_fast64_t actionIndex) const { @@ -273,31 +273,6 @@ 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 18d730ecc..202788816 100644 --- a/src/storm/storage/prism/Module.h +++ b/src/storm/storage/prism/Module.h @@ -11,6 +11,7 @@ #include "storm/storage/prism/IntegerVariable.h" #include "storm/storage/prism/ClockVariable.h" #include "storm/storage/prism/Command.h" +#include "storm/storage/prism/ModuleRenaming.h" #include "storm/storage/BoostTypes.h" #include "storm/utility/OsDetection.h" @@ -47,7 +48,7 @@ namespace storm { * @param filename The filename in which the module is defined. * @param lineNumber The line number in which the module is defined. */ - Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, storm::expressions::Expression const& invariant, std::vector const& commands, std::string const& renamedFromModule, std::map const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); + Module(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& clockVariables, storm::expressions::Expression const& invariant, std::vector const& commands, std::string const& renamedFromModule, storm::prism::ModuleRenaming const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0); // Create default implementations of constructors/assignment. Module() = default; @@ -275,14 +276,6 @@ namespace storm { 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: /*! * Computes the locally maintained mappings for fast data retrieval. @@ -326,7 +319,7 @@ namespace storm { std::string renamedFromModule; // If the module was created by renaming, this mapping contains the provided renaming of identifiers. - std::map renaming; + storm::prism::ModuleRenaming renaming; }; } // namespace prism diff --git a/src/storm/storage/prism/ModuleRenaming.cpp b/src/storm/storage/prism/ModuleRenaming.cpp new file mode 100644 index 000000000..0d31ff4bb --- /dev/null +++ b/src/storm/storage/prism/ModuleRenaming.cpp @@ -0,0 +1,32 @@ +#include "storm/storage/prism/ModuleRenaming.h" + +namespace storm { + namespace prism { + ModuleRenaming::ModuleRenaming(std::map const& renaming) : renaming(renaming) { + // Intentionally left empty + } + + ModuleRenaming::ModuleRenaming(std::map&& renaming) : renaming(std::move(renaming)) { + // Intentionally left empty + } + + std::map const& ModuleRenaming::getRenaming() const { + return this->renaming; + } + + std::ostream& operator<<(std::ostream& stream, ModuleRenaming const& renaming) { + stream << "[ "; + bool first = true; + for (auto const& renamingPair : renaming.getRenaming()) { + stream << renamingPair.first << "=" << renamingPair.second; + if (first) { + first = false; + } else { + stream << ","; + } + } + stream << "]"; + } + + } // namespace prism +} // namespace storm diff --git a/src/storm/storage/prism/ModuleRenaming.h b/src/storm/storage/prism/ModuleRenaming.h new file mode 100644 index 000000000..88ebb69fe --- /dev/null +++ b/src/storm/storage/prism/ModuleRenaming.h @@ -0,0 +1,60 @@ +#pragma once + +#include +#include +#include +#include +#include + +#include "storm/storage/prism/BooleanVariable.h" +#include "storm/storage/prism/IntegerVariable.h" +#include "storm/storage/prism/ClockVariable.h" +#include "storm/storage/prism/Command.h" +#include "storm/storage/BoostTypes.h" +#include "storm/utility/OsDetection.h" + +namespace storm { + namespace prism { + class ModuleRenaming : public LocatedInformation { + public: + /*! + * Creates a module renaming. + * + * @param renaming The renaming of identifiers. + */ + ModuleRenaming(std::map const& renaming); + + /*! + * Creates a module renaming. + * + * @param renaming The renaming of identifiers. + */ + ModuleRenaming(std::map&& renaming); + + // Create default implementations of constructors/assignment. + ModuleRenaming() = default; + ModuleRenaming(ModuleRenaming const& other) = default; + ModuleRenaming& operator=(ModuleRenaming const& other)= default; + ModuleRenaming(ModuleRenaming&& other) = default; + ModuleRenaming& operator=(ModuleRenaming&& other) = default; + + + + /*! + * If the module was created via renaming, this method returns the applied renaming of identifiers used for + * the renaming process. + * + * @return A mapping of identifiers to new identifiers that was used in the renaming process. + */ + std::map const& getRenaming() const; + + friend std::ostream& operator<<(std::ostream& stream, ModuleRenaming const& module); + + private: + // contains the provided renaming of identifiers. + std::map renaming; + }; + + } // namespace prism +} // namespace storm +