From 1cf2e544ac047e53ce0ab3befd2bfc9339ccc9bb Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Thu, 13 Aug 2020 18:49:53 +0200 Subject: [PATCH] add assertion for module indices in second --- src/storm-parsers/parser/PrismParser.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm-parsers/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp index 46b644982..e039f6cbb 100644 --- a/src/storm-parsers/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -778,7 +778,11 @@ namespace storm { } storm::prism::Module PrismParser::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 { - 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()); }