Browse Source

Switch ConstructModel class to PrismComponent interface.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7238 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 13 years ago
parent
commit
e109eadf71
  1. 15
      prism/src/explicit/ConstructModel.java
  2. 2
      prism/src/explicit/PrismExplicit.java
  3. 2
      prism/src/explicit/QuantAbstractRefineExample.java
  4. 4
      prism/src/prism/Prism.java

15
prism/src/explicit/ConstructModel.java

@ -38,6 +38,7 @@ import parser.VarList;
import parser.ast.ModulesFile;
import prism.ModelType;
import prism.Prism;
import prism.PrismComponent;
import prism.PrismException;
import prism.PrismLog;
import prism.PrismPrintStreamLog;
@ -45,11 +46,10 @@ import prism.ProgressDisplay;
import prism.UndefinedConstants;
import simulator.SimulatorEngine;
public class ConstructModel
public class ConstructModel extends PrismComponent
{
// The simulator engine and a log for output
// The simulator engine
private SimulatorEngine engine;
private PrismLog mainLog;
// Options:
// Find deadlocks during model construction?
@ -57,16 +57,13 @@ public class ConstructModel
// Automatically fix deadlocks?
private boolean fixDeadlocks = true;
// Basic info needed about model
// private ModelType modelType;
// Details of built model
private List<State> statesList;
public ConstructModel(SimulatorEngine engine, PrismLog mainLog)
public ConstructModel(PrismComponent parent, SimulatorEngine engine) throws PrismException
{
super(parent);
this.engine = engine;
this.mainLog = mainLog;
}
public List<State> getStatesList()
@ -338,7 +335,7 @@ public class ConstructModel
if (args.length > 2)
undefinedConstants.defineUsingConstSwitch(args[2]);
modulesFile.setUndefinedConstants(undefinedConstants.getMFConstantValues());
ConstructModel constructModel = new ConstructModel(prism.getSimulator(), mainLog);
ConstructModel constructModel = new ConstructModel(prism, prism.getSimulator());
Model model = constructModel.constructModel(modulesFile);
model.exportToPrismExplicitTra(args[1]);
} catch (FileNotFoundException e) {

2
prism/src/explicit/PrismExplicit.java

@ -67,7 +67,7 @@ public class PrismExplicit extends PrismComponent
mainLog.print("\nBuilding model...\n");
// create translator
constructModel = new ConstructModel(simEngine, mainLog);
constructModel = new ConstructModel(this, simEngine);
// build model
l = System.currentTimeMillis();

2
prism/src/explicit/QuantAbstractRefineExample.java

@ -317,7 +317,7 @@ public class QuantAbstractRefineExample extends QuantAbstractRefine
modulesFile = (ModulesFile) modulesFile.deepCopy().expandConstants(modulesFile.getConstantList());
// Build the model (explicit-state reachability)
ConstructModel constructModel = new ConstructModel(prism.getSimulator(), mainLog);
ConstructModel constructModel = new ConstructModel(prism, prism.getSimulator());
ModelSimple model = (ModelSimple) constructModel.constructModel(modulesFile, false, false);
model.exportToPrismExplicitTra(args[1]);

4
prism/src/prism/Prism.java

@ -1804,7 +1804,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
currentModel = mod2mtbdd.translate();
currentModelExpl = null;
} else {
ConstructModel constructModel = new ConstructModel(getSimulator(), mainLog);
ConstructModel constructModel = new ConstructModel(this, getSimulator());
constructModel.setFixDeadlocks(getFixDeadlocks());
currentModelExpl = constructModel.constructModel(currentModulesFile, false, true);
currentModel = null;
@ -1957,7 +1957,7 @@ public class Prism extends PrismComponent implements PrismSettingsListener
if (currentDefinedMFConstants != null && currentDefinedMFConstants.getNumValues() > 0)
mainLog.println("Model constants: " + currentDefinedMFConstants);
constructModel = new ConstructModel(getSimulator(), mainLog);
constructModel = new ConstructModel(this, getSimulator());
modelExpl = constructModel.constructModel(modulesFile);
statesList = constructModel.getStatesList();

Loading…
Cancel
Save