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

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();