From 6eb375c441377a793830034441360dc944401dba Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 20 Nov 2011 23:36:44 +0000 Subject: [PATCH] Added printSeparator method to PrismLog. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4183 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 8 ++++---- prism/src/prism/PrismLog.java | 8 ++++++++ prism/src/userinterface/GUIComputationThread.java | 1 + prism/src/userinterface/GUIPlugin.java | 7 +++++++ prism/src/userinterface/log/GUILog.java | 10 +++++++--- .../model/computation/BuildModelThread.java | 2 +- prism/src/userinterface/properties/GUIExperiment.java | 8 ++++---- .../properties/computation/ModelCheckThread.java | 4 ++-- .../computation/SimulateModelCheckThread.java | 4 ++-- prism/src/userinterface/util/GUILogEvent.java | 3 ++- 10 files changed, 38 insertions(+), 17 deletions(-) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index d5b99b23..9f041bec 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -357,7 +357,7 @@ public class PrismCL // for simulation we can do multiple values of property constants simultaneously if (simulate && undefinedConstants[j].getNumPropertyIterations() > 1) { try { - mainLog.println("\n-------------------------------------------"); + mainLog.printSeparator(); mainLog.println("\nSimulating: " + propertiesToCheck.get(j)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) @@ -391,7 +391,7 @@ public class PrismCL } // log output - mainLog.println("\n-------------------------------------------"); + mainLog.printSeparator(); mainLog.println("\n" + (simulate ? "Simulating" : "Model checking") + ": " + propertiesToCheck.get(j)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) @@ -705,7 +705,7 @@ public class PrismCL StateList states; int i; - mainLog.println("\n-------------------------------------------"); + mainLog.printSeparator(); // build model if (!explicit) { @@ -1055,7 +1055,7 @@ public class PrismCL // notify about any warnings int numWarnings = mainLog.getNumberOfWarnings(); if (numWarnings > 0) { - mainLog.println("\n-------------------------------------------"); + mainLog.printSeparator(); mainLog.print("\nNote: There "); if (numWarnings == 1) mainLog.print("was 1 warning"); diff --git a/prism/src/prism/PrismLog.java b/prism/src/prism/PrismLog.java index 80d3cf87..aa889441 100644 --- a/prism/src/prism/PrismLog.java +++ b/prism/src/prism/PrismLog.java @@ -362,6 +362,14 @@ public abstract class PrismLog println(arr); } + /** + * Prints a separator between sections of log output. + */ + public void printSeparator() + { + println("\n---------------------------------------------------------------------"); + } + /** * Prints a warning message {@code s}, preceded by "\nWarning: " and followed by a newline character. *

diff --git a/prism/src/userinterface/GUIComputationThread.java b/prism/src/userinterface/GUIComputationThread.java index 4dbde8a8..0c308423 100644 --- a/prism/src/userinterface/GUIComputationThread.java +++ b/prism/src/userinterface/GUIComputationThread.java @@ -72,6 +72,7 @@ public class GUIComputationThread extends Thread public void logln(short s) { plug.logln(s); } public void logln(byte b) { plug.logln(b); } public void logln(boolean b) { plug.logln(b); } + public void logSeparator() { plug.logSeparator(); } public void logWarning(String s) { plug.logWarning(s); } /** pop up an error dialog */ diff --git a/prism/src/userinterface/GUIPlugin.java b/prism/src/userinterface/GUIPlugin.java index f5f6cc17..656e0496 100644 --- a/prism/src/userinterface/GUIPlugin.java +++ b/prism/src/userinterface/GUIPlugin.java @@ -543,6 +543,13 @@ public abstract class GUIPlugin extends JPanel implements GUIEventListener, Pris gui.enableTab(this, enabled); } + /** Method to add a separator to the log contained within the parent GUIPrism. + */ + public void logSeparator() + { + notifyEventListeners(new GUILogEvent(GUILogEvent.PRINTSEPARATOR, "")); + } + /** Method to add a warning message to the log contained within the parent GUIPrism. * @param message The message to be added to the log */ diff --git a/prism/src/userinterface/log/GUILog.java b/prism/src/userinterface/log/GUILog.java index d582bc47..5c0c1eef 100644 --- a/prism/src/userinterface/log/GUILog.java +++ b/prism/src/userinterface/log/GUILog.java @@ -114,15 +114,19 @@ public class GUILog extends GUIPlugin implements MouseListener, PrismSettingsLis if(e instanceof GUILogEvent) { GUILogEvent le = (GUILogEvent)e; - if(le.getID() == le.PRINTLN) + if(le.getID() == GUILogEvent.PRINTLN) { theLog.println(le.getData()); } - else if(le.getID() == le.PRINT) + else if(le.getID() == GUILogEvent.PRINT) { theLog.print(le.getData()); } - else if(le.getID() == le.PRINTWARNING) + else if(le.getID() == GUILogEvent.PRINTSEPARATOR) + { + theLog.printSeparator(); + } + else if(le.getID() == GUILogEvent.PRINTWARNING) { theLog.printWarning((String) le.getData()); } diff --git a/prism/src/userinterface/model/computation/BuildModelThread.java b/prism/src/userinterface/model/computation/BuildModelThread.java index e1a5e42a..f95e7e25 100644 --- a/prism/src/userinterface/model/computation/BuildModelThread.java +++ b/prism/src/userinterface/model/computation/BuildModelThread.java @@ -190,7 +190,7 @@ public class BuildModelThread extends GUIComputationThread // do build try { - logln("\n-------------------------------------------"); + logSeparator(); model = prism.buildModel(mod); } catch (PrismException e) { diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index 7ae14c39..381beef4 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -264,7 +264,7 @@ public class GUIExperiment // build model try { - logln("\n-------------------------------------------"); + logSeparator(); model = prism.buildModel(modulesFile); clear = false; } catch (PrismException e) { @@ -352,7 +352,7 @@ public class GUIExperiment else if (useSimulation && prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS) && undefinedConstants.getNumPropertyIterations() > 1) { try { - logln("\n-------------------------------------------"); + logSeparator(); logln("\nSimulating: " + propertyToCheck); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) @@ -398,7 +398,7 @@ public class GUIExperiment } // log output - logln("\n-------------------------------------------"); + logSeparator(); logln("\n" + (useSimulation ? "Simulating" : "Model checking") + ": " + propertyToCheck); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) @@ -415,7 +415,7 @@ public class GUIExperiment modulesFileToCheck = dc.getNewModulesFile(); modulesFileToCheck.setUndefinedConstants(modulesFile.getConstantValues()); // build model - logln("\n-------------------------------------------"); + logSeparator(); model = prism.buildModel(modulesFileToCheck); clear = false; // by construction, deadlocks can only occur from timelocks diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index 3a8e6f2d..eb3abb8a 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/ModelCheckThread.java @@ -129,7 +129,7 @@ public class ModelCheckThread extends GUIComputationThread // Do model checking try { // Print info to log - logln("\n-------------------------------------------"); + logSeparator(); logln("\nModel checking: " + propertiesFile.getProperty(i)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) @@ -145,7 +145,7 @@ public class ModelCheckThread extends GUIComputationThread modulesFileToCheck = dc.getNewModulesFile(); modulesFileToCheck.setUndefinedConstants(modulesFile.getConstantValues()); // build model - logln("\n-------------------------------------------"); + logSeparator(); model = prism.buildModel(modulesFileToCheck); clear = false; // by construction, deadlocks can only occur from timelocks diff --git a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java index 298aaba1..2a746966 100644 --- a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java @@ -114,7 +114,7 @@ public class SimulateModelCheckThread extends GUIComputationThread try { // display info - logln("\n-------------------------------------------"); + logSeparator(); log("\nSimulating"); if (pf.getNumProperties() == 1) { logln(": " + properties.get(0)); @@ -179,7 +179,7 @@ public class SimulateModelCheckThread extends GUIComputationThread ict.start(); // do model checking try { - logln("\n-------------------------------------------"); + logSeparator(); logln("\nSimulating" + ": " + pf.getProperty(i)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) diff --git a/prism/src/userinterface/util/GUILogEvent.java b/prism/src/userinterface/util/GUILogEvent.java index 2b33578e..622243cd 100644 --- a/prism/src/userinterface/util/GUILogEvent.java +++ b/prism/src/userinterface/util/GUILogEvent.java @@ -31,7 +31,8 @@ public class GUILogEvent extends GUIEvent { public static final int PRINTLN = 0; public static final int PRINT = 1; - public static final int PRINTWARNING = 2; + public static final int PRINTSEPARATOR = 2; + public static final int PRINTWARNING = 3; /** * Constructs an instance of GUILogEvent with the specified detail message.