Browse Source

Make sure Prism takes care of clear()ing models.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4568 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 14 years ago
parent
commit
b840d7f3a3
  1. 24
      prism/src/prism/Prism.java
  2. 3
      prism/src/prism/PrismCL.java

24
prism/src/prism/Prism.java

@ -1400,6 +1400,8 @@ public class Prism implements PrismSettingsListener
currentModelSource = ModelSource.PRISM_MODEL; currentModelSource = ModelSource.PRISM_MODEL;
// Store PRISM model // Store PRISM model
currentModulesFile = modulesFile; currentModulesFile = modulesFile;
// Clear any existing built model(s)
clearBuiltModel();
// Reset dependent info // Reset dependent info
currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType(); currentModelType = currentModulesFile == null ? null : currentModulesFile.getModelType();
currentDefinedMFConstants = null; currentDefinedMFConstants = null;
@ -1444,6 +1446,8 @@ public class Prism implements PrismSettingsListener
if (currentDefinedMFConstants != null && currentDefinedMFConstants.equals(definedMFConstants)) if (currentDefinedMFConstants != null && currentDefinedMFConstants.equals(definedMFConstants))
return; return;
// Clear any existing built model(s)
clearBuiltModel();
// Store constants here and in ModulesFile // Store constants here and in ModulesFile
currentDefinedMFConstants = definedMFConstants; currentDefinedMFConstants = definedMFConstants;
currentModulesFile.setUndefinedConstants(definedMFConstants); currentModulesFile.setUndefinedConstants(definedMFConstants);
@ -1474,6 +1478,8 @@ public class Prism implements PrismSettingsListener
public void loadPRISMModelAndBuiltModel(ModulesFile modulesFile, Model model) public void loadPRISMModelAndBuiltModel(ModulesFile modulesFile, Model model)
{ {
currentModelSource = ModelSource.PRISM_MODEL; currentModelSource = ModelSource.PRISM_MODEL;
// Clear any existing built model(s)
clearBuiltModel();
// Store model info // Store model info
currentModulesFile = modulesFile; currentModulesFile = modulesFile;
currentModel = model; currentModel = model;
@ -1492,6 +1498,8 @@ public class Prism implements PrismSettingsListener
public void loadBuiltModel(Model model) public void loadBuiltModel(Model model)
{ {
currentModelSource = ModelSource.BUILT_MODEL; currentModelSource = ModelSource.BUILT_MODEL;
// Clear any existing built model(s)
clearBuiltModel();
// Store model info // Store model info
currentModulesFile = null; currentModulesFile = null;
currentModel = model; currentModel = model;
@ -1512,6 +1520,8 @@ public class Prism implements PrismSettingsListener
public ModulesFile loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException public ModulesFile loadModelFromExplicitFiles(File statesFile, File transFile, File labelsFile, ModelType typeOverride) throws PrismException
{ {
currentModelSource = ModelSource.EXPLICIT_FILES; currentModelSource = ModelSource.EXPLICIT_FILES;
// Clear any existing built model(s)
clearBuiltModel();
// Create ExplicitFiles2MTBDD object and build state space // Create ExplicitFiles2MTBDD object and build state space
expf2mtbdd = new ExplicitFiles2MTBDD(this, statesFile, transFile, labelsFile, typeOverride); expf2mtbdd = new ExplicitFiles2MTBDD(this, statesFile, transFile, labelsFile, typeOverride);
currentModulesFile = expf2mtbdd.buildStates(); currentModulesFile = expf2mtbdd.buildStates();
@ -1611,6 +1621,9 @@ public class Prism implements PrismSettingsListener
{ {
long l; // timer long l; // timer
// Clear any existing built model(s)
clearBuiltModel();
try { try {
if (currentModulesFile == null) if (currentModulesFile == null)
throw new PrismException("There is no currently loaded PRISM model to build"); throw new PrismException("There is no currently loaded PRISM model to build");
@ -2677,15 +2690,14 @@ public class Prism implements PrismSettingsListener
} }
/** /**
* Clear the built model (free/deallocate memory etc)
* Clear the built model if needed (free/deallocate memory etc)
*/ */
public void clearBuiltModel()
private void clearBuiltModel()
{ {
if (currentModel != null) if (currentModel != null)
currentModel.clear(); currentModel.clear();
// TODO: if (currentModelExpl != null)
//currentModelExpl.clear();
loadBuiltModel(null);
/*if (currentModelExpl != null)
currentModelExpl.clear();*/
} }
/** /**
@ -2702,6 +2714,8 @@ public class Prism implements PrismSettingsListener
*/ */
public void closeDown(boolean check) public void closeDown(boolean check)
{ {
// Clear any built model(s)
clearBuiltModel();
// Close down engines // Close down engines
PrismMTBDD.closeDown(); PrismMTBDD.closeDown();
PrismSparse.closeDown(); PrismSparse.closeDown();

3
prism/src/prism/PrismCL.java

@ -345,9 +345,6 @@ public class PrismCL
} }
} }
// clear model
prism.clearBuiltModel();
// iterate to next model // iterate to next model
undefinedMFConstants.iterateModel(); undefinedMFConstants.iterateModel();
for (j = 0; j < numPropertiesToCheck; j++) { for (j = 0; j < numPropertiesToCheck; j++) {

Loading…
Cancel
Save