Merge branch 'master' into deterministicScheds

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<std::pair<std::string,std::string>>(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<std::pair<std::string,std::string>>(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<std::string, std::string> 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<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const {
+        storm::prism::ModuleRenaming PrismParser::createModuleRenaming(std::map<std::string,std::string> 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;
                 }
                 

src/storm-parsers/parser/PrismParser.h

@@ -235,8 +235,8 @@ namespace storm {
             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, 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;
+            qi::rule<Iterator, storm::prism::ModuleRenaming, qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
+            qi::rule<Iterator, storm::prism::Module(GlobalProgramInformation&), qi::locals<std::string, storm::prism::ModuleRenaming>, Skipper> renamedModule;
             
             // 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;
@@ -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<std::string, std::string> 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<storm::prism::Composition> 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<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, boost::optional<storm::expressions::Expression> const& invariant, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
-            storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const;
+            storm::prism::ModuleRenaming createModuleRenaming(std::map<std::string,std::string> 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<std::string> const& observables);
 

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.

src/storm/storage/prism/Module.cpp

@@ -10,7 +10,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> 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<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> 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<std::string, std::string> 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<uint_fast64_t> 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()) {

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<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+            Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::ClockVariable> const& clockVariables, storm::expressions::Expression const& invariant, std::vector<storm::prism::Command> 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<std::string, std::string> renaming;
+            storm::prism::ModuleRenaming renaming;
         };
         
     } // namespace prism

src/storm/storage/prism/ModuleRenaming.cpp

@@ -0,0 +1,32 @@
+#include "storm/storage/prism/ModuleRenaming.h"
+
+namespace storm {
+    namespace prism {
+        ModuleRenaming::ModuleRenaming(std::map<std::string,std::string> const& renaming) : renaming(renaming) {
+            // Intentionally left empty
+        }
+        
+        ModuleRenaming::ModuleRenaming(std::map<std::string,std::string>&& renaming) : renaming(std::move(renaming)) {
+            // Intentionally left empty
+        }
+
+        std::map<std::string, std::string> 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

src/storm/storage/prism/ModuleRenaming.h

@@ -0,0 +1,60 @@
+#pragma once
+
+#include <set>
+#include <map>
+#include <string>
+#include <vector>
+#include <memory>
+
+#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<std::string,std::string> const& renaming);
+            
+            /*!
+             * Creates a module renaming.
+             *
+             * @param renaming The renaming of identifiers.
+             */
+            ModuleRenaming(std::map<std::string,std::string>&& 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<std::string, std::string> const& getRenaming() const;
+            
+            friend std::ostream& operator<<(std::ostream& stream, ModuleRenaming const& module);
+            
+        private:
+            // contains the provided renaming of identifiers.
+            std::map<std::string, std::string> renaming;
+        };
+        
+    } // namespace prism
+} // namespace storm
+