Browse Source

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
master
Dave Parker 19 years ago
parent
commit
bbc42fe37a
  1. 4
      prism/src/prism/PrismCL.java
  2. 1
      prism/src/userinterface/model/computation/BuildModelThread.java
  3. 3
      prism/src/userinterface/properties/GUIExperiment.java
  4. 1
      prism/src/userinterface/properties/computation/ModelCheckThread.java
  5. 2
      prism/src/userinterface/properties/computation/SimulateModelCheckThread.java

4
prism/src/prism/PrismCL.java

@ -285,6 +285,7 @@ public class PrismCL
// for simulation we can do multiple values of property constants simultaneously // for simulation we can do multiple values of property constants simultaneously
if (simulate && undefinedConstants.getNumPropertyIterations() > 1) { if (simulate && undefinedConstants.getNumPropertyIterations() > 1) {
try { try {
mainLog.println("\n-------------------------------------------");
mainLog.println("\nSimulating: " + propertiesToCheck[j]); mainLog.println("\nSimulating: " + propertiesToCheck[j]);
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("Model constants: " + definedMFConstants); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("Model constants: " + definedMFConstants);
mainLog.println("Property constants: " + undefinedConstants.getPFDefinedConstantsString()); mainLog.println("Property constants: " + undefinedConstants.getPFDefinedConstantsString());
@ -319,6 +320,7 @@ public class PrismCL
} }
// do model checking // do model checking
mainLog.println("\n-------------------------------------------");
mainLog.println("\n"+(simulate?"Simulating":"Model checking")+": " + propertiesToCheck[j]); mainLog.println("\n"+(simulate?"Simulating":"Model checking")+": " + propertiesToCheck[j]);
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("Model constants: " + definedMFConstants); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) mainLog.println("Model constants: " + definedMFConstants);
if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) mainLog.println("Property constants: " + definedPFConstants); if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) mainLog.println("Property constants: " + definedPFConstants);
@ -525,6 +527,8 @@ public class PrismCL
StateList states; StateList states;
int i; int i;
mainLog.println("\n-------------------------------------------");
// build model // build model
if (importtrans) { if (importtrans) {
model = prism.buildExplicitModel(); model = prism.buildExplicitModel();

1
prism/src/userinterface/model/computation/BuildModelThread.java

@ -198,6 +198,7 @@ public class BuildModelThread extends GUIComputationThread
// do build // do build
try { try {
logln("\n-------------------------------------------");
model = prism.buildModel(mod); model = prism.buildModel(mod);
} }
catch (PrismException e) { catch (PrismException e) {

3
prism/src/userinterface/properties/GUIExperiment.java

@ -274,6 +274,7 @@ public class GUIExperiment
{ {
// build model // build model
try { try {
logln("\n-------------------------------------------");
model = prism.buildModel(modulesFile); model = prism.buildModel(modulesFile);
clear = false; clear = false;
} }
@ -367,6 +368,7 @@ public class GUIExperiment
else if(useSimulation && prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS) && undefinedConstants.getNumPropertyIterations() > 1) else if(useSimulation && prism.getSettings().getBoolean(PrismSettings.SIMULATOR_SIMULTANEOUS) && undefinedConstants.getNumPropertyIterations() > 1)
{ {
try { try {
logln("\n-------------------------------------------");
logln("\nSimulating: " + propertyToCheck); logln("\nSimulating: " + propertyToCheck);
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants);
logln("Property constants: " + undefinedConstants.getPFDefinedConstantsString()); logln("Property constants: " + undefinedConstants.getPFDefinedConstantsString());
@ -407,6 +409,7 @@ public class GUIExperiment
} }
// do model checking // do model checking
logln("\n-------------------------------------------");
logln("\n"+(useSimulation?"Simulating":"Model checking")+": " + propertyToCheck); logln("\n"+(useSimulation?"Simulating":"Model checking")+": " + propertyToCheck);
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants);
if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants); if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants);

1
prism/src/userinterface/properties/computation/ModelCheckThread.java

@ -97,6 +97,7 @@ public class ModelCheckThread extends GUIComputationThread
// do model checking // do model checking
try try
{ {
logln("\n-------------------------------------------");
logln("\nModel checking: " + prFi.getProperty(i)); logln("\nModel checking: " + prFi.getProperty(i));
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants);
if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants); if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants);

2
prism/src/userinterface/properties/computation/SimulateModelCheckThread.java

@ -127,6 +127,7 @@ public class SimulateModelCheckThread extends GUIComputationThread
try try
{ {
// display info // display info
logln("\n-------------------------------------------");
log("\nSimulating"); log("\nSimulating");
if (pf.getNumProperties() == 1) { if (pf.getNumProperties() == 1) {
logln(": " + properties.get(0)); logln(": " + properties.get(0));
@ -180,6 +181,7 @@ public class SimulateModelCheckThread extends GUIComputationThread
// do model checking // do model checking
try try
{ {
logln("\n-------------------------------------------");
logln("\nSimulating"+": " + pf.getProperty(i)); logln("\nSimulating"+": " + pf.getProperty(i));
if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants); if (definedMFConstants != null) if (definedMFConstants.getNumValues() > 0) logln("Model constants: " + definedMFConstants);
if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants); if (definedPFConstants != null) if (definedPFConstants.getNumValues() > 0) logln("Property constants: " + definedPFConstants);

Loading…
Cancel
Save