From 311031fb8b8a9d9c32be7e08f26b566278941438 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Mon, 27 Jan 2025 06:53:25 +0100
Subject: [PATCH] reset OutputCollector together with TLC4BGlobals
avoid incorrect model check results extracted from old messages, important for ProB2(-UI)
---
src/main/java/de/tlc4b/TLC4BGlobals.java | 45 +++++++++++++++++++
.../java/de/tlc4b/tlc/TLCMessageListener.java | 4 +-
src/main/java/de/tlc4b/tlc/TLCResults.java | 8 ++--
3 files changed, 51 insertions(+), 6 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 2ae19fc..8653fc4 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -1,5 +1,15 @@
package de.tlc4b;
+import tla2sany.semantic.ExprNode;
+import tla2sany.st.Location;
+import tlc2.output.Message;
+import tlc2.output.OutputCollector;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
public class TLC4BGlobals {
private static int DEFERRED_SET_SIZE;
private static int MAX_INT;
@@ -29,6 +39,10 @@ public class TLC4BGlobals {
private static int workers;
private static int dfid_initial_depth;
+ private static final List<Message> handledMessages = new ArrayList<>();
+ private static final Map<Location, Long> handledLineCounts = new HashMap<>();
+ private static final List<ExprNode> handledViolatedAssumptions = new ArrayList<>();
+
static {
resetGlobals();
}
@@ -62,6 +76,37 @@ public class TLC4BGlobals {
deleteFilesOnExit = false; // if enabled: deletes all created '.tla', '.cfg' files on exit of the JVM.
// This includes the created B2TLA standard modules (e.g. Relation, but not Naturals etc.).
createTraceFile = true;
+
+ resetOutputCollector();
+ // TODO: do we also have to reset TLCGlobals?
+ }
+
+ private static void resetOutputCollector() {
+ // otherwise we will analyse old messages from previous checks -> wrong results in the same JVM (important for ProB2(-UI))
+ OutputCollector.setModuleNode(null);
+ OutputCollector.setInitialState(null);
+ OutputCollector.setTrace(new ArrayList<>());
+ handledMessages.addAll(OutputCollector.getAllMessages());
+ handledLineCounts.putAll(OutputCollector.getLineCountTable());
+ handledViolatedAssumptions.addAll(OutputCollector.getViolatedAssumptions());
+ }
+
+ public static List<Message> getCurrentMessages() {
+ List<Message> messages = new ArrayList<>(OutputCollector.getAllMessages()); // all messages including old
+ messages.removeAll(handledMessages); // remove already handled messages from old checks
+ return messages;
+ }
+
+ public static Map<Location, Long> getCurrentLineCounts() {
+ Map<Location, Long> lineCounts = new HashMap<>(OutputCollector.getLineCountTable());
+ handledLineCounts.forEach(lineCounts::remove);
+ return lineCounts;
+ }
+
+ public static List<ExprNode> getCurrentViolatedAssumptions() {
+ List<ExprNode> violatedAssumptions = new ArrayList<>(OutputCollector.getViolatedAssumptions());
+ violatedAssumptions.removeAll(handledViolatedAssumptions);
+ return violatedAssumptions;
}
public static boolean isCreateTraceFile() {
diff --git a/src/main/java/de/tlc4b/tlc/TLCMessageListener.java b/src/main/java/de/tlc4b/tlc/TLCMessageListener.java
index d1f276a..5692318 100644
--- a/src/main/java/de/tlc4b/tlc/TLCMessageListener.java
+++ b/src/main/java/de/tlc4b/tlc/TLCMessageListener.java
@@ -1,7 +1,7 @@
package de.tlc4b.tlc;
+import de.tlc4b.TLC4BGlobals;
import tlc2.output.Message;
-import tlc2.output.OutputCollector;
import java.util.*;
@@ -13,7 +13,7 @@ public abstract class TLCMessageListener extends Thread {
@Override
public void run() {
while (tlcRunning) {
- List<Message> currentMessages = OutputCollector.getAllMessages();
+ List<Message> currentMessages = TLC4BGlobals.getCurrentMessages();
int currentMessageIndex = currentMessages.size();
if (lastMessageIndex < currentMessageIndex) {
for (int i = lastMessageIndex; i < currentMessageIndex; i++) {
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index 8864a40..db983c9 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -105,14 +105,14 @@ public class TLCResults implements ToolGlobals {
tlcResult = InitialStateError;
}
- if (TLC4BGlobals.isPrintCoverage() && !OutputCollector.getLineCountTable().isEmpty()) {
+ if (TLC4BGlobals.isPrintCoverage() && !TLC4BGlobals.getCurrentLineCounts().isEmpty()) {
evalCoverage();
}
}
private void evalCoverage() {
Hashtable<Integer, Long> lineCount = new Hashtable<>();
- Set<Entry<Location, Long>> entrySet = OutputCollector.getLineCountTable().entrySet();
+ Set<Entry<Location, Long>> entrySet = TLC4BGlobals.getCurrentLineCounts().entrySet();
for (Entry<Location, Long> entry : entrySet) {
int endline = entry.getKey().endLine();
if (lineCount.containsKey(endline)) {
@@ -193,7 +193,7 @@ public class TLCResults implements ToolGlobals {
private void evalAllMessages() {
- List<Message> messages = new ArrayList<>(OutputCollector.getAllMessages());
+ List<Message> messages = new ArrayList<>(TLC4BGlobals.getCurrentMessages());
for (Message m : messages) {
switch (m.getMessageClass()) {
case ERROR:
@@ -282,7 +282,7 @@ public class TLCResults implements ToolGlobals {
case EC.TLC_ASSUMPTION_FALSE:
// get the violated assumption expr from the OutputCollector
- List<ExprNode> violatedAssumptions = OutputCollector.getViolatedAssumptions();
+ List<ExprNode> violatedAssumptions = TLC4BGlobals.getCurrentViolatedAssumptions();
if (!violatedAssumptions.isEmpty()) {
// try to find the assume node contain the expr in order to get
// the name of the assumption
--
GitLab