diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java index 2ae19fc3df4eb8d544b9b0d3d933704fc621f4b5..8653fc4f2a4089a17fece4b65c6210d6fbf7a66d 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 d1f276a0f16cc859aa72fd3713946d39de098f50..5692318643a55d9ca80d2cccc9a8534187eddc9f 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 8864a40ba9afeac78499c022c460ddfb27445208..db983c9e797aa425c0f7a84789d49b2e2dfed080 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