From 609310c5d82621bc7a5b33d152faa1bf7a17f764 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 22:27:20 +0200
Subject: [PATCH] Remove last use of TLC4BGlobals.testingMode

The tests seem to work just fine without this special case.
---
 src/main/java/de/tlc4b/TLC4B.java             |  2 --
 src/main/java/de/tlc4b/TLC4BGlobals.java      | 11 ----------
 src/main/java/de/tlc4b/tlc/TLCResults.java    |  2 +-
 .../java/de/tlc4b/ltl/LTLFormulaTest.java     | 20 +++++--------------
 4 files changed, 6 insertions(+), 29 deletions(-)

diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 3646563..f75a1f2 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -194,7 +194,6 @@ public class TLC4B {
 		System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
 		TLC4BGlobals.resetGlobals();
 		TLC4BGlobals.setDeleteOnExit(deleteFiles);
-		TLC4BGlobals.setTestingMode(true);
 		// B2TLAGlobals.setCleanup(true);
 		TLC4B tlc4b = new TLC4B();
 		try {
@@ -221,7 +220,6 @@ public class TLC4B {
 		System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up windows
 		TLC4BGlobals.resetGlobals();
 		TLC4BGlobals.setDeleteOnExit(deleteFiles);
-		TLC4BGlobals.setTestingMode(true);
 		// B2TLAGlobals.setCleanup(true);
 		TLC4B tlc4b = new TLC4B();
 		tlc4b.buildDir = new File("temp/");
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 8a510ca..eea24e9 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -27,8 +27,6 @@ public class TLC4BGlobals {
 	private static boolean hideTLCConsoleOutput;
 	private static boolean createTraceFile;
 
-	private static boolean testingMode;
-
 	private static boolean cleanup;
 
 	private static boolean forceTLCToEvalConstants;
@@ -75,7 +73,6 @@ 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.).
 		runTestscript = false;
-		testingMode = false;
 		createTraceFile = true;
 	}
 
@@ -231,14 +228,6 @@ public class TLC4BGlobals {
 		TLC4BGlobals.proBconstantsSetup = proBconstantsSetup;
 	}
 
-	public static void setTestingMode(boolean b) {
-		TLC4BGlobals.testingMode = b;
-	}
-
-	public static boolean getTestingMode() {
-		return TLC4BGlobals.testingMode;
-	}
-
 	public static void setWelldefinednessCheck(boolean b) {
 		TLC4BGlobals.checkWD = b;
 	}
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index 3578220..8864a40 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -96,7 +96,7 @@ public class TLCResults implements ToolGlobals {
 
 		evalAllMessages();
 
-		if (hasTrace() || (TLC4BGlobals.getTestingMode() && OutputCollector.getInitialState() != null)) {
+		if (hasTrace()) {
 			evalTrace();
 		}
 
diff --git a/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java b/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java
index ba07509..70a4f5e 100644
--- a/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java
+++ b/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java
@@ -1,26 +1,16 @@
 package de.tlc4b.ltl;
 
-
-import static de.tlc4b.util.TestUtil.compareModuleAndConfig;
-import static de.tlc4b.util.TestUtil.compareLTLFormula;
-
-import org.junit.BeforeClass;
-import org.junit.Ignore;
-import org.junit.Test;
-
-import de.tlc4b.TLC4BGlobals;
 import de.tlc4b.exceptions.LTLParseException;
 import de.tlc4b.exceptions.ScopeException;
 import de.tlc4b.exceptions.TypeErrorException;
 
+import org.junit.Ignore;
+import org.junit.Test;
 
-public class LTLFormulaTest {
+import static de.tlc4b.util.TestUtil.compareLTLFormula;
+import static de.tlc4b.util.TestUtil.compareModuleAndConfig;
 
-	@BeforeClass
-	public static void setUp(){
-		TLC4BGlobals.setTestingMode(true);
-	}
-	
+public class LTLFormulaTest {
 	@Test (expected = ScopeException.class)
 	public void testScopeException() throws Exception {
 		String machine = "MACHINE test\n"
-- 
GitLab