diff --git a/.gitignore b/.gitignore
index f3654b08020d6631b523fafd8d052529cbdb9689..1bb8669b490ece744c69e3abda15c41c7c1f00d9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -14,3 +14,7 @@ src/test/resources/testing
 src/test/resources/todo
 TLC4B.jar
 temp
+out/
+src/test/**/*.tla
+src/test/**/*.cfg
+public_examples
diff --git a/.travis.yml b/.travis.yml
index abe843baddbc5952e76f80cf52d2386c1248bb8d..5149dfc6f470e97b754b9d376b3a05d11d4adf74 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,6 +1,5 @@
 language: java
-sudo: true
-script: gradle build
+script: ./gradlew --no-daemon --console verbose --stacktrace build
 before_install:
 - openssl aes-256-cbc -pass pass:$ENCRYPTION_PASSWORD -in secring.gpg.enc -out secring.gpg
   -d
@@ -8,10 +7,7 @@ before_install:
   -d
 - openssl aes-256-cbc -pass pass:$ENCRYPTION_PASSWORD -in gradle.properties.enc -out
   gradle.properties -d
-after_success: "[ $TRAVIS_BRANCH = 'master' ] && gradle uploadArchives"
+after_success: "[ $TRAVIS_BRANCH = 'master' ] && ./gradlew --no-daemon uploadArchives"
 env:
   global:
   - secure: EnIo0zaQsHATGH8S5L1W0EHtqgV2kx6bfSgxyhz7XU+xw5y2JLDn+Y3ZaX7EcMK25RkgM8nld5Se72QmpienkP7tQlb5KHdwC10KgwbHDq+IP9q+ZMD2V1MsMRdTilW/eTZ0SUohlV5g4t3KqIe8l3Hs1dzNL0YmCMtXwYHdfwk=
-notifications:
-  slack:
-    secure: VWTQE6Z6o9Xz4gZ1SOUKroz5g+exD//+FUdd6wM0tLESFhqqrfwR1dyZHIbQJpcC8KROQD5Bip6vihhACBmr+NU6nPwoNN7fJ9Dvgqt4xG4NEk3+VpVCQVfRDJF4IhHqRFx4K+9fV5I2Kr93G39U/N92lMLk/RkyoaUyju85uwM=
diff --git a/build.gradle b/build.gradle
index d6daa92230e728a347a790fa50e8b62bb03992b7..6fa3de76be5ad3d3fb8c546676dcf9e2ee84c622 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,174 +1,193 @@
-apply plugin: 'java'
-apply plugin: 'eclipse'
-apply plugin: 'maven'
-apply plugin: 'jacoco'
-apply plugin: 'findbugs'
-
-project.version = '1.0.3'
-project.group = 'de.hhu.stups'
-
-project.sourceCompatibility = '1.7'
-project.targetCompatibility = '1.7'
-
-repositories {
-  mavenCentral()
-    maven {
-      name "sonatype snapshots"
-      url "https://oss.sonatype.org/content/repositories/snapshots"
-    }
-}
-
-configurations.all {
- resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
-}
-
-def parser_version = '2.9.12'
-def tlatools_version = '1.0.2'
-
-dependencies {
-	//compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
-	compile 'commons-cli:commons-cli:1.2'
-	compile (group: 'de.hhu.stups', name: 'tlatools', version: tlatools_version)
-
-	compile (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
-	compile (group: 'de.hhu.stups', name: 'parserbase', version: parser_version)
-	compile (group: 'de.hhu.stups', name: 'bparser', version: parser_version)
-	compile (group: 'de.hhu.stups', name: 'ltlparser', version: parser_version)
-
-	//compile(group: 'de.hhu.stups', name: 'de.prob.core.kernel', version: '2.0.0-milestone-13-SNAPSHOT')
-
-	testCompile (group: 'junit', name: 'junit', version: '4.12')
-	testCompile (group: 'de.hhu.stups', name: 'tla2bAST', version: '1.1.0')
-}
-
-jacoco {
-    toolVersion = "0.7.1.201405082137"
-    reportsDir = file("$buildDir/JacocoReports")
-}
-
-jacocoTestReport {
-    reports {
-        xml.enabled false
-        csv.enabled false
-        html.destination "${buildDir}/jacocoHtml"
-    }
-}
-
-
-test {
-	exclude('de/tlc4b/tlc/integration/probprivate')
-	exclude('testing')
-	//exclude('de/tlc4b/tlc/integration')
-}
-
-
-task regressionTests(type: Test){
-	doFirst{ println("Running integration tests") }
-	scanForTestClasses = true
-	//include('de/tlc4b/tlc/integration/probprivate/**')
-	include('de/tlc4b/**')
-}
-
-// type 'gradle integrationTests jacocoIntegrationTestReport' in order to run the jacoco code coverage analysis
-task jacocoIntegrationTestReport(type: JacocoReport) {
-	sourceSets sourceSets.main
-	//executionData files('build/jacoco/integrationTests.exec')
-	executionData fileTree(project.rootDir.absolutePath).include("**/build/jacoco/*.exec")
-}
-
-tasks.withType(FindBugs) {
-	// disable findbugs by default
-	// in order to run findbugs type 'gradle build findbugsMain findbugsTest'
-	task -> enabled = gradle.startParameter.taskNames.contains(task.name)
-
-    reports {
-        xml.enabled = false
-        html.enabled = true
-    }
-
-	ignoreFailures = true
-}
-
-task createJar(type: Jar, dependsOn: build){
-	archiveName = 'TLC4B.jar'
-	from sourceSets.main.output
-	from {configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
-	exclude('**/*.java')
-	manifest {
-		attributes "Main-Class" : 'de.tlc4b.TLC4B'
-	}
-}
-
-
-if (project.hasProperty('ossrhUsername') && project.hasProperty('ossrhPassword')) {
-
-apply plugin: 'signing'
-
-signing {
-    sign configurations.archives
-}
-
-javadoc {
-	failOnError = false
-}
-
-task javadocJar(type: Jar) {
-	 classifier = 'javadoc'
-	 from javadoc
-}
-
-task sourcesJar(type: Jar) {
-	 classifier = 'sources'
-	 from sourceSets.main.allSource
-}
-
-artifacts {
-	 archives javadocJar, sourcesJar
-}
-
-uploadArchives {
-  repositories {
-    mavenDeployer {
-      beforeDeployment { MavenDeployment deployment -> signing.signPom(deployment) }
-
-      repository(url: "https://oss.sonatype.org/service/local/staging/deploy/maven2/") {
-        authentication(userName: ossrhUsername, password: ossrhPassword)
-      }
-
-      snapshotRepository(url: "https://oss.sonatype.org/content/repositories/snapshots/") {
-        authentication(userName: ossrhUsername, password: ossrhPassword)
-      }
-
-      pom.project {
-        name 'TLC integration into ProB'
-        packaging 'jar'
-        // optionally artifactId can be defined here
-        description "Use the TLC model checker within ProB."
-        url 'https://github.com/hhu-stups/tlc4b'
-
-        licenses {
-          license {
-            name 'Eclipse Public License, Version 2.1'
-            url 'https://www.eclipse.org/legal/epl-v10.html'
-          }
-        }
-
-        scm {
-          connection 'scm:git:git://github.com/hhu-stups/tlc4b.git'
-          developerConnection 'scm:git:git@github.com:hhu-stups/tlc4b.git'
-          url 'https://github.com/bendisposto/hhu-stups/tlc4b'
-        }
-
-
-        developers {
-          developer {
-            id 'bendisposto'
-            name 'Jens Bendisposto'
-            email 'jens@bendisposto.de'
-          }
-        }
-      }
-    }
-  }
-}
-}
+plugins {
+    id 'java'
+    id 'eclipse'
+    id 'maven'
+    id 'jacoco'
+    id 'findbugs'
+    id "de.undercouch.download" version "3.4.3"
+}
+
+project.version = '1.0.4'
+project.group = 'de.hhu.stups'
+
+project.sourceCompatibility = '1.7'
+project.targetCompatibility = '1.7'
+
+repositories {
+  mavenCentral()
+    maven {
+      name "sonatype snapshots"
+      url "https://oss.sonatype.org/content/repositories/snapshots"
+    }
+}
+
+configurations.all {
+ resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
+}
+
+def parser_version = '2.9.12'
+def tlatools_version = '1.0.2'
+
+dependencies {
+	//compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
+	compile 'commons-cli:commons-cli:1.2'
+	compile (group: 'de.hhu.stups', name: 'tlatools', version: tlatools_version)
+
+	compile (group: 'de.hhu.stups', name: 'prologlib', version: parser_version)
+	compile (group: 'de.hhu.stups', name: 'parserbase', version: parser_version)
+	compile (group: 'de.hhu.stups', name: 'bparser', version: parser_version)
+	compile (group: 'de.hhu.stups', name: 'ltlparser', version: parser_version)
+
+	//compile(group: 'de.hhu.stups', name: 'de.prob.core.kernel', version: '2.0.0-milestone-13-SNAPSHOT')
+
+	testCompile (group: 'junit', name: 'junit', version: '4.12')
+	testCompile (group: 'de.hhu.stups', name: 'tla2bAST', version: '1.1.0')
+}
+
+jacoco {
+    toolVersion = "0.7.1.201405082137"
+    reportsDir = file("$buildDir/JacocoReports")
+}
+
+
+jacocoTestReport {
+    reports {
+        xml.enabled false
+        csv.enabled false
+        html.destination file("${buildDir}/jacocoHtml")
+    }
+}
+
+
+test {
+	exclude('de/tlc4b/tlc/integration/probprivate')
+	exclude('testing')
+	//exclude('de/tlc4b/tlc/integration')
+}
+
+task downloadPublicExamples(type: Download) {
+  src 'https://www3.hhu.de/stups/downloads/prob/source/ProB_public_examples.tgz'
+  dest buildDir
+  onlyIfModified true
+}
+
+task extractPublicExamples(dependsOn: downloadPublicExamples, type: Copy) {
+  from tarTree(resources.gzip("${buildDir}/ProB_public_examples.tgz"))
+  into projectDir
+}
+
+clean {
+  delete "${projectDir}/public_examples"
+}
+
+task regressionTests(dependsOn: extractPublicExamples, type: Test){
+	doFirst{ println("Running integration tests") }
+	scanForTestClasses = true
+	//include('de/tlc4b/tlc/integration/probprivate/**')
+	include('de/tlc4b/**')
+}
+check.dependsOn(regressionTests)
+
+// type 'gradle integrationTests jacocoIntegrationTestReport' in order to run the jacoco code coverage analysis
+task jacocoIntegrationTestReport(type: JacocoReport) {
+	sourceSets sourceSets.main
+	//executionData files('build/jacoco/integrationTests.exec')
+	executionData fileTree(project.rootDir.absolutePath).include("**/build/jacoco/*.exec")
+}
+
+tasks.withType(FindBugs) {
+	// disable findbugs by default
+	// in order to run findbugs type 'gradle build findbugsMain findbugsTest'
+	task -> enabled = gradle.startParameter.taskNames.contains(task.name)
+
+    reports {
+        xml.enabled = false
+        html.enabled = true
+    }
+
+	ignoreFailures = true
+}
+
+task createJar(type: Jar, dependsOn: build){
+	archiveName = 'TLC4B.jar'
+	from sourceSets.main.output
+	from {configurations.compile.collect { it.isDirectory() ? it : zipTree(it) } }
+	exclude('**/*.java')
+	manifest {
+		attributes "Main-Class" : 'de.tlc4b.TLC4B'
+	}
+}
+
+
+if (project.hasProperty('ossrhUsername') && project.hasProperty('ossrhPassword')) {
+
+apply plugin: 'signing'
+
+signing {
+    sign configurations.archives
+}
+
+javadoc {
+	failOnError = false
+}
+
+task javadocJar(type: Jar) {
+	 classifier = 'javadoc'
+	 from javadoc
+}
+
+task sourcesJar(type: Jar) {
+	 classifier = 'sources'
+	 from sourceSets.main.allSource
+}
+
+artifacts {
+	 archives javadocJar, sourcesJar
+}
+
+uploadArchives {
+  repositories {
+    mavenDeployer {
+      beforeDeployment { MavenDeployment deployment -> signing.signPom(deployment) }
+
+      repository(url: "https://oss.sonatype.org/service/local/staging/deploy/maven2/") {
+        authentication(userName: ossrhUsername, password: ossrhPassword)
+      }
+
+      snapshotRepository(url: "https://oss.sonatype.org/content/repositories/snapshots/") {
+        authentication(userName: ossrhUsername, password: ossrhPassword)
+      }
+
+      pom.project {
+        name 'TLC integration into ProB'
+        packaging 'jar'
+        // optionally artifactId can be defined here
+        description "Use the TLC model checker within ProB."
+        url 'https://github.com/hhu-stups/tlc4b'
+
+        licenses {
+          license {
+            name 'Eclipse Public License, Version 2.1'
+            url 'https://www.eclipse.org/legal/epl-v10.html'
+          }
+        }
+
+        scm {
+          connection 'scm:git:git://github.com/hhu-stups/tlc4b.git'
+          developerConnection 'scm:git:git@github.com:hhu-stups/tlc4b.git'
+          url 'https://github.com/bendisposto/hhu-stups/tlc4b'
+        }
+
+
+        developers {
+          developer {
+            id 'bendisposto'
+            name 'Jens Bendisposto'
+            email 'jens@bendisposto.de'
+          }
+        }
+      }
+    }
+  }
+}
+}
diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar
new file mode 100644
index 0000000000000000000000000000000000000000..29953ea141f55e3b8fc691d31b5ca8816d89fa87
Binary files /dev/null and b/gradle/wrapper/gradle-wrapper.jar differ
diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
new file mode 100644
index 0000000000000000000000000000000000000000..e0b3fb8d70b1bbf790f6f8ed1c928ddf09f54628
--- /dev/null
+++ b/gradle/wrapper/gradle-wrapper.properties
@@ -0,0 +1,5 @@
+distributionBase=GRADLE_USER_HOME
+distributionPath=wrapper/dists
+distributionUrl=https\://services.gradle.org/distributions/gradle-4.10.2-bin.zip
+zipStoreBase=GRADLE_USER_HOME
+zipStorePath=wrapper/dists
diff --git a/gradlew b/gradlew
new file mode 100755
index 0000000000000000000000000000000000000000..cccdd3d517fc5249beaefa600691cf150f2fa3e6
--- /dev/null
+++ b/gradlew
@@ -0,0 +1,172 @@
+#!/usr/bin/env sh
+
+##############################################################################
+##
+##  Gradle start up script for UN*X
+##
+##############################################################################
+
+# Attempt to set APP_HOME
+# Resolve links: $0 may be a link
+PRG="$0"
+# Need this for relative symlinks.
+while [ -h "$PRG" ] ; do
+    ls=`ls -ld "$PRG"`
+    link=`expr "$ls" : '.*-> \(.*\)$'`
+    if expr "$link" : '/.*' > /dev/null; then
+        PRG="$link"
+    else
+        PRG=`dirname "$PRG"`"/$link"
+    fi
+done
+SAVED="`pwd`"
+cd "`dirname \"$PRG\"`/" >/dev/null
+APP_HOME="`pwd -P`"
+cd "$SAVED" >/dev/null
+
+APP_NAME="Gradle"
+APP_BASE_NAME=`basename "$0"`
+
+# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
+DEFAULT_JVM_OPTS=""
+
+# Use the maximum available, or set MAX_FD != -1 to use that value.
+MAX_FD="maximum"
+
+warn () {
+    echo "$*"
+}
+
+die () {
+    echo
+    echo "$*"
+    echo
+    exit 1
+}
+
+# OS specific support (must be 'true' or 'false').
+cygwin=false
+msys=false
+darwin=false
+nonstop=false
+case "`uname`" in
+  CYGWIN* )
+    cygwin=true
+    ;;
+  Darwin* )
+    darwin=true
+    ;;
+  MINGW* )
+    msys=true
+    ;;
+  NONSTOP* )
+    nonstop=true
+    ;;
+esac
+
+CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar
+
+# Determine the Java command to use to start the JVM.
+if [ -n "$JAVA_HOME" ] ; then
+    if [ -x "$JAVA_HOME/jre/sh/java" ] ; then
+        # IBM's JDK on AIX uses strange locations for the executables
+        JAVACMD="$JAVA_HOME/jre/sh/java"
+    else
+        JAVACMD="$JAVA_HOME/bin/java"
+    fi
+    if [ ! -x "$JAVACMD" ] ; then
+        die "ERROR: JAVA_HOME is set to an invalid directory: $JAVA_HOME
+
+Please set the JAVA_HOME variable in your environment to match the
+location of your Java installation."
+    fi
+else
+    JAVACMD="java"
+    which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
+
+Please set the JAVA_HOME variable in your environment to match the
+location of your Java installation."
+fi
+
+# Increase the maximum file descriptors if we can.
+if [ "$cygwin" = "false" -a "$darwin" = "false" -a "$nonstop" = "false" ] ; then
+    MAX_FD_LIMIT=`ulimit -H -n`
+    if [ $? -eq 0 ] ; then
+        if [ "$MAX_FD" = "maximum" -o "$MAX_FD" = "max" ] ; then
+            MAX_FD="$MAX_FD_LIMIT"
+        fi
+        ulimit -n $MAX_FD
+        if [ $? -ne 0 ] ; then
+            warn "Could not set maximum file descriptor limit: $MAX_FD"
+        fi
+    else
+        warn "Could not query maximum file descriptor limit: $MAX_FD_LIMIT"
+    fi
+fi
+
+# For Darwin, add options to specify how the application appears in the dock
+if $darwin; then
+    GRADLE_OPTS="$GRADLE_OPTS \"-Xdock:name=$APP_NAME\" \"-Xdock:icon=$APP_HOME/media/gradle.icns\""
+fi
+
+# For Cygwin, switch paths to Windows format before running java
+if $cygwin ; then
+    APP_HOME=`cygpath --path --mixed "$APP_HOME"`
+    CLASSPATH=`cygpath --path --mixed "$CLASSPATH"`
+    JAVACMD=`cygpath --unix "$JAVACMD"`
+
+    # We build the pattern for arguments to be converted via cygpath
+    ROOTDIRSRAW=`find -L / -maxdepth 1 -mindepth 1 -type d 2>/dev/null`
+    SEP=""
+    for dir in $ROOTDIRSRAW ; do
+        ROOTDIRS="$ROOTDIRS$SEP$dir"
+        SEP="|"
+    done
+    OURCYGPATTERN="(^($ROOTDIRS))"
+    # Add a user-defined pattern to the cygpath arguments
+    if [ "$GRADLE_CYGPATTERN" != "" ] ; then
+        OURCYGPATTERN="$OURCYGPATTERN|($GRADLE_CYGPATTERN)"
+    fi
+    # Now convert the arguments - kludge to limit ourselves to /bin/sh
+    i=0
+    for arg in "$@" ; do
+        CHECK=`echo "$arg"|egrep -c "$OURCYGPATTERN" -`
+        CHECK2=`echo "$arg"|egrep -c "^-"`                                 ### Determine if an option
+
+        if [ $CHECK -ne 0 ] && [ $CHECK2 -eq 0 ] ; then                    ### Added a condition
+            eval `echo args$i`=`cygpath --path --ignore --mixed "$arg"`
+        else
+            eval `echo args$i`="\"$arg\""
+        fi
+        i=$((i+1))
+    done
+    case $i in
+        (0) set -- ;;
+        (1) set -- "$args0" ;;
+        (2) set -- "$args0" "$args1" ;;
+        (3) set -- "$args0" "$args1" "$args2" ;;
+        (4) set -- "$args0" "$args1" "$args2" "$args3" ;;
+        (5) set -- "$args0" "$args1" "$args2" "$args3" "$args4" ;;
+        (6) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" ;;
+        (7) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" ;;
+        (8) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" "$args7" ;;
+        (9) set -- "$args0" "$args1" "$args2" "$args3" "$args4" "$args5" "$args6" "$args7" "$args8" ;;
+    esac
+fi
+
+# Escape application args
+save () {
+    for i do printf %s\\n "$i" | sed "s/'/'\\\\''/g;1s/^/'/;\$s/\$/' \\\\/" ; done
+    echo " "
+}
+APP_ARGS=$(save "$@")
+
+# Collect all arguments for the java command, following the shell quoting and substitution rules
+eval set -- $DEFAULT_JVM_OPTS $JAVA_OPTS $GRADLE_OPTS "\"-Dorg.gradle.appname=$APP_BASE_NAME\"" -classpath "\"$CLASSPATH\"" org.gradle.wrapper.GradleWrapperMain "$APP_ARGS"
+
+# by default we should be in the correct project dir, but when run from Finder on Mac, the cwd is wrong
+if [ "$(uname)" = "Darwin" ] && [ "$HOME" = "$PWD" ]; then
+  cd "$(dirname "$0")"
+fi
+
+exec "$JAVACMD" "$@"
diff --git a/gradlew.bat b/gradlew.bat
new file mode 100644
index 0000000000000000000000000000000000000000..f9553162f122c71b34635112e717c3e733b5b212
--- /dev/null
+++ b/gradlew.bat
@@ -0,0 +1,84 @@
+@if "%DEBUG%" == "" @echo off
+@rem ##########################################################################
+@rem
+@rem  Gradle startup script for Windows
+@rem
+@rem ##########################################################################
+
+@rem Set local scope for the variables with windows NT shell
+if "%OS%"=="Windows_NT" setlocal
+
+set DIRNAME=%~dp0
+if "%DIRNAME%" == "" set DIRNAME=.
+set APP_BASE_NAME=%~n0
+set APP_HOME=%DIRNAME%
+
+@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
+set DEFAULT_JVM_OPTS=
+
+@rem Find java.exe
+if defined JAVA_HOME goto findJavaFromJavaHome
+
+set JAVA_EXE=java.exe
+%JAVA_EXE% -version >NUL 2>&1
+if "%ERRORLEVEL%" == "0" goto init
+
+echo.
+echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
+echo.
+echo Please set the JAVA_HOME variable in your environment to match the
+echo location of your Java installation.
+
+goto fail
+
+:findJavaFromJavaHome
+set JAVA_HOME=%JAVA_HOME:"=%
+set JAVA_EXE=%JAVA_HOME%/bin/java.exe
+
+if exist "%JAVA_EXE%" goto init
+
+echo.
+echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME%
+echo.
+echo Please set the JAVA_HOME variable in your environment to match the
+echo location of your Java installation.
+
+goto fail
+
+:init
+@rem Get command-line arguments, handling Windows variants
+
+if not "%OS%" == "Windows_NT" goto win9xME_args
+
+:win9xME_args
+@rem Slurp the command line arguments.
+set CMD_LINE_ARGS=
+set _SKIP=2
+
+:win9xME_args_slurp
+if "x%~1" == "x" goto execute
+
+set CMD_LINE_ARGS=%*
+
+:execute
+@rem Setup the command line
+
+set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar
+
+@rem Execute Gradle
+"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %CMD_LINE_ARGS%
+
+:end
+@rem End local scope for the variables with windows NT shell
+if "%ERRORLEVEL%"=="0" goto mainEnd
+
+:fail
+rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of
+rem the _cmd.exe /c_ return code!
+if  not "" == "%GRADLE_EXIT_CONSOLE%" exit 1
+exit /b 1
+
+:mainEnd
+if "%OS%"=="Windows_NT" endlocal
+
+:omega
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index dcd72ea77eb42cecedfbc8acd40e9e8f58a0850a..970b42bf0774f7ee922fdc11d3b1b18bdf6d73ae 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -376,7 +376,7 @@ public class TLC4B {
 		// the following lines fix incorrect file names
 		filename = filename.replace("\\", File.separator);
 		filename = filename.replace("/", File.separator);
-		if (!filename.toLowerCase().endsWith(".mch") ||
+		if (!filename.toLowerCase().endsWith(".mch") &&
 		    !filename.toLowerCase().endsWith(".sys")) {
 			filename = filename + ".mch";
 		}
diff --git a/src/test/java/de/tlc4b/coverage/CoverageTest.java b/src/test/java/de/tlc4b/coverage/CoverageTest.java
index a106b1f20a8fee813f5516f57ea6df335af43583..f5d7ca539988f540f5d0d07506970b49e8767ce2 100644
--- a/src/test/java/de/tlc4b/coverage/CoverageTest.java
+++ b/src/test/java/de/tlc4b/coverage/CoverageTest.java
@@ -32,7 +32,7 @@ public class CoverageTest extends AbstractParseMachineTest {
 	public static Configuration getConfig() {
 		final ArrayList<String> list = new ArrayList<String>();
 		final ArrayList<String> ignoreList = new ArrayList<String>();
-		list.add("../prob_examples/public_examples/TLC/");
+		list.add("public_examples/TLC/");
 
 		list.add("./src/test/resources/");
 		ignoreList.add("./src/test/resources/compound/");
diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java
index c694d80486f966e6981d34612e7ad6f44599968b..03b294910763772b6bdc0b6d1669d7896f9daea5 100644
--- a/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java
@@ -37,7 +37,7 @@ public class AssertionErrorTest extends AbstractParseMachineTest {
 	@Config
 	public static Configuration getConfig() {
 		final ArrayList<TestPair> list = new ArrayList<TestPair>();
-		list.add(new TestPair(AssertionError, "../prob_examples/public_examples/TLC/AssertionError"));
+		list.add(new TestPair(AssertionError, "public_examples/TLC/AssertionError"));
 		return getConfiguration(list);
 	}
 }
diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java
index f49ff366ed77e548ec52d27f4b23d9f0179a49f0..bce24e39ce418ee58b83947c263ce5e8b1c71507 100644
--- a/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/DeadlockTest.java
@@ -38,7 +38,7 @@ public class DeadlockTest extends AbstractParseMachineTest {
 	public static Configuration getConfig() {
 		final ArrayList<TestPair> list = new ArrayList<TestPair>();
 		list.add(new TestPair(Deadlock,
-				"../prob_examples/public_examples/TLC/Deadlock"));
+				"public_examples/TLC/Deadlock"));
 		return getConfiguration(list);
 	}
 }
diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java
index d41789215c177421896b2d71a05c19bbfaacee43..8692465f62a6bc765abd6cf140749a2f905c9779 100644
--- a/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/GoalTest.java
@@ -38,7 +38,7 @@ public class GoalTest extends AbstractParseMachineTest {
 	public static Configuration getConfig() {
 		final ArrayList<TestPair> list = new ArrayList<TestPair>();
 		list.add(new TestPair(Goal,
-				"../prob_examples/public_examples/TLC/GOAL"));
+				"public_examples/TLC/GOAL"));
 		return getConfiguration(list);
 	}
 }
diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java
index 8499fdb947012c36ec7f55f4b02bc7f4322891a1..32b3aca18b90989cff6cc387419d0c6231f5d78a 100644
--- a/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/InvariantViolationTest.java
@@ -38,7 +38,7 @@ public class InvariantViolationTest extends AbstractParseMachineTest {
 	public static Configuration getConfig() {
 		final ArrayList<TestPair> list = new ArrayList<TestPair>();
 		list.add(new TestPair(InvariantViolation,
-				"../prob_examples/public_examples/TLC/InvariantViolation"));
+				"public_examples/TLC/InvariantViolation"));
 		return getConfiguration(list);
 	}
 }
diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java
index b0e5e3f81514e13038ca5a804379d8eae7d1988c..0a48252e85825bf62a0e9edd82de3c6e28441785 100644
--- a/src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java
@@ -17,70 +17,70 @@ public class LawsTest {
 	@Test
 	public void BoolLaws() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolLaws.mch"};
+		String[] a = new String[] { "public_examples/TLC/Laws/BoolLaws.mch"};
 		assertEquals(NoError, test(a));
 	}
 	
 	@Test
 	public void BoolWithArithLaws() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolWithArithLaws.mch", "-nodead"};
+		String[] a = new String[] { "public_examples/TLC/Laws/BoolWithArithLaws.mch", "-nodead"};
 		assertEquals(NoError, test(a));
 	}
 	
 	@Test
 	public void FunLaws() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/FunLaws.mch"};
+		String[] a = new String[] { "public_examples/TLC/Laws/FunLaws.mch"};
 		assertEquals(NoError, test(a));
 	}
 	
 	@Test
 	public void FunLawsWithLambda() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/FunLawsWithLambda.mch"};
+		String[] a = new String[] { "public_examples/TLC/Laws/FunLawsWithLambda.mch"};
 		assertEquals(NoError, test(a));
 	}
 	
 	@Test
 	public void RelLaws_TLC() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/RelLaws_TLC.mch"};
+		String[] a = new String[] { "public_examples/TLC/Laws/RelLaws_TLC.mch"};
 		assertEquals(Goal, test(a));
 	}
 	
 	@Test
 	public void BoolLaws_SetCompr() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolLaws_SetCompr.mch"};
+		String[] a = new String[] { "public_examples/TLC/Laws/BoolLaws_SetCompr.mch"};
 		assertEquals(NoError, test(a));
 	}
 	
 	@Test
 	public void BoolLaws_SetComprCLPFD() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/BoolLaws_SetComprCLPFD.mch"};
+		String[] a = new String[] { "public_examples/TLC/Laws/BoolLaws_SetComprCLPFD.mch"};
 		assertEquals(NoError, test(a));
 	}
 
 	@Test
 	public void CardinalityLaws_TLC() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/CardinalityLaws_TLC.mch", "-nodead"};
+		String[] a = new String[] { "public_examples/TLC/Laws/CardinalityLaws_TLC.mch", "-nodead"};
 		assertEquals(NoError, test(a));
 	}
 	
 	@Test
 	public void EqualityLaws() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/EqualityLaws.mch", "-nodead"};
+		String[] a = new String[] { "public_examples/TLC/Laws/EqualityLaws.mch", "-nodead"};
 		assertEquals(NoError, test(a));
 	}
 	
 	@Test
 	public void SubsetLaws() throws Exception {
 		TLC4BGlobals.setDeleteOnExit(true);
-		String[] a = new String[] { "../prob_examples/public_examples/TLC/Laws/SubsetLaws.mch", "-nodead"};
+		String[] a = new String[] { "public_examples/TLC/Laws/SubsetLaws.mch", "-nodead"};
 		assertEquals(NoError, test(a));
 	}
 }
diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java
index 9983401381a4f237e476c1efd1c550ba0f3a1846..8605ab1f7c6196d2dd345385d36bb1d24f6b9c84 100644
--- a/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/NoErrorTest.java
@@ -38,7 +38,7 @@ public class NoErrorTest extends AbstractParseMachineTest {
 	public static Configuration getConfig() {
 		final ArrayList<TestPair> list = new ArrayList<TestPair>();
 		list.add(new TestPair(NoError,
-				"../prob_examples/public_examples/TLC/NoError"));
+				"public_examples/TLC/NoError"));
 		return getConfiguration(list);
 	}
 
diff --git a/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java b/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java
index e258315a6c9dd4fbd0796008cd6b30cf986a0320..f92a4e25538e6a9295ea9f1dede517f93846b66f 100644
--- a/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java
@@ -37,7 +37,7 @@ public class WellDefinednessTest extends AbstractParseMachineTest  {
 		@Config
 		public static Configuration getConfig() {
 			final ArrayList<TestPair> list = new ArrayList<TestPair>();
-			list.add(new TestPair(WellDefinednessError, "../prob_examples/public_examples/TLC/WellDefinednessError"));
+			list.add(new TestPair(WellDefinednessError, "public_examples/TLC/WellDefinednessError"));
 			return getConfiguration(list);
 		}
 }