[PEx] Minor correction

Update liveness check, minor renaming
p-org · Aug 6, 2024 · ad40c1c · ad40c1c
1 parent 261d289
commit ad40c1c
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 10 deletions.
diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/RuntimeExecutor.java
@@ -88,7 +88,7 @@ private static void preprocess() {
         PExplicitGlobal.setResult("error");
 
         StatWriter.log("project-name", String.format("%s", PExplicitGlobal.getConfig().getProjectName()));
-        StatWriter.log("strategy", String.format("%s", PExplicitGlobal.getConfig().getSearchStrategyMode()));
+        StatWriter.log("mode", String.format("%s", PExplicitGlobal.getConfig().getSearchStrategyMode()));
         StatWriter.log("time-limit-seconds", String.format("%.1f", PExplicitGlobal.getConfig().getTimeLimit()));
         StatWriter.log("memory-limit-MB", String.format("%.1f", PExplicitGlobal.getConfig().getMemLimit()));
     }

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/STATUS.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/STATUS.java
@@ -5,8 +5,8 @@ public enum STATUS {
     SCHEDULEOUT("scheduleout"),                         // schedule limit reached
     TIMEOUT("timeout"),                                 // timeout reached
     MEMOUT("memout"),                                   // memout reached
-    VERIFIED("proved"),                                 // full state space explored and no bug found
-    VERIFIED_UPTO_MAX_STEPS("proved"),   // full state space explored and no bug found upto max steps
+    VERIFIED("verified"),                               // full state space explored and no bug found
+    VERIFIED_UPTO_MAX_STEPS("verified"),                // full state space explored and no bug found upto max steps
     BUG_FOUND("cex"),                                   // found a bug
     INTERRUPTED("interrupted"),                         // interrupted by user
     ERROR("error");                                     // unexpected error encountered

diff --git a/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java b/Src/PRuntimes/PExplicitRuntime/src/main/java/pexplicit/runtime/scheduler/Scheduler.java
@@ -357,12 +357,10 @@ public void checkDeadlock() {
      * Check for liveness at the end of a completed schedule
      */
     public void checkLiveness(boolean terminated) {
-        for (PMachine monitor : PExplicitGlobal.getModel().getMonitors()) {
-            if (monitor.getCurrentState().isHotState()) {
-                if (terminated) {
-                    Assert.liveness(String.format("Monitor %s detected liveness bug in hot state %s at the end of program execution", monitor, monitor.getCurrentState()));
-                } else {
-                    Assert.liveness(String.format("Monitor %s detected potential liveness bug in hot state %s", monitor, monitor.getCurrentState()));
+        if (terminated) {
+            for (PMachine monitor : PExplicitGlobal.getModel().getMonitors()) {
+                if (monitor.getCurrentState().isHotState()) {
+                        Assert.liveness(String.format("Monitor %s detected liveness bug in hot state %s at the end of program execution", monitor, monitor.getCurrentState()));
                 }
             }
         }

diff --git a/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java b/...itRuntime/src/main/java/pexplicit/runtime/scheduler/explicit/ExplicitSearchScheduler.java
@@ -599,7 +599,7 @@ public void recordStats() {
         printProgress(true);
 
         // print basic statistics
-        StatWriter.log("#-executions", String.format("%d", SearchStatistics.iteration));
+        StatWriter.log("#-schedules", String.format("%d", SearchStatistics.iteration));
         if (PExplicitGlobal.getConfig().getStateCachingMode() != StateCachingMode.None) {
             StatWriter.log("#-states", String.format("%d", SearchStatistics.totalStates));
             StatWriter.log("#-distinct-states", String.format("%d", SearchStatistics.totalDistinctStates));