Browse Source

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
master
Dave Parker 10 years ago
parent
commit
9e18844a26
  1. 6
      prism/src/simulator/ModulesFileModelGenerator.java

6
prism/src/simulator/ModulesFileModelGenerator.java

@ -83,13 +83,13 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator
*/ */
private void initialise() throws PrismLangException 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 // Get info
varList = modulesFile.createVarList(); varList = modulesFile.createVarList();
labelList = modulesFile.getLabelList(); 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 // Create data structures for exploring model
updater = new Updater(modulesFile, varList, parent); updater = new Updater(modulesFile, varList, parent);
transitionList = new TransitionList(); transitionList = new TransitionList();

Loading…
Cancel
Save