Browse Source

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
master
Dave Parker 11 years ago
parent
commit
b6828a7045
  1. 4
      prism/etc/scripts/prism-auto
  2. 2
      prism/src/explicit/ConstructModel.java
  3. 4
      prism/src/explicit/PrismExplicit.java
  4. 2
      prism/src/explicit/QuantAbstractRefineExample.java
  5. 2
      prism/src/prism/ExplicitModel2MTBDD.java
  6. 2
      prism/src/prism/Modules2MTBDD.java
  7. 4
      prism/src/prism/Preprocessor.java
  8. 57
      prism/src/prism/Prism.java
  9. 22
      prism/src/prism/PrismCL.java
  10. 2
      prism/src/prism/PrismTest.java
  11. 3
      prism/src/prism/StateModelChecker.java
  12. 2
      prism/src/userinterface/GUIPrism.java

4
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()

2
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)

4
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]));

2
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("");

2
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

2
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);

4
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);

57
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<PrismModelListener>();
}
/**
* 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();

22
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);

2
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

3
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;

2
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();
}

Loading…
Cancel
Save