From 9e18844a2690efc0eec7cfed51ea50ca2d9b5faa Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 3 Dec 2015 19:52:29 +0000 Subject: [PATCH] Bug fix in ModulesFileModelGenerator: need to make sure model constants are expanded in labels. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10977 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/simulator/ModulesFileModelGenerator.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 94651ff6..4afd7a57 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -83,13 +83,13 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator */ private void initialise() throws PrismLangException { + // Evaluate constants and optimise (a copy of) the model for analysis + modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(mfConstants).simplify(); + // Get info varList = modulesFile.createVarList(); labelList = modulesFile.getLabelList(); - // Evaluate constants and optimise (a copy of) the model for analysis - modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(mfConstants).simplify(); - // Create data structures for exploring model updater = new Updater(modulesFile, varList, parent); transitionList = new TransitionList();