Skip to content
Snippets Groups Projects
Commit 609310c5 authored by dgelessus's avatar dgelessus
Browse files

Remove last use of TLC4BGlobals.testingMode

The tests seem to work just fine without this special case.
parent bd573e7d
Branches
Tags
No related merge requests found
......@@ -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/");
......
......@@ -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;
}
......
......@@ -96,7 +96,7 @@ public class TLCResults implements ToolGlobals {
evalAllMessages();
if (hasTrace() || (TLC4BGlobals.getTestingMode() && OutputCollector.getInitialState() != null)) {
if (hasTrace()) {
evalTrace();
}
......
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 {
@BeforeClass
public static void setUp(){
TLC4BGlobals.setTestingMode(true);
}
import static de.tlc4b.util.TestUtil.compareLTLFormula;
import static de.tlc4b.util.TestUtil.compareModuleAndConfig;
public class LTLFormulaTest {
@Test (expected = ScopeException.class)
public void testScopeException() throws Exception {
String machine = "MACHINE test\n"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment