diff --git a/.gitignore b/.gitignore
index 8c3cba9c1459c3656353e57f12a4d641d90035a3..1bb8669b490ece744c69e3abda15c41c7c1f00d9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,3 +17,4 @@ temp
 out/
 src/test/**/*.tla
 src/test/**/*.cfg
+public_examples
diff --git a/.travis.yml b/.travis.yml
index abe843baddbc5952e76f80cf52d2386c1248bb8d..582d9d2b30f9f2ceaee4b60d01666356d5b3c067 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,6 +1,6 @@
 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
diff --git a/build.gradle b/build.gradle
index 8d3d6a0c7635266dbed77a2bb6682ac7cc392070..1c6c787dfdee407a5279c192ff513cae2748d8df 100644
--- a/build.gradle
+++ b/build.gradle
@@ -1,174 +1,192 @@
-apply plugin: 'java'
-apply plugin: 'eclipse'
-apply plugin: 'maven'
-apply plugin: 'jacoco'
-apply plugin: 'findbugs'
-
-project.version = '1.0.4-SNAPSHOT'
-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-SNAPSHOT'
+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 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/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);
 		}
 }