diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index 57bc7820..5af18f9e 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/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 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 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) { diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index d211e924..2cc0ca3c 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/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(); diff --git a/prism/src/explicit/QuantAbstractRefineExample.java b/prism/src/explicit/QuantAbstractRefineExample.java index be9ebf31..05474b39 100644 --- a/prism/src/explicit/QuantAbstractRefineExample.java +++ b/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]); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 7e051754..c1303463 100644 --- a/prism/src/prism/Prism.java +++ b/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();