From 74ae5f1654d09dcda2c4001401094a65be51a09b Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 22:33:27 +0200
Subject: [PATCH] Remove TLC4BGlobals.checkOnlyMainAssertions which was always
false
Apparently this has never been used since it was added in 2015 (see
58c457300d9b6e4a7eba131c4cba4d0cd662a7e5 and
22c9bd79d503f75db8aa88585954ec8c885af8f4), so it was probably left in
accidentally.
---
src/main/java/de/tlc4b/TLC4BGlobals.java | 8 --------
.../de/tlc4b/analysis/transformation/SeesEliminator.java | 3 ---
2 files changed, 11 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index bed89c2..b72fb81 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -18,8 +18,6 @@ public class TLC4BGlobals {
private static boolean verbose;
private static boolean silent;
- private static boolean checkOnlyMainAssertions;
-
private static boolean deleteFilesOnExit;
private static boolean runTLC;
@@ -53,7 +51,6 @@ public class TLC4BGlobals {
useSymmetry = false;
printCoverage = false;
forceTLCToEvalConstants = false;
- checkOnlyMainAssertions = false;
verbose = false;
silent = false;
@@ -263,9 +260,4 @@ public class TLC4BGlobals {
public static boolean isSilent() {
return silent;
}
-
- public static boolean isCheckOnlyMainAssertions() {
- return checkOnlyMainAssertions;
- }
-
}
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
index b557542..2ec908b 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
@@ -24,7 +24,6 @@ import de.be4.classicalb.core.parser.node.PParseUnit;
import de.be4.classicalb.core.parser.node.PPredicate;
import de.be4.classicalb.core.parser.node.Start;
import de.be4.classicalb.core.parser.util.Utils;
-import de.tlc4b.TLC4BGlobals;
public class SeesEliminator extends DepthFirstAdapter {
@@ -182,8 +181,6 @@ public class SeesEliminator extends DepthFirstAdapter {
}
public void caseAAssertionsMachineClause(AAssertionsMachineClause node) {
- if (TLC4BGlobals.isCheckOnlyMainAssertions())
- return;
AAssertionsMachineClause main = (AAssertionsMachineClause) machineClauseHashMap.get(node.getClass());
if (main == null) {
additionalMachineClauseList.add(node);
--
GitLab