From faa8e1e51fc409e26efcd3cff3d8e68aa43e4b18 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Tue, 9 Feb 2016 16:19:26 +0000 Subject: [PATCH] ModulesFileModelGenerator: fix constant evaluation in explicit engine when built from GUI [with Steffen Maercker] When building a model from the GUI with the explicit engine, constant were sometimes not updated correctly: (1) Open xprism, switch to explicit engine (2) Load a model with undefined constants, e.g., brp.pm (3) Build the model, setting constants (e.g., 2 and 3) (4) Build the model again, setting *other* constants (e.g., 22 and 3) In step (4), the log file reflects the changed constants, but the generated model has the same number of states as in step (3) and is fact built with the constants of step (3). The cause: If the PRISM file is not reloaded, then the currentModelGenerator remains the same. In ModulesFileModelGenerator.initialise(), called from setSomeUndefinedConstants() in step (3), the modulesFile is overwritten with the modulesFile where the constants set in step (3) have been replaced in the AST with the concrete values. In step (4), there are no more AST-elements with undefined constants and hence the modules file does not reflect the changed constants when the constants in the constant list are changed. The fix is to keep a copy of the original modules file in the ModulesFileModelGenerator which is freshly deepCopyied and processed in the subsequent calls to initialise(). Regression introduced in SVN r10996 when switching to the ModulesFileModelGenerator infrastructure. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11159 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../src/simulator/ModulesFileModelGenerator.java | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/prism/src/simulator/ModulesFileModelGenerator.java b/prism/src/simulator/ModulesFileModelGenerator.java index 753d74c9..91c9a5b7 100644 --- a/prism/src/simulator/ModulesFileModelGenerator.java +++ b/prism/src/simulator/ModulesFileModelGenerator.java @@ -23,6 +23,9 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator protected PrismComponent parent; // PRISM model info + /** The original modules file (might have unresolved constants) */ + private ModulesFile originalModulesFile; + /** The modules file used for generating (has no unresolved constants after {@code initialise}) */ private ModulesFile modulesFile; private ModelType modelType; private Values mfConstants; @@ -68,6 +71,7 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator // Store basic model info this.modulesFile = modulesFile; + this.originalModulesFile = modulesFile; modelType = modulesFile.getModelType(); // If there are no constants to define, go ahead and initialise; @@ -79,12 +83,12 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator } /** - * Initialise the class ready for model exploration + * (Re-)Initialise the class ready for model exploration * (can only be done once any constants needed have been provided) */ private void initialise() throws PrismLangException { - // Evaluate constants and optimise (a copy of) the model for analysis + // Evaluate constants on (a copy) of the modules file, insert constant values and optimize arithmetic expressions modulesFile = (ModulesFile) modulesFile.deepCopy().replaceConstants(mfConstants).simplify(); // Get info @@ -108,6 +112,13 @@ public class ModulesFileModelGenerator extends DefaultModelGenerator @Override public void setSomeUndefinedConstants(Values someValues) throws PrismException { + // We start again with a copy of the original modules file + // and set the constants in the copy. + // As {@code initialise()} can replace references to constants + // with the concrete values in modulesFile, this ensures that we + // start again at a place where references to constants have not + // yet been replaced. + modulesFile = (ModulesFile) originalModulesFile.deepCopy(); modulesFile.setSomeUndefinedConstants(someValues); mfConstants = modulesFile.getConstantValues(); initialise();