diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java index bed89c27fc53245c83920f3b69a704c0d2a65e78..b72fb81bb4888c0674209855716c7efd2f67c49e 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 b557542200c21dcfcece49d98a3bddf674972243..2ec908b5d6960ad821275f94ba24fc4695c72f92 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);