diff --git a/Makefile b/Makefile
deleted file mode 100644
index edcdcde56c97aca593c770a160f2c0420b2f0122..0000000000000000000000000000000000000000
--- a/Makefile
+++ /dev/null
@@ -1,8 +0,0 @@
-.PHONY: build
-build:
-	./gradlew createJar
-
-.PHONY: install
-install:
-	echo "installing to local probcli/lib folder:"
-	cp build/libs/tlc4b-1.0.*.jar ../../prob_prolog/lib/TLC4B.jar 
diff --git a/build.gradle b/build.gradle
index 561ade0971b4f9d78166a6416888c93251dad67c..88e3609a56ebe14eb76303c31379521e641d7c24 100644
--- a/build.gradle
+++ b/build.gradle
@@ -7,7 +7,7 @@ plugins {
 	id "de.undercouch.download" version "5.4.0"
 }
 
-project.version = '1.0.5'
+project.version = '1.1.0'
 project.group = 'de.hhu.stups'
 
 final isSnapshot = project.version.endsWith("-SNAPSHOT")
@@ -26,24 +26,23 @@ configurations.all {
 	resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
 }
 
-def parser_version = '2.9.25'
-def tlatools_version = '1.0.2'
+def parser_version = '2.12.4'
 
 dependencies {
 	//implementation(group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
 	implementation(group: 'commons-cli', name: 'commons-cli', version: '1.5.0')
-	implementation(group: 'de.hhu.stups', name: 'tlatools', version: tlatools_version)
+	implementation(group: 'de.hhu.stups', name: 'tlatools', version: '1.0.2')
 
 	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.1.3')
+	testImplementation(group: 'de.hhu.stups', name: 'tla2bAST', version: '1.1.5')
 }
 
 java {
-	project.sourceCompatibility = JavaVersion.VERSION_1_7
-	project.targetCompatibility = JavaVersion.VERSION_1_7
+	project.sourceCompatibility = JavaVersion.VERSION_1_8
+	project.targetCompatibility = JavaVersion.VERSION_1_8
 	
 	withSourcesJar()
 	withJavadocJar()
@@ -77,8 +76,13 @@ task downloadPublicExamples(type: Download) {
 }
 
 task extractPublicExamples(dependsOn: downloadPublicExamples, type: Copy) {
+	final outDir = "${buildDir}/prob_examples"
+	doFirst {
+		delete(outDir)
+	}
+	
 	from tarTree(resources.gzip("${buildDir}/ProB_public_examples.tgz"))
-	into "${buildDir}/prob_examples"
+	into outDir
 	include "public_examples/TLC/**"
 }
 
@@ -100,16 +104,6 @@ task jacocoIntegrationTestReport(type: JacocoReport) {
 	executionData fileTree(project.rootDir.absolutePath).include("**/build/jacoco/*.exec")
 }
 
-task createJar(type: Jar, dependsOn: build){
-	archiveFileName = 'TLC4B.jar'
-	from sourceSets.main.output
-	from {configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
-	exclude('**/*.java')
-	manifest {
-		attributes "Main-Class" : 'de.tlc4b.TLC4B'
-	}
-}
-
 publishing {
 	publications {
 		mavenJava(MavenPublication) {
diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar
index 943f0cbfa754578e88a3dae77fce6e3dea56edbf..c1962a79e29d3e0ab67b14947c167a862655af9b 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 508322917bdcd5b42c43cf8ce0d1f9269226a405..37aef8d3f0c9fffa920a8290320a6c78095e1591 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-7.6.1-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip
 networkTimeout=10000
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists
diff --git a/gradlew b/gradlew
index 65dcd68d65c82f2a5338fded4af852f9caf93b93..aeb74cbb43e3931a2455a838345c3f6b8131aaa2 100755
--- a/gradlew
+++ b/gradlew
@@ -85,9 +85,6 @@ done
 APP_BASE_NAME=${0##*/}
 APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit
 
-# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
-DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
-
 # Use the maximum available, or set MAX_FD != -1 to use that value.
 MAX_FD=maximum
 
@@ -144,7 +141,7 @@ if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then
     case $MAX_FD in #(
       max*)
         # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked.
-        # shellcheck disable=SC3045 
+        # shellcheck disable=SC3045
         MAX_FD=$( ulimit -H -n ) ||
             warn "Could not query maximum file descriptor limit"
     esac
@@ -152,7 +149,7 @@ if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then
       '' | soft) :;; #(
       *)
         # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked.
-        # shellcheck disable=SC3045 
+        # shellcheck disable=SC3045
         ulimit -n "$MAX_FD" ||
             warn "Could not set maximum file descriptor limit to $MAX_FD"
     esac
@@ -197,6 +194,10 @@ if "$cygwin" || "$msys" ; then
     done
 fi
 
+
+# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
+DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
+
 # Collect all arguments for the java command;
 #   * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of
 #     shell script including quotes and variable substitutions, so put them in
diff --git a/src/main/java/de/tlc4b/analysis/MachineContext.java b/src/main/java/de/tlc4b/analysis/MachineContext.java
index 184f6bd70abff3acc9d02a697ac20894ce4dda18..3bcadcdd318d593c6efad2ce7228477382440c63 100644
--- a/src/main/java/de/tlc4b/analysis/MachineContext.java
+++ b/src/main/java/de/tlc4b/analysis/MachineContext.java
@@ -38,6 +38,7 @@ import de.be4.classicalb.core.parser.node.AInvariantMachineClause;
 import de.be4.classicalb.core.parser.node.ALambdaExpression;
 import de.be4.classicalb.core.parser.node.ALetSubstitution;
 import de.be4.classicalb.core.parser.node.AMachineHeader;
+import de.be4.classicalb.core.parser.node.AMachineReferenceNoParams;
 import de.be4.classicalb.core.parser.node.AOpSubstitution;
 import de.be4.classicalb.core.parser.node.AOperation;
 import de.be4.classicalb.core.parser.node.AOperationsMachineClause;
@@ -58,6 +59,7 @@ import de.be4.classicalb.core.parser.node.PDefinition;
 import de.be4.classicalb.core.parser.node.PExpression;
 import de.be4.classicalb.core.parser.node.PMachineClause;
 import de.be4.classicalb.core.parser.node.PMachineHeader;
+import de.be4.classicalb.core.parser.node.PMachineReferenceNoParams;
 import de.be4.classicalb.core.parser.node.POperation;
 import de.be4.classicalb.core.parser.node.PPredicate;
 import de.be4.classicalb.core.parser.node.PSet;
@@ -90,7 +92,7 @@ public class MachineContext extends DepthFirstAdapter {
 	private final LinkedHashMap<String, Node> constants;
 	private final LinkedHashMap<String, Node> definitions;
 	private final LinkedHashMap<String, Node> operations;
-	private final LinkedHashMap<String, AIdentifierExpression> seenMachines;
+	private final LinkedHashMap<String, AMachineReferenceNoParams> seenMachines;
 
 	private PMachineHeader header;
 	private AAbstractMachineParseUnit abstractMachineParseUnit;
@@ -124,7 +126,7 @@ public class MachineContext extends DepthFirstAdapter {
 		this.variables = new LinkedHashMap<String, Node>();
 		this.definitions = new LinkedHashMap<String, Node>();
 		this.operations = new LinkedHashMap<String, Node>();
-		this.seenMachines = new LinkedHashMap<String, AIdentifierExpression>();
+		this.seenMachines = new LinkedHashMap<>();
 	}
 
 	public void analyseMachine() {
@@ -383,13 +385,12 @@ public class MachineContext extends DepthFirstAdapter {
 	@Override
 	public void caseASeesMachineClause(ASeesMachineClause node) {
 		this.seesMachineClause = node;
-		List<PExpression> copy = new ArrayList<PExpression>(node.getMachineNames());
-		for (PExpression e : copy) {
-			AIdentifierExpression p = (AIdentifierExpression) e;
-			String name = Utils.getTIdentifierListAsString(p.getIdentifier());
+		for (PMachineReferenceNoParams e : new ArrayList<>(node.getMachineNames())) {
+			AMachineReferenceNoParams p = (AMachineReferenceNoParams) e;
+			String name = Utils.getTIdentifierListAsString(p.getMachineName());
 
 			try {
-				exist(p.getIdentifier());
+				identifierAlreadyExists(name);
 			} catch (ScopeException e2) {
 				throw new ScopeException("Machine '" + name + "' is seen twice.");
 			}
@@ -966,7 +967,7 @@ public class MachineContext extends DepthFirstAdapter {
 		return new LinkedHashMap<>(enumValues);
 	}
 
-	public LinkedHashMap<String, AIdentifierExpression> getSeenMachines() {
+	public LinkedHashMap<String, AMachineReferenceNoParams> getSeenMachines() {
 		return new LinkedHashMap<>(seenMachines);
 	}
 
diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
index 3831adefc9894707cb2605d5c0d5a5e8aa45a5ce..c872e28c92bc150f52e2291f1e6dab64daf54a0c 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java
@@ -81,12 +81,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 			if (e instanceof AExpressionDefinitionDefinition) {
 				String name = ((AExpressionDefinitionDefinition) e).getName()
 						.getText().toString();
-				if (name.startsWith("ASSERT_LTL")
-						|| name.startsWith("scope_")
-						|| name.startsWith("SET_PREF_")
-						|| name.equals("VISB_JSON_FILE")
-						|| name.startsWith("ANIMATION_FUNCTION")
-						|| name.startsWith("ANIMATION_IMG"))
+				if (Utils.isProBSpecialDefinitionName(name))
 					continue;
 			}
 			e.apply(this);
@@ -100,12 +95,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 
 				String name = ((AExpressionDefinitionDefinition) e).getName()
 						.getText().toString();
-				if (name.startsWith("ASSERT_LTL")
-						|| name.startsWith("scope_")
-						|| name.startsWith("SET_PREF_")
-						|| name.equals("VISB_JSON_FILE")
-						|| name.startsWith("ANIMATION_FUNCTION")
-						|| name.startsWith("ANIMATION_IMG")
+				if (Utils.isProBSpecialDefinitionName(name)
 						|| StandardMadules
 								.isKeywordInModuleExternalFunctions(name)) {
 
@@ -114,7 +104,7 @@ public class DefinitionsEliminator extends DepthFirstAdapter {
 			} else if (e instanceof APredicateDefinitionDefinition) {
 				String name = ((APredicateDefinitionDefinition) e).getName()
 						.getText().toString();
-				if (name.equals("GOAL")
+				if (Utils.isProBSpecialDefinitionName(name)
 						|| StandardMadules
 								.isKeywordInModuleExternalFunctions(name)) {
 					newDefinitionsList.add(e);
diff --git a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
index fb46a533605db50d523fd85450eef4f3553e5df3..aa51bfa00aae1b1d3336b88f06865bb29ce78e50 100644
--- a/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
+++ b/src/main/java/de/tlc4b/analysis/transformation/SeesEliminator.java
@@ -13,12 +13,13 @@ import de.be4.classicalb.core.parser.node.AAssertionsMachineClause;
 import de.be4.classicalb.core.parser.node.AConjunctPredicate;
 import de.be4.classicalb.core.parser.node.AConstantsMachineClause;
 import de.be4.classicalb.core.parser.node.ADefinitionsMachineClause;
-import de.be4.classicalb.core.parser.node.AIdentifierExpression;
+import de.be4.classicalb.core.parser.node.AMachineReferenceNoParams;
 import de.be4.classicalb.core.parser.node.APropertiesMachineClause;
 import de.be4.classicalb.core.parser.node.ASeesMachineClause;
 import de.be4.classicalb.core.parser.node.PDefinition;
 import de.be4.classicalb.core.parser.node.PExpression;
 import de.be4.classicalb.core.parser.node.PMachineClause;
+import de.be4.classicalb.core.parser.node.PMachineReferenceNoParams;
 import de.be4.classicalb.core.parser.node.PParseUnit;
 import de.be4.classicalb.core.parser.node.PPredicate;
 import de.be4.classicalb.core.parser.node.Start;
@@ -52,11 +53,10 @@ public class SeesEliminator extends DepthFirstAdapter {
 	}
 
 	public void inASeesMachineClause(ASeesMachineClause node) {
-		LinkedList<PExpression> machineNames = node.getMachineNames();
-		for (PExpression pExpression : machineNames) {
-			AIdentifierExpression id = (AIdentifierExpression) pExpression;
+		for (PMachineReferenceNoParams pExpression : node.getMachineNames()) {
+			AMachineReferenceNoParams id = (AMachineReferenceNoParams) pExpression;
 			String machineName = Utils
-					.getTIdentifierListAsString(id.getIdentifier());
+					.getTIdentifierListAsString(id.getMachineName());
 			if (!resolvedMachines.contains(machineName)) {
 				resolvedMachines.add(machineName);
 				Start start = parsedMachines.get(machineName);