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

 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() {

src/main/java/de/tlc4b/tlc/TLCMessageListener.java

 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++) {

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