diff --git a/.gitignore b/.gitignore
index 1bb8669b490ece744c69e3abda15c41c7c1f00d9..aea28287072eb61d21d66786fceeb2905dad621b 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,6 +7,7 @@ build.xml
 TODO.txt
 .gradle
 .settings
+.idea
 build
 src/test/java/testing
 src/test/resources/other
diff --git a/build.gradle b/build.gradle
index 28e56efbcb2d751e386f7cd634ab6203db1fd295..f99e7c7c53e1ccef2aa95a2ee811240db7baee2c 100644
--- a/build.gradle
+++ b/build.gradle
@@ -8,7 +8,7 @@ plugins {
 }
 
 project.group = 'de.hhu.stups'
-project.version = "1.2.0"
+project.version = "1.2.1"
 
 final isSnapshot = project.version.endsWith("-SNAPSHOT")
 
@@ -16,8 +16,8 @@ repositories {
 	mavenCentral()
 	if (isSnapshot) {
 		maven {
-			name "sonatype snapshots"
-			url "https://oss.sonatype.org/content/repositories/snapshots"
+			name = "sonatype snapshots"
+			url = "https://oss.sonatype.org/content/repositories/snapshots"
 		}
 	}
 }
@@ -26,23 +26,22 @@ configurations.all {
 	resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
 }
 
-def parser_version = '2.13.5'
+def parser_version = '2.15.0'
 
 dependencies {
 	//implementation(group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
-	implementation(group: 'commons-cli', name: 'commons-cli', version: '1.8.0')
+	implementation(group: 'commons-cli', name: 'commons-cli', version: '1.9.0')
 	implementation(group: 'de.hhu.stups', name: 'tlatools', version: '1.1.0')
 
 	implementation(group: 'de.hhu.stups', name: 'bparser', version: parser_version)
 	implementation(group: 'de.hhu.stups', name: 'ltlparser', version: parser_version)
 
 	testImplementation(group: 'junit', name: 'junit', version: '4.13.2')
-	testImplementation(group: 'de.hhu.stups', name: 'tla2bAST', version: '1.4.0')
+	testImplementation(group: 'de.hhu.stups', name: 'tla2bAST', version: '1.4.1')
 }
 
 java {
 	sourceCompatibility = JavaVersion.VERSION_1_8
-	targetCompatibility = JavaVersion.VERSION_1_8
 	
 	withSourcesJar()
 	withJavadocJar()
@@ -144,11 +143,11 @@ publishing {
 		maven {
 			final releasesRepoUrl = "https://oss.sonatype.org/service/local/staging/deploy/maven2"
 			final snapshotsRepoUrl = "https://oss.sonatype.org/content/repositories/snapshots"
-			url isSnapshot ? snapshotsRepoUrl : releasesRepoUrl
+			url = isSnapshot ? snapshotsRepoUrl : releasesRepoUrl
 			if (project.hasProperty("ossrhUsername") && project.hasProperty("ossrhPassword")) {
 				credentials {
-					username project.ossrhUsername
-					password project.ossrhPassword
+					username = project.ossrhUsername
+					password = project.ossrhPassword
 				}
 			}
 		}
diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar
index a4b76b9530d66f5e68d973ea569d8e19de379189..9bbc975c742b298b441bfb90dbc124400a3751b9 100644
Binary files a/gradle/wrapper/gradle-wrapper.jar and b/gradle/wrapper/gradle-wrapper.jar differ
diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
index df97d72b8b91fa0e088ae27b1c84a6063481fe22..37f853b1c84d2e2dd1c88441fcc755d7f6643668 100644
--- a/gradle/wrapper/gradle-wrapper.properties
+++ b/gradle/wrapper/gradle-wrapper.properties
@@ -1,6 +1,6 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.10.2-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.13-bin.zip
 networkTimeout=10000
 validateDistributionUrl=true
 zipStoreBase=GRADLE_USER_HOME
diff --git a/gradlew b/gradlew
index f5feea6d6b116baaca5a2642d4d9fa1f47d574a7..faf93008b77e7b52e18c44e4eef257fc2f8fd76d 100755
--- a/gradlew
+++ b/gradlew
@@ -86,8 +86,7 @@ done
 # shellcheck disable=SC2034
 APP_BASE_NAME=${0##*/}
 # Discard cd standard output in case $CDPATH is set (https://github.com/gradle/gradle/issues/25036)
-APP_HOME=$( cd -P "${APP_HOME:-./}" > /dev/null && printf '%s
-' "$PWD" ) || exit
+APP_HOME=$( cd -P "${APP_HOME:-./}" > /dev/null && printf '%s\n' "$PWD" ) || exit
 
 # Use the maximum available, or set MAX_FD != -1 to use that value.
 MAX_FD=maximum
@@ -206,7 +205,7 @@ fi
 DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
 
 # Collect all arguments for the java command:
-#   * DEFAULT_JVM_OPTS, JAVA_OPTS, JAVA_OPTS, and optsEnvironmentVar are not allowed to contain shell fragments,
+#   * DEFAULT_JVM_OPTS, JAVA_OPTS, and optsEnvironmentVar are not allowed to contain shell fragments,
 #     and any embedded shellness will be escaped.
 #   * For example: A user cannot expect ${Hostname} to be expanded, as it is an environment variable and will be
 #     treated as '${Hostname}' itself on the command line.
diff --git a/src/main/java/de/tlc4b/TLC4BGlobals.java b/src/main/java/de/tlc4b/TLC4BGlobals.java
index 2ae19fc3df4eb8d544b9b0d3d933704fc621f4b5..8653fc4f2a4089a17fece4b65c6210d6fbf7a66d 100644
--- a/src/main/java/de/tlc4b/TLC4BGlobals.java
+++ b/src/main/java/de/tlc4b/TLC4BGlobals.java
@@ -1,5 +1,15 @@
 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() {
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index d6ccdea86faace053e5851b9806f3eb42e5815fb..83d4896c2bcad67713f5b39cba8cf6d21c6b0198 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -4,22 +4,22 @@ import static de.tlc4b.util.StopWatch.Watches.MODEL_CHECKING_TIME;
 
 import java.io.BufferedReader;
 import java.io.File;
-import java.io.FileNotFoundException;
 import java.io.IOException;
 import java.io.InputStream;
 import java.io.InputStreamReader;
-import java.net.UnknownHostException;
 import java.nio.charset.StandardCharsets;
 import java.nio.file.FileSystems;
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.HashSet;
 import java.util.List;
+import java.util.Locale;
 import java.util.Set;
 
 import de.tlc4b.tlc.TLCMessageListener;
 import de.tlc4b.util.StopWatch;
 import tlc2.TLCGlobals;
+import tlc2.tool.fp.FPSetFactory;
 import util.SimpleFilenameToStream;
 import util.ToolIO;
 import tlc2.TLC;
@@ -47,26 +47,26 @@ public class TLCRunner {
 		}
 	}
 
-	private static Process startJVM(final String optionsAsString,
-			final String mainClass, final String[] arguments)
+	private static Process startJVM(final String mainClass, final List<String> arguments)
 			throws IOException {
 
-		String separator = FileSystems.getDefault().getSeparator();
-
-		String jvm = System.getProperty("java.home") + separator + "bin"
-				+ separator + "java";
+		boolean isWindows = System.getProperty("os.name").toLowerCase(Locale.ROOT).startsWith("windows");
+		String jvm = System.getProperty("java.home") + File.separator + "bin" + File.separator + (isWindows ? "java.exe" : "java");
 		String classpath = System.getProperty("java.class.path");
 
-		List<String> command = Arrays.asList(jvm, "-cp", classpath, mainClass);
-		command.addAll(Arrays.asList(arguments));
+		List<String> command = new ArrayList<>();
+		command.add(jvm);
+		command.addAll(Arrays.asList("-XX:+UseParallelGC", "-Dfile.encoding=UTF-8", "-Dtlc2.tool.fp.FPSet.impl=" + FPSetFactory.getImplementationDefault()));
+		command.add(mainClass);
+		command.addAll(arguments);
 
 		ProcessBuilder processBuilder = new ProcessBuilder(command);
+		processBuilder.environment().put("CLASSPATH", classpath);
 		return processBuilder.start();
 	}
 
-	public static ArrayList<String> runTLCInANewJVM(String machineName,
-			String path) throws IOException {
-		ArrayList<String> list = new ArrayList<>();
+	public static ArrayList<String> runTLCInANewJVM(String machineName, String path) throws IOException {
+		List<String> list = new ArrayList<>();
 		list.add(path);
 		list.add(machineName);
 		if (!TLC4BGlobals.isDeadlockCheck()) {
@@ -79,8 +79,7 @@ public class TLCRunner {
 		// list.add("-coverage");
 		// list.add("1");
 
-		String[] args = list.toArray(new String[0]);
-		final Process p = startJVM("", TLCRunner.class.getCanonicalName(), args);
+		final Process p = startJVM(TLCRunner.class.getCanonicalName(), list);
 		StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
 		stdOut.start();
 		StreamGobbler errOut = new StreamGobbler(p.getErrorStream());
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 92de4664c54c76feee80744c02a2d67c0e9c9d49..ff194588996457bf2a9878714cba8103dd67b1bc 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -16,9 +16,6 @@ import de.tlc4b.exceptions.ScopeException;
 import de.tlc4b.ltl.LTLBPredicate;
 import de.tlc4b.ltl.LTLFormulaVisitor;
 
-import static de.tlc4b.util.UtilMethods.getIdentifierExpression;
-import static de.tlc4b.util.UtilMethods.getOperation;
-
 public class MachineContext extends DepthFirstAdapter {
 
 	private String machineName;
@@ -391,7 +388,7 @@ public class MachineContext extends DepthFirstAdapter {
 
 	private void extractIdentifierExpressions(List<PExpression> copy, Map<String, Node> addToMap) {
 		for (PExpression e : copy) {
-			AIdentifierExpression identifier = getIdentifierExpression(e);
+			AIdentifierExpression identifier = (AIdentifierExpression) e;
 			String name = Utils.getTIdentifierListAsString(identifier.getIdentifier());
 			exist(identifier.getIdentifier());
 			addToMap.put(name, identifier);
@@ -557,7 +554,7 @@ public class MachineContext extends DepthFirstAdapter {
 		List<POperation> copy = new ArrayList<>(node.getOperations());
 		// first collect all operations
 		for (POperation e : copy) {
-			AOperation op = getOperation(e);
+			AOperation op = (AOperation) e;
 			String name = Utils.getTIdentifierListAsString(op.getOpName());
 			// existString(name);
 			if (operations.containsKey(name)) {
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index 907739f9ce192973a7b0a26cc49769da05f31c35..d98a9ffe40983a34cb856a37234bb8579d71315a 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -147,13 +147,11 @@ public class Renamer extends DepthFirstAdapter {
 		for (PDefinition e : copy) {
 			String name = null;
 			if (e instanceof AExpressionDefinitionDefinition) {
-				name = ((AExpressionDefinitionDefinition) e).getName()
-						.getText();
+				name = ((AExpressionDefinitionDefinition) e).getName().getText();
 			} else if (e instanceof APredicateDefinitionDefinition) {
 				name = ((APredicateDefinitionDefinition) e).getName().getText();
 			} else if (e instanceof ASubstitutionDefinitionDefinition) {
-				name = ((ASubstitutionDefinitionDefinition) e).getName()
-						.getText();
+				name = ((ASubstitutionDefinitionDefinition) e).getName().getText();
 			}
 			String newName = incName(name);
 			namesTable.put(e, newName);
diff --git a/src/main/java/de/tlc4b/analysis/Typechecker.java b/src/main/java/de/tlc4b/analysis/Typechecker.java
index b76c6da8037890f5c2239271e034afd76e7247a1..01baa17b896614ef4e2373e41687de9a4ad11b50 100644
--- a/src/main/java/de/tlc4b/analysis/Typechecker.java
+++ b/src/main/java/de/tlc4b/analysis/Typechecker.java
@@ -30,8 +30,6 @@ import de.tlc4b.exceptions.UnificationException;
 import de.tlc4b.ltl.LTLBPredicate;
 import de.tlc4b.ltl.LTLFormulaVisitor;
 
-import static de.tlc4b.util.UtilMethods.getIdentifierExpression;
-
 /**
  * TODO we need a second run over the AST to check if all local variables have a
  * type. This run should be performed after the normal model checking task.
@@ -181,25 +179,25 @@ public class Typechecker extends DepthFirstAdapter implements ITypechecker {
 	@Override
 	public void caseAConstantsMachineClause(AConstantsMachineClause node) {
 		List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
-		copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType()));
+		copy.forEach(e -> setType(e, new UntypedType()));
 	}
 
 	@Override
 	public void caseAAbstractConstantsMachineClause(AAbstractConstantsMachineClause node) {
 		List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
-		copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType()));
+		copy.forEach(e -> setType(e, new UntypedType()));
 	}
 
 	@Override
 	public void caseAVariablesMachineClause(AVariablesMachineClause node) {
 		List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
-		copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType()));
+		copy.forEach(e -> setType(e, new UntypedType()));
 	}
 
 	@Override
 	public void caseAConcreteVariablesMachineClause(AConcreteVariablesMachineClause node) {
 		List<PExpression> copy = new ArrayList<>(node.getIdentifiers());
-		copy.forEach(e -> setType(getIdentifierExpression(e), new UntypedType()));
+		copy.forEach(e -> setType(e, new UntypedType()));
 	}
 
 	/**
diff --git a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
index 21ddc60bca560bdd8223a0e7f5e239fe0586d3ee..1860cd30b40c0e5ea2cf3eb012a5032fa82d18d2 100644
--- a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
+++ b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
@@ -76,4 +76,34 @@ public class UnsupportedConstructsFinder extends DepthFirstAdapter {
 		}
 	}
 
+	// quick fix: ignore labels and descriptions FIXME: improve
+	@Override
+	public void caseALabelPredicate(ALabelPredicate node) {
+		node.getPredicate().apply(this);
+		node.replaceBy(node.getPredicate());
+	}
+
+	@Override
+	public void caseADescriptionPredicate(ADescriptionPredicate node) {
+		node.getPredicate().apply(this);
+		node.replaceBy(node.getPredicate());
+	}
+
+	@Override
+	public void caseADescriptionExpression(ADescriptionExpression node) {
+		node.getExpression().apply(this);
+		node.replaceBy(node.getExpression());
+	}
+
+	@Override
+	public void caseADescriptionOperation(ADescriptionOperation node) {
+		node.getOperation().apply(this);
+		node.replaceBy(node.getOperation());
+	}
+
+	@Override
+	public void caseADescriptionSet(ADescriptionSet node) {
+		node.getSet().apply(this);
+		node.replaceBy(node.getSet());
+	}
 }
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
deleted file mode 100644
index ee05bf463a8eeee5c85ca5618fb1377f0a7be5bf..0000000000000000000000000000000000000000
--- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionCollector.java
+++ /dev/null
@@ -1,96 +0,0 @@
-package de.tlc4b.analysis.transformation;
-
-import java.util.Hashtable;
-
-import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
-import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
-import de.be4.classicalb.core.parser.node.AExpressionDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.AInitialisationMachineClause;
-import de.be4.classicalb.core.parser.node.AInvariantMachineClause;
-import de.be4.classicalb.core.parser.node.ALocalOperationsMachineClause;
-import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
-import de.be4.classicalb.core.parser.node.APredicateDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
-import de.be4.classicalb.core.parser.node.ASubstitutionDefinitionDefinition;
-import de.be4.classicalb.core.parser.node.PDefinition;
-import de.be4.classicalb.core.parser.node.Start;
-
-/**
- * This class only collects all Definitions of a Machine. Definitions of other
- * files which are included are not contained.
- */
-
-public class DefinitionCollector extends DepthFirstAdapter {
-
-	private final Hashtable<String, PDefinition> definitionsTable;
-	private ADefinitionsMachineClause definitionsMachineClause;
-
-	public Hashtable<String, PDefinition> getDefinitions() {
-		return new Hashtable<>(definitionsTable);
-	}
-
-	public ADefinitionsMachineClause getDefinitionsMachineClause() {
-		return this.definitionsMachineClause;
-	}
-
-	public DefinitionCollector(Start tree) {
-		definitionsTable = new Hashtable<>();
-		tree.apply(this);
-	}
-
-	@Override
-	public void inADefinitionsMachineClause(ADefinitionsMachineClause node) {
-		this.definitionsMachineClause = node;
-	}
-
-	@Override
-	public void caseAPredicateDefinitionDefinition(
-			APredicateDefinitionDefinition node) {
-		definitionsTable.put(node.getName().getText(), node);
-	}
-
-	@Override
-	public void caseASubstitutionDefinitionDefinition(
-			ASubstitutionDefinitionDefinition node) {
-		definitionsTable.put(node.getName().getText(), node);
-	}
-
-	@Override
-	public void caseAExpressionDefinitionDefinition(
-			AExpressionDefinitionDefinition node) {
-		definitionsTable.put(node.getName().getText(), node);
-	}
-
-	/***************************************************************************
-	 * exclude large sections of a machine without machine references by doing
-	 * nothing
-	 */
-
-	@Override
-	public void caseAConstraintsMachineClause(AConstraintsMachineClause node) {
-	}
-
-	@Override
-	public void caseAInvariantMachineClause(AInvariantMachineClause node) {
-	}
-
-	@Override
-	public void caseAOperationsMachineClause(AOperationsMachineClause node) {
-	}
-
-	@Override
-	public void caseAPropertiesMachineClause(APropertiesMachineClause node) {
-	}
-
-	@Override
-	public void caseAInitialisationMachineClause(
-			AInitialisationMachineClause node) {
-	}
-
-	@Override
-	public void caseALocalOperationsMachineClause(
-			ALocalOperationsMachineClause node) {
-	}
-
-}
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
index 4837b2b3bc425abdc7f18f7ab36f9a4ba89034bc..0c6cc9339633b628da5307bd08cd989d8c24e16f 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
@@ -4,7 +4,10 @@ import java.util.ArrayList;
 import java.util.Hashtable;
 import java.util.List;
 
+import de.be4.classicalb.core.parser.Definitions;
+import de.be4.classicalb.core.parser.IDefinitions;
 import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.analysis.checking.DefinitionCollector;
 import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit;
 import de.be4.classicalb.core.parser.node.ADefinitionExpression;
 import de.be4.classicalb.core.parser.node.ADefinitionPredicate;
@@ -34,7 +37,7 @@ import de.tlc4b.analysis.StandardModules;
  */
 public class DefinitionsEliminator extends DepthFirstAdapter {
 
-	private final Hashtable<String, PDefinition> definitionsTable;
+	private final IDefinitions definitions = new Definitions();
 	private final ArrayList<Hashtable<String, PExpression>> contextStack;
 
 	public static void eliminateDefinitions(Start start){
@@ -42,8 +45,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 	}
 	
 	private DefinitionsEliminator(Start node) {
-		DefinitionCollector collector = new DefinitionCollector(node);
-		definitionsTable = collector.getDefinitions();
+		new DefinitionCollector(definitions).collectDefinitions(node);
 		contextStack = new ArrayList<>();
 		node.apply(this);
 	}
@@ -113,7 +115,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 	@Override
 	public void caseADefinitionSubstitution(ADefinitionSubstitution node) {
 		String name = node.getDefLiteral().getText();
-		PDefinition def = definitionsTable.get(name);
+		PDefinition def = definitions.getDefinition(name);
 
 		ASubstitutionDefinitionDefinition clone = (ASubstitutionDefinitionDefinition) def.clone();
 		Hashtable<String, PExpression> context = new Hashtable<>();
@@ -144,7 +146,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 			return;
 		}
 
-		PDefinition def = definitionsTable.get(name);
+		PDefinition def = definitions.getDefinition(name);
 		AExpressionDefinitionDefinition clone = (AExpressionDefinitionDefinition) def.clone();
 		Hashtable<String, PExpression> context = new Hashtable<>();
 
@@ -164,7 +166,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 	@Override
 	public void caseADefinitionPredicate(ADefinitionPredicate node) {
 		String name = node.getDefLiteral().getText();
-		PDefinition def = definitionsTable.get(name);
+		PDefinition def = definitions.getDefinition(name);
 
 		ArrayList<PExpression> arguments = new ArrayList<>(node.getParameters());
 		if (StandardModules.isKeywordInModuleExternalFunctions(name)) {
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 479abd532fecaa8a83f1cd20b2370cc3ae426a9e..2d2a7d6d3852312a1a6691e4034d366513b9b58b 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -53,7 +53,6 @@ import de.tlc4b.analysis.Typechecker;
 import de.tlc4b.btypes.BType;
 import de.tlc4b.exceptions.NotSupportedException;
 import de.tlc4b.ltl.LTLFormulaVisitor;
-import de.tlc4b.util.UtilMethods;
 
 public class TypeRestrictor extends DepthFirstAdapter {
 
@@ -500,12 +499,10 @@ public class TypeRestrictor extends DepthFirstAdapter {
 					AIdentifierExpression id = (AIdentifierExpression) e;
 					String localVariableName = Utils.getTIdentifierListAsString(id.getIdentifier());
 					throw new NotSupportedException(
-							"Unable to restrict the type '"
-									+ conType
-									+ "' of identifier '"
-									+ localVariableName
+							"Unable to restrict the type '" + conType + "' of identifier '" + localVariableName
 									+ "' to a finite set. TLC is not able to handle infinite sets.\n"
-									+ UtilMethods.getPositionAsString(e));
+									+ (e.getStartPos() == null ? "### Unknown position."
+											: "### Line " + e.getStartPos().getLine() + ", Column " + e.getEndPos().getPos()));
 				}
 
 				tree = conType.createASTNode(typechecker);
diff --git a/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java b/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
index e20b807696b7448adcd7d8c3fbb0e87f592cdbec..05cfb6a61e83473ab3b78723ed0b92e9c820321b 100644
--- a/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
+++ b/src/main/java/de/tlc4b/btypes/EnumeratedSetElement.java
@@ -2,9 +2,9 @@ package de.tlc4b.btypes;
 
 import de.be4.classicalb.core.parser.node.AIdentifierExpression;
 import de.be4.classicalb.core.parser.node.PExpression;
+import de.be4.classicalb.core.parser.util.ASTBuilder;
 import de.tlc4b.analysis.Typechecker;
 import de.tlc4b.exceptions.UnificationException;
-import de.tlc4b.util.UtilMethods;
 
 public class EnumeratedSetElement implements BType {
 	private final String name;
@@ -58,7 +58,7 @@ public class EnumeratedSetElement implements BType {
 	}
 
 	public PExpression createASTNode(Typechecker typechecker) {
-		AIdentifierExpression id = UtilMethods.createAIdentifierExpression(name);
+		AIdentifierExpression id = ASTBuilder.createIdentifier(name);
 		typechecker.setType(id, new SetType(this));
 		return id;
 	}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 7c6f9510cece6e8bb051d46fa3600dbc4a4914ce..b43f7a120d8d5a01f9d2dda0b1119daab672ecc5 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -247,16 +247,14 @@ public class TLAPrinter extends DepthFirstAdapter {
 			}
 		}
 		// CONSTANTS
-		ArrayList<ConfigFileAssignment> assignments = configFile
-				.getAssignments();
+		List<ConfigFileAssignment> assignments = configFile.getAssignments();
 		if (!assignments.isEmpty()) {
 			configFileString.append("CONSTANTS\n");
 			for (ConfigFileAssignment assignment : assignments) {
 				configFileString.append(assignment.getString(renamer));
 			}
 		}
-		if (TLC4BGlobals.useSymmetry()
-				&& !machineContext.getDeferredSets().isEmpty()) {
+		if (TLC4BGlobals.useSymmetry() && !machineContext.getDeferredSets().isEmpty()) {
 			configFileString.append("SYMMETRY Symmetry\n");
 		}
 
diff --git a/src/main/java/de/tlc4b/tla/ConfigFile.java b/src/main/java/de/tlc4b/tla/ConfigFile.java
index 456c37d07d71ba7beaf39a93fbf91598e53b2fb4..9ae6778c49709e39312cd5a1e0b5ef6517763d67 100644
--- a/src/main/java/de/tlc4b/tla/ConfigFile.java
+++ b/src/main/java/de/tlc4b/tla/ConfigFile.java
@@ -1,46 +1,41 @@
 package de.tlc4b.tla;
 
 import java.util.ArrayList;
+import java.util.List;
 
 import de.tlc4b.tla.config.ConfigFileAssignment;
 
-
 public class ConfigFile {
 
-	private final ArrayList<ConfigFileAssignment> assignments;
+	private final List<ConfigFileAssignment> assignments;
 	private int invariantNumber;
 	private boolean spec;
 	private boolean init;
 	private boolean next;
 	private int assertionsSize;
 	private boolean goal;
-	
-	
-	public ConfigFile(){
+
+	public ConfigFile() {
 		this.assignments = new ArrayList<>();
 		this.invariantNumber = 0;
 	}
 
-
-	public ArrayList<ConfigFileAssignment> getAssignments() {
+	public List<ConfigFileAssignment> getAssignments() {
 		return assignments;
 	}
 
 	public boolean isSpec(){
 		return spec;
 	}
-	
 
 	public void setInvariantNumber(int number) {
 		this.invariantNumber = number;
 	}
 
-
 	public boolean isInit() {
 		return init;
 	}
 
-
 	public boolean isNext() {
 		return next;
 	}
@@ -49,22 +44,18 @@ public class ConfigFile {
 		assignments.add(assignment);
 	}
 
-
 	public int getInvariantNumber() {
 		return this.invariantNumber;
 	}
 
-
 	public void setInit() {
 		this.init = true;
 	}
 
-
 	public void setNext() {
 		this.next = true;
 	}
 
-
 	public void setAssertionSize(int size) {
 		assertionsSize = size;
 	}
diff --git a/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java b/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
index 64b0fafa49eb5626bcfb1d2fdbcd9cc87ef01421..e74f20da48dab142b531808c02ecbca16bc6bfc2 100644
--- a/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/ConfigFileAssignment.java
@@ -2,6 +2,7 @@ package de.tlc4b.tla.config;
 
 import java.util.ArrayList;
 import java.util.List;
+import java.util.stream.Collectors;
 
 import de.be4.classicalb.core.parser.node.AIdentifierExpression;
 import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
@@ -12,14 +13,9 @@ public abstract class ConfigFileAssignment {
 	public abstract String getString(Renamer renamer);
 	
 	public String getIdentifier(AIdentifierExpression node) {
-		StringBuilder res = new StringBuilder();
-		
-		List<TIdentifierLiteral> copy = new ArrayList<>(
-				node.getIdentifier());
-		for (TIdentifierLiteral e : copy) {
-			res.append(e.getText());
-		}
-		return res.toString();
+		return node.getIdentifier().stream()
+				.map(TIdentifierLiteral::getText)
+				.collect(Collectors.joining());
 	}
 	
 }
diff --git a/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java b/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java
index a92f63620687d0e86a29aecc633c2c7d86087674..d341ca8ccb0f334d0fdd1f3effb6201f27b093c3 100644
--- a/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/ModelValueAssignment.java
@@ -13,9 +13,7 @@ public class ModelValueAssignment extends ConfigFileAssignment{
 
 	public String getString(Renamer renamer) {
 		AIdentifierExpression id = (AIdentifierExpression) node;
-		getIdentifier(id);
 		String conString = renamer.getNameOfRef(id);
-		return conString+ " = "+ conString +"\n";
+		return conString + " = " + conString + "\n";
 	}
-	
 }
diff --git a/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java b/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
index 5d0607d6c77f1456d68f6c4dc31b68150a4657f2..b05655464bb39c8efbee976e0f0c97ce319a9206 100644
--- a/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
+++ b/src/main/java/de/tlc4b/tla/config/SetOfModelValuesAssignment.java
@@ -1,62 +1,39 @@
 package de.tlc4b.tla.config;
 
-import java.util.List;
-
 import de.be4.classicalb.core.parser.node.ADeferredSetSet;
 import de.be4.classicalb.core.parser.node.AIdentifierExpression;
 import de.be4.classicalb.core.parser.node.Node;
-import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
 import de.tlc4b.TLC4BGlobals;
 import de.tlc4b.analysis.Renamer;
 
+import java.util.stream.Collectors;
+import java.util.stream.IntStream;
+
 /**
  * 
  * This class represents an assignment in the configuration file. The left side
  * of the assignment is a constant and the right side a set of model values.
  * E.g. k = {k1, k2, k3}
  */
-
 public class SetOfModelValuesAssignment extends ConfigFileAssignment {
 	private final Node node;
 	private final int size;
 
 	public SetOfModelValuesAssignment(Node node, Integer size) {
 		this.node = node;
-		if (size == null) {
-			this.size = TLC4BGlobals.getDEFERRED_SET_SIZE();
-		} else {
-			this.size = size;
-		}
-
+		this.size = size == null ? TLC4BGlobals.getDEFERRED_SET_SIZE() : size;
 	}
 
 	public String getString(Renamer renamer) {
-		StringBuilder res = new StringBuilder();
-
-		StringBuilder conString;
+		String conString;
 		if (node instanceof ADeferredSetSet) {
-			conString = new StringBuilder();
-			List<TIdentifierLiteral> copy = ((ADeferredSetSet) node)
-					.getIdentifier();
-			for (TIdentifierLiteral e : copy) {
-				conString.append(e.getText());
-			}
-			conString = new StringBuilder(renamer.getName(node));
+			conString = renamer.getName(node);
 		} else {
-			AIdentifierExpression id = (AIdentifierExpression) node;
-			conString = new StringBuilder(getIdentifier(id));
+			conString = getIdentifier((AIdentifierExpression) node);
 		}
 
-		res.append(conString).append(" = {");
-		for (int j = 1; j < size + 1; j++) {
-			res.append(conString).append(j);
-			if (j < size) {
-				res.append(",");
-			}
-		}
-		res.append("}\n");
-
-		return res.toString();
+		return conString + " = {" +
+				IntStream.rangeClosed(1, size).mapToObj(j -> conString + j).collect(Collectors.joining(",")) +
+				"}\n";
 	}
-
 }
diff --git a/src/main/java/de/tlc4b/tlc/TLCMessageListener.java b/src/main/java/de/tlc4b/tlc/TLCMessageListener.java
index d1f276a0f16cc859aa72fd3713946d39de098f50..5692318643a55d9ca80d2cccc9a8534187eddc9f 100644
--- a/src/main/java/de/tlc4b/tlc/TLCMessageListener.java
+++ b/src/main/java/de/tlc4b/tlc/TLCMessageListener.java
@@ -1,7 +1,7 @@
 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++) {
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index ed5a7bd500f44cc89c37fd010b25a63e8e70bfdd..1a5407bd1ace82e3187999fd9d092928b3d9e34d 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -63,14 +63,11 @@ public class TLCOutputInfo {
 		identifiers.putAll(machineContext.getEnumValues());
 		//TODO add sets of modelvalues
 		
-		
-		for (Entry<String, Node> entry : identifiers.entrySet()) {
-			String name = entry.getKey();
-			Node node = entry.getValue();
+		identifiers.forEach((name, node) -> {
 			String newName = renamer.getNameOfRef(node);
 			namesMapping.put(newName, name);
 			typesTable.put(newName, typechecker.getType(node));
-		}
+		});
 	}
 
 }
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index 8864a40ba9afeac78499c022c460ddfb27445208..db983c9e797aa425c0f7a84789d49b2e2dfed080 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/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
diff --git a/src/main/java/de/tlc4b/tlc/TracePrinter.java b/src/main/java/de/tlc4b/tlc/TracePrinter.java
index 6e5fd3eb22f8e87fe234dd31ac78ec7c84c8e848..7a4d7dc3b154d393f2b222e110368e33eb8ceeba 100644
--- a/src/main/java/de/tlc4b/tlc/TracePrinter.java
+++ b/src/main/java/de/tlc4b/tlc/TracePrinter.java
@@ -147,8 +147,7 @@ public class TracePrinter {
 				} else {
 					BType subtype = ((FunctionType) type).getRange();
 					res.append("[");
-					res.append(parseEnumerationValue(((TupleValue) val).elems,
-							subtype));
+					res.append(parseEnumerationValue(((TupleValue) val).elems, subtype));
 					res.append("]");
 				}
 				return res;
diff --git a/src/main/java/de/tlc4b/util/UtilMethods.java b/src/main/java/de/tlc4b/util/UtilMethods.java
deleted file mode 100644
index 2e824b3dfc82c032a7c063d09142440a9e3d82c2..0000000000000000000000000000000000000000
--- a/src/main/java/de/tlc4b/util/UtilMethods.java
+++ /dev/null
@@ -1,57 +0,0 @@
-package de.tlc4b.util;
-
-import java.util.ArrayList;
-
-import de.be4.classicalb.core.parser.node.*;
-import de.hhu.stups.sablecc.patch.SourcePosition;
-
-public class UtilMethods {
-
-	public static AIdentifierExpression createAIdentifierExpression(String name) {
-		TIdentifierLiteral literal = new TIdentifierLiteral(name);
-		ArrayList<TIdentifierLiteral> idList = new ArrayList<>();
-		idList.add(literal);
-		return new AIdentifierExpression(idList);
-	}
-
-	public static AIdentifierExpression getIdentifierExpression(PExpression e) {
-		AIdentifierExpression identifier;
-		if (e instanceof ADescriptionExpression) {
-			identifier = getIdentifierExpression(((ADescriptionExpression) e).getExpression());
-		} else if (e instanceof AIdentifierExpression) {
-			identifier = (AIdentifierExpression) e;
-		} else {
-			throw new IllegalStateException("Unexpected expression type: " + e);
-		}
-		return identifier;
-	}
-
-	public static AOperation getOperation(POperation e) {
-		AOperation op;
-		if (e instanceof ADescriptionOperation) {
-			op = getOperation(((ADescriptionOperation) e).getOperation());
-		} else if (e instanceof AOperation) {
-			op = (AOperation) e;
-		} else {
-			throw new IllegalStateException("Unexpected operation type: " + e);
-		}
-		return op;
-	}
-
-	public static String getPositionAsString(Node node) {
-		StringBuilder sb = new StringBuilder();
-		SourcePosition startPos = node.getStartPos();
-		SourcePosition endPos = node.getEndPos();
-		if (startPos == null) {
-			sb.append("### Unknown position.");
-		} else {
-			sb.append("### Line ");
-			sb.append(startPos.getLine());
-			sb.append(", Column ");
-			sb.append(endPos.getPos());
-		}
-
-		return sb.toString();
-	}
-
-}
diff --git a/src/test/java/de/tlc4b/analysis/ConstantsTest.java b/src/test/java/de/tlc4b/analysis/ConstantsTest.java
index fc42e4d2d88e8a69a8b32fe067820f67407884fd..73ddb1a5279a2c6d0374624059aac59e8d4c52e5 100644
--- a/src/test/java/de/tlc4b/analysis/ConstantsTest.java
+++ b/src/test/java/de/tlc4b/analysis/ConstantsTest.java
@@ -147,5 +147,31 @@ public class ConstantsTest {
 				+ "======";
 		compare(expected, machine);
 	}
+
+	@Test
+	public void testPropertiesDescPragma() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "CONSTANTS n\n"
+				+ "PROPERTIES n = 1 /*@desc description*/\n"
+				+ "END";
+
+		String expected = "---- MODULE test----\n"
+				+ "n == 1\n"
+				+ "======";
+		compare(expected, machine);
+	}
+
+	@Test
+	public void testPropertiesLabelAndDescPragma() throws Exception {
+		String machine = "MACHINE test\n"
+				+ "CONSTANTS n\n"
+				+ "PROPERTIES /*@label lbl1 */ n = 1 /*@desc description*/\n"
+				+ "END";
+
+		String expected = "---- MODULE test----\n"
+				+ "n == 1\n"
+				+ "======";
+		compare(expected, machine);
+	}
 	
 }