From bbc42fe37a3d19330de915ac12b8b1c78f38fb5f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 31 May 2007 11:47:56 +0000 Subject: [PATCH] Clearer log output: separator lines between each build/verification. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@382 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/PrismCL.java | 4 ++++ .../src/userinterface/model/computation/BuildModelThread.java | 1 + prism/src/userinterface/properties/GUIExperiment.java | 3 +++ .../properties/computation/ModelCheckThread.java | 1 + .../properties/computation/SimulateModelCheckThread.java | 2 ++ 5 files changed, 11 insertions(+) diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index e8d0ee64..61127268 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -285,6 +285,7 @@ public class PrismCL // for simulation we can do multiple values of property constants simultaneously if (simulate && undefinedConstants.getNumPropertyIterations() > 1) { try { + mainLog.println("\n-------------------------------------------"); mainLog.println("\nSimulating: " + propertiesToCheck[j]); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("Model constants: " + definedMFConstants); mainLog.println("Property constants: " + undefinedConstants.getPFDefinedConstantsString()); @@ -319,6 +320,7 @@ public class PrismCL } // do model checking + mainLog.println("\n-------------------------------------------"); mainLog.println("\n"+(simulate?"Simulating":"Model checking")+": " + propertiesToCheck[j]); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("Model constants: " + definedMFConstants); if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) mainLog.println("Property constants: " + definedPFConstants); @@ -525,6 +527,8 @@ public class PrismCL StateList states; int i; + mainLog.println("\n-------------------------------------------"); + // build model if (importtrans) { model = prism.buildExplicitModel(); diff --git a/prism/src/userinterface/model/computation/BuildModelThread.java b/prism/src/userinterface/model/computation/BuildModelThread.java index 3cf20fdd..5c185ca6 100644 --- a/prism/src/userinterface/model/computation/BuildModelThread.java +++ b/prism/src/userinterface/model/computation/BuildModelThread.java @@ -198,6 +198,7 @@ public class BuildModelThread extends GUIComputationThread // do build try { + logln("\n-------------------------------------------"); model = prism.buildModel(mod); } catch (PrismException e) { diff --git a/prism/src/userinterface/properties/GUIExperiment.java b/prism/src/userinterface/properties/GUIExperiment.java index 7e479de0..d49889de 100644 --- a/prism/src/userinterface/properties/GUIExperiment.java +++ b/prism/src/userinterface/properties/GUIExperiment.java @@ -274,6 +274,7 @@ public class GUIExperiment { // build model try { + logln("\n-------------------------------------------"); model = prism.buildModel(modulesFile); clear = false; } @@ -367,6 +368,7 @@ public class GUIExperiment else if(useSimulation && prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS) && undefinedConstants.getNumPropertyIterations() > 1) { try { + logln("\n-------------------------------------------"); logln("\nSimulating: " + propertyToCheck); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); logln("Property constants: " + undefinedConstants.getPFDefinedConstantsString()); @@ -407,6 +409,7 @@ public class GUIExperiment } // do model checking + logln("\n-------------------------------------------"); logln("\n"+(useSimulation?"Simulating":"Model checking")+": " + propertyToCheck); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants); diff --git a/prism/src/userinterface/properties/computation/ModelCheckThread.java b/prism/src/userinterface/properties/computation/ModelCheckThread.java index 69a52643..47584e89 100644 --- a/prism/src/userinterface/properties/computation/ModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/ModelCheckThread.java @@ -97,6 +97,7 @@ public class ModelCheckThread extends GUIComputationThread // do model checking try { + logln("\n-------------------------------------------"); logln("\nModel checking: " + prFi.getProperty(i)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants); diff --git a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java index 3dc7be09..76d82180 100644 --- a/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java +++ b/prism/src/userinterface/properties/computation/SimulateModelCheckThread.java @@ -127,6 +127,7 @@ public class SimulateModelCheckThread extends GUIComputationThread try { // display info + logln("\n-------------------------------------------"); log("\nSimulating"); if (pf.getNumProperties() == 1) { logln(": " + properties.get(0)); @@ -180,6 +181,7 @@ public class SimulateModelCheckThread extends GUIComputationThread // do model checking try { + logln("\n-------------------------------------------"); logln("\nSimulating"+": " + pf.getProperty(i)); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants);