From 584fbf23c1d69b9ed6c23a96743c157b98075e78 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Thu, 13 Aug 2020 18:49:53 +0200
Subject: [PATCH] add assertion for module indices in second

---
 src/storm-parsers/parser/PrismParser.cpp | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp
index 0368d843c..a9bd43547 100644
--- a/src/storm-parsers/parser/PrismParser.cpp
+++ b/src/storm-parsers/parser/PrismParser.cpp
@@ -755,12 +755,16 @@ namespace storm {
             this->observables.insert(observables.begin(), observables.end());
             // We need this list to be filled in both runs.
         }
-        
+
         storm::prism::Module PrismParser::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 {
-            globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
+            if (!this->secondRun) {
+                globalProgramInformation.moduleToIndexMap[moduleName] = globalProgramInformation.modules.size();
+            } else {
+                STORM_LOG_THROW(globalProgramInformation.moduleToIndexMap[moduleName] == globalProgramInformation.modules.size(), storm::exceptions::WrongFormatException, "Internal error while parsing: the index for module " << moduleName << " does not match the on in the first run.");
+            }
             return storm::prism::Module(moduleName, booleanVariables, integerVariables, clockVariables, invariant.is_initialized()? invariant.get() : storm::expressions::Expression(), commands, this->getFilename());
         }
-        
+
         bool PrismParser::isValidModuleRenaming(std::string const& oldModuleName, storm::prism::ModuleRenaming const& moduleRenaming, GlobalProgramInformation const& globalProgramInformation) const {
             if (!this->secondRun) {
                 auto const& renaming = moduleRenaming.getRenaming();