s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Prism: reset currentModel and currentModelExpl to null in clearBuiltModel() 

Generally, as soon as clearBuiltModel is called, the models should not be
touched anymore. In doBuildModel, keep the null assignments for the
model storage variable for the unused engine.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11825 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Joachim Klein 9 years ago
parent
3d48780b8d
commit
16bbd0b24b
1 changed files with 6 additions and 16 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 22
      prism/src/prism/Prism.java

22
prism/src/prism/Prism.java
View File

@ -1689,8 +1689,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType(); currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
currentModelInfo = currentModulesFile; currentModelInfo = currentModulesFile;
currentDefinedMFConstants = null; currentDefinedMFConstants = null;
currentModel = null;
currentModelExpl = null;
// Print basic model info // Print basic model info
mainLog.println("\nType: " + currentModulesFile.getModelType()); mainLog.println("\nType: " + currentModulesFile.getModelType());
@ -1736,8 +1734,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
currentModelType = currentModelGenerator == null ? null : currentModelGenerator.getModelType(); currentModelType = currentModelGenerator == null ? null : currentModelGenerator.getModelType();
currentModelInfo = currentModelGenerator; currentModelInfo = currentModelGenerator;
currentDefinedMFConstants = null; currentDefinedMFConstants = null;
currentModel = null;
currentModelExpl = null;
// Print basic model info // Print basic model info
mainLog.println("\nGenerator: " + currentModelGenerator.getClass().getName()); mainLog.println("\nGenerator: " + currentModelGenerator.getClass().getName());
@ -1768,9 +1764,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
if (currentModelGenerator != null) { if (currentModelGenerator != null) {
currentModelGenerator.setSomeUndefinedConstants(definedMFConstants); currentModelGenerator.setSomeUndefinedConstants(definedMFConstants);
} }
// Reset dependent info
currentModel = null;
currentModelExpl = null;
// If required, export parsed PRISM model, with constants expanded // If required, export parsed PRISM model, with constants expanded
if (exportPrismConst) { if (exportPrismConst) {
@ -1804,7 +1797,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType(); currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
currentModelInfo = currentModulesFile; currentModelInfo = currentModulesFile;
currentDefinedMFConstants = null; currentDefinedMFConstants = null;
currentModelExpl = null;
} }
/** /**
@ -1824,7 +1816,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
// Reset dependent info // Reset dependent info
currentModelType = currentModel == null ? null : currentModel.getModelType(); currentModelType = currentModel == null ? null : currentModel.getModelType();
currentDefinedMFConstants = null; currentDefinedMFConstants = null;
currentModelExpl = null;
} }
/** /**
@ -1854,8 +1845,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType(); currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
currentModelInfo = currentModulesFile; currentModelInfo = currentModulesFile;
currentDefinedMFConstants = null; currentDefinedMFConstants = null;
currentModel = null;
currentModelExpl = null;
return currentModulesFile; return currentModulesFile;
} }
@ -2909,8 +2898,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener
currentModelType = ModelType.MDP; currentModelType = ModelType.MDP;
currentModelGenerator = new ModulesFileModelGenerator(currentModulesFile, this); currentModelGenerator = new ModulesFileModelGenerator(currentModulesFile, this);
clearBuiltModel(); clearBuiltModel();
currentModel = null;
currentModelExpl = null;
// If required, export generated PRISM model // If required, export generated PRISM model
if (exportDigital) { if (exportDigital) {
try { try {
@ -3610,13 +3597,16 @@ public class Prism extends PrismComponent implements PrismSettingsListener
/** /**
* Clear the built model if needed (free/deallocate memory etc) * Clear the built model if needed (free/deallocate memory etc)
* <br>
* Resets {@code currentModel} and {@code currentModelExpl} to {@code null}.
*/ */
private void clearBuiltModel() private void clearBuiltModel()
{ {
if (currentModel != null)
if (currentModel != null) {
currentModel.clear(); currentModel.clear();
/*if (currentModelExpl != null)
currentModelExpl.clear();*/
currentModel = null;
}
currentModelExpl = null;
} }
/** /**

Write Preview
Loading…
Cancel
Save