From b6828a7045c59fc1f538c477ba34f9e3c72e6669 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 22 Dec 2015 13:40:26 +0000 Subject: [PATCH] Remove unused "techLog" from Prism object and other classes. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11078 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/etc/scripts/prism-auto | 4 +- prism/src/explicit/ConstructModel.java | 2 +- prism/src/explicit/PrismExplicit.java | 4 +- .../explicit/QuantAbstractRefineExample.java | 2 +- prism/src/prism/ExplicitModel2MTBDD.java | 2 - prism/src/prism/Modules2MTBDD.java | 2 - prism/src/prism/Preprocessor.java | 4 +- prism/src/prism/Prism.java | 57 +++++-------------- prism/src/prism/PrismCL.java | 22 +------ prism/src/prism/PrismTest.java | 2 +- prism/src/prism/StateModelChecker.java | 3 - prism/src/userinterface/GUIPrism.java | 2 +- 12 files changed, 26 insertions(+), 80 deletions(-) diff --git a/prism/etc/scripts/prism-auto b/prism/etc/scripts/prism-auto index 6251d49d..a302ee67 100755 --- a/prism/etc/scripts/prism-auto +++ b/prism/etc/scripts/prism-auto @@ -330,13 +330,13 @@ def runPrism(args, dir=""): if options.logDir: logFile = os.path.join(options.logDir, createLogFileName(args, dir)) #f = open(logFile, 'w') - prismArgs = prismArgs + ['-mainlog', logFile, '-techlog', logFile] + prismArgs = prismArgs + ['-mainlog', logFile] exitCode = subprocess.Popen(prismArgs).wait() #exitCode = subprocess.Popen(prismArgs, cwd=dir, stdout=f).wait() elif options.test: f = tempfile.NamedTemporaryFile(delete=False) logFile = f.name - prismArgs = prismArgs + ['-mainlog', logFile, '-techlog', logFile] + prismArgs = prismArgs + ['-mainlog', logFile] exitCode = subprocess.Popen(prismArgs).wait() else: exitCode = subprocess.Popen(prismArgs).wait() diff --git a/prism/src/explicit/ConstructModel.java b/prism/src/explicit/ConstructModel.java index b5d98f25..bd1c8e8e 100644 --- a/prism/src/explicit/ConstructModel.java +++ b/prism/src/explicit/ConstructModel.java @@ -395,7 +395,7 @@ public class ConstructModel extends PrismComponent try { // Simple example: parse a PRISM file from a file, construct the model and export to a .tra file PrismLog mainLog = new PrismPrintStreamLog(System.out); - Prism prism = new Prism(mainLog, mainLog); + Prism prism = new Prism(mainLog); parser.ast.ModulesFile modulesFile = prism.parseModelFile(new File(args[0])); UndefinedConstants undefinedConstants = new UndefinedConstants(modulesFile, null); if (args.length > 2) diff --git a/prism/src/explicit/PrismExplicit.java b/prism/src/explicit/PrismExplicit.java index b68eb6da..f35e90fa 100644 --- a/prism/src/explicit/PrismExplicit.java +++ b/prism/src/explicit/PrismExplicit.java @@ -430,7 +430,7 @@ public class PrismExplicit extends PrismComponent Prism prism; try { PrismLog mainLog = new PrismFileLog("stdout"); - prism = new Prism(mainLog, mainLog); + prism = new Prism(mainLog); //prism.initialise(); ModulesFile modulesFile = prism.parseModelFile(new File(args[0])); modulesFile.setUndefinedConstants(null); @@ -454,7 +454,7 @@ public class PrismExplicit extends PrismComponent Prism prism; try { PrismLog log = new PrismFileLog("stdout"); - prism = new Prism(log, log); + prism = new Prism(log); prism.initialise(); prism.setDoProbChecks(false); ModulesFile modulesFile = prism.parseModelFile(new File(args[0])); diff --git a/prism/src/explicit/QuantAbstractRefineExample.java b/prism/src/explicit/QuantAbstractRefineExample.java index da207ad9..060c3ca2 100644 --- a/prism/src/explicit/QuantAbstractRefineExample.java +++ b/prism/src/explicit/QuantAbstractRefineExample.java @@ -320,7 +320,7 @@ public class QuantAbstractRefineExample extends QuantAbstractRefine try { // Load/parse a PRISM model description PrismLog mainLog = new PrismPrintStreamLog(System.out); - Prism prism = new Prism(mainLog, mainLog); + Prism prism = new Prism(mainLog); ModulesFile modulesFile = prism.parseModelFile(new File(args[0])); UndefinedConstants undefinedConstants = new UndefinedConstants(modulesFile, null); undefinedConstants.defineUsingConstSwitch(""); diff --git a/prism/src/prism/ExplicitModel2MTBDD.java b/prism/src/prism/ExplicitModel2MTBDD.java index 357969b1..5eab016e 100644 --- a/prism/src/prism/ExplicitModel2MTBDD.java +++ b/prism/src/prism/ExplicitModel2MTBDD.java @@ -43,7 +43,6 @@ public class ExplicitModel2MTBDD // logs private PrismLog mainLog; // main log - private PrismLog techLog; // tech log // Explicit-state model private explicit.Model modelExpl; @@ -100,7 +99,6 @@ public class ExplicitModel2MTBDD { this.prism = prism; mainLog = prism.getMainLog(); - techLog = prism.getTechLog(); } // Build model diff --git a/prism/src/prism/Modules2MTBDD.java b/prism/src/prism/Modules2MTBDD.java index 9207b312..1292f2ef 100644 --- a/prism/src/prism/Modules2MTBDD.java +++ b/prism/src/prism/Modules2MTBDD.java @@ -46,7 +46,6 @@ public class Modules2MTBDD // logs private PrismLog mainLog; // main log - private PrismLog techLog; // tech log // ModulesFile object to store syntax tree from parser private ModulesFile modulesFile; @@ -161,7 +160,6 @@ public class Modules2MTBDD { prism = p; mainLog = p.getMainLog(); - techLog = p.getTechLog(); modulesFile = mf; // get symmetry reduction info String s = prism.getSettings().getString(PrismSettings.PRISM_SYMM_RED_PARAMS); diff --git a/prism/src/prism/Preprocessor.java b/prism/src/prism/Preprocessor.java index 2c2fcb17..859982d1 100644 --- a/prism/src/prism/Preprocessor.java +++ b/prism/src/prism/Preprocessor.java @@ -461,9 +461,7 @@ public class Preprocessor public static void main(String[] args) { if (args.length < 1) return; - PrismLog pl1 = new PrismFileLog("stdout"); - PrismLog pl2 = new PrismFileLog("stdout"); - Prism p = new Prism(pl1, pl2); + Prism p = new Prism(new PrismFileLog("stdout")); try { Preprocessor pp = new Preprocessor(p, new File(args[0])); pp.setParameters(args); diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 6c357ca0..ba4f2062 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -219,12 +219,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener // Method to use for (symbolic) state-space reachability private int reachMethod = REACH_BFS; - //------------------------------------------------------------------------------ - // Logs - //------------------------------------------------------------------------------ - - private PrismLog techLog; // log for technical/diagnostic output - //------------------------------------------------------------------------------ // Parsers/translators/model checkers/simulators/etc. //------------------------------------------------------------------------------ @@ -285,20 +279,8 @@ public class Prism extends PrismComponent implements PrismSettingsListener */ public Prism(PrismLog mainLog) { - this(mainLog, mainLog); - } - - /** - * Construct a new Prism object. - * @param mainLog PrismLog where messages and model checking output will be sent. - * @param techLog PrismLog for output of detailed technical info (not really used). - */ - public Prism(PrismLog mainLog, PrismLog techLog) - { - // set up logs + // set up log this.mainLog = mainLog; - this.techLog = techLog; - // set up some default options settings = new PrismSettings(); // add this Prism object as a results listener @@ -307,6 +289,15 @@ public class Prism extends PrismComponent implements PrismSettingsListener modelListeners = new ArrayList(); } + /** + * Construct a new Prism object. + * @deprecated ({@code techLog} is no longer used, use the {@link #prism.Prism(PrismLog)} constructor instead). + */ + public Prism(PrismLog mainLog, PrismLog techLog) + { + this(mainLog); + } + /** * Read in PRISM settings from the default file (.prism in user's home directory). * If no file exists, attempt to create a new one with default settings. @@ -352,25 +343,12 @@ public class Prism extends PrismComponent implements PrismSettingsListener // store new log mainLog = l; // pass to other components + JDD.SetOutputStream(mainLog.getFilePointer()); PrismMTBDD.setMainLog(mainLog); PrismSparse.setMainLog(mainLog); PrismHybrid.setMainLog(mainLog); } - /** - * Set the PrismLog for output of detailed technical info (not really used). - */ - public void setTechLog(PrismLog l) - { - // store new log - techLog = l; - // pass to other components - JDD.SetOutputStream(techLog.getFilePointer()); - PrismMTBDD.setTechLog(techLog); - PrismSparse.setTechLog(techLog); - PrismHybrid.setTechLog(techLog); - } - // Set methods for main prism settings // (provided for convenience and for compatibility with old code) @@ -687,11 +665,6 @@ public class Prism extends PrismComponent implements PrismSettingsListener return mainLog; } - public PrismLog getTechLog() - { - return techLog; - } - public PrismSettings getSettings() { return settings; @@ -1313,13 +1286,13 @@ public class Prism extends PrismComponent implements PrismSettingsListener long cuddMaxMem = PrismUtils.convertMemoryStringtoKB(getCUDDMaxMem()); JDD.InitialiseCUDD(cuddMaxMem, getCUDDEpsilon()); cuddStarted = true; - JDD.SetOutputStream(techLog.getFilePointer()); + JDD.SetOutputStream(mainLog.getFilePointer()); // initialise libraries/engines PrismNative.initialise(this); - PrismMTBDD.initialise(mainLog, techLog); - PrismSparse.initialise(mainLog, techLog); - PrismHybrid.initialise(mainLog, techLog); + PrismMTBDD.initialise(mainLog, mainLog); + PrismSparse.initialise(mainLog, mainLog); + PrismHybrid.initialise(mainLog, mainLog); // set cudd manager in other packages DoubleVector.setCUDDManager(); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 24330646..15592206 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -116,7 +116,6 @@ public class PrismCL implements PrismModelListener // files/filenames private String mainLogFilename = "stdout"; - private String techLogFilename = "stdout"; private String settingsFilename = null; private String modelFilename = null; private String importStatesFilename = null; @@ -143,7 +142,6 @@ public class PrismCL implements PrismModelListener // logs private PrismLog mainLog = null; - private PrismLog techLog = null; // prism object private Prism prism = null; @@ -504,14 +502,13 @@ public class PrismCL implements PrismModelListener { try { // prepare storage for parametric model checking - // default to logs going to stdout + // default to log going to stdout // this means all errors etc. can be safely sent to the log // even if a new log is created shortly mainLog = new PrismFileLog("stdout"); - techLog = new PrismFileLog("stdout"); // create prism object(s) - prism = new Prism(mainLog, techLog); + prism = new Prism(mainLog); prism.addModelListener(this); // parse command line arguments @@ -936,7 +933,6 @@ public class PrismCL implements PrismModelListener mainLog.println(); // Close logs (in case they are files) mainLog.close(); - techLog.close(); } /** Set a timeout, exit program if timeout is reached */ @@ -1659,20 +1655,6 @@ public class PrismCL implements PrismModelListener errorAndExit("No file specified for -" + sw + " switch"); } } - // specify mtbdd log (hidden option) - else if (sw.equals("techlog")) { - if (i < args.length - 1) { - techLogFilename = args[++i]; - log = new PrismFileLog(techLogFilename); - if (!log.ready()) { - errorAndExit("Couldn't open log file \"" + techLogFilename + "\""); - } - techLog = log; - prism.setTechLog(techLog); - } else { - errorAndExit("No file specified for -" + sw + " switch"); - } - } // mtbdd construction method (hidden option) else if (sw.equals("c1")) { prism.setConstruction(1); diff --git a/prism/src/prism/PrismTest.java b/prism/src/prism/PrismTest.java index c44ecc23..110635c2 100644 --- a/prism/src/prism/PrismTest.java +++ b/prism/src/prism/PrismTest.java @@ -55,7 +55,7 @@ public class PrismTest // Init mainLog = new PrismFileLog("stdout"); - prism = new Prism(mainLog, mainLog); + prism = new Prism(mainLog); prism.initialise(); // Parse/load model 1 diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java index c34ad242..3a115ebd 100644 --- a/prism/src/prism/StateModelChecker.java +++ b/prism/src/prism/StateModelChecker.java @@ -45,7 +45,6 @@ public class StateModelChecker extends PrismComponent implements ModelChecker { // PRISM stuff protected Prism prism; - protected PrismLog techLog; // Properties file protected PropertiesFile propertiesFile; @@ -94,7 +93,6 @@ public class StateModelChecker extends PrismComponent implements ModelChecker // Initialise this.prism = prism; - techLog = prism.getTechLog(); model = m; propertiesFile = pf; constantValues = new Values(); @@ -136,7 +134,6 @@ public class StateModelChecker extends PrismComponent implements ModelChecker // Initialise this.prism = prism; - techLog = prism.getTechLog(); this.varList = varList; this.varDDRowVars = varDDRowVars; this.constantValues = constantValues; diff --git a/prism/src/userinterface/GUIPrism.java b/prism/src/userinterface/GUIPrism.java index 1debf8a4..ba1a3ff4 100644 --- a/prism/src/userinterface/GUIPrism.java +++ b/prism/src/userinterface/GUIPrism.java @@ -250,7 +250,7 @@ public class GUIPrism extends JFrame private void setupPrism() throws PrismException { theLog = new userinterface.log.GUIWindowLog(); - prism = new Prism(theLog, new PrismFileLog("stdout")); + prism = new Prism(theLog); prism.loadUserSettingsFile(); prism.initialise(); }