Merge branch 'develop'

Makefile

-.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 

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) {

gradle/wrapper/gradle-wrapper.properties

 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

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
 
@@ -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

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);
 	}
 

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);

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);