diff --git a/build.gradle b/build.gradle index f7a1171ab97c31512fcd4f76edea1bae5e9f6404..d975517f7d084ca0114b724766343f7eeaca8b97 100644 --- a/build.gradle +++ b/build.gradle @@ -94,11 +94,11 @@ task downloadPublicExamples(type: Download) { task extractPublicExamples(dependsOn: downloadPublicExamples, type: Copy) { from tarTree(resources.gzip("${buildDir}/ProB_public_examples.tgz")) - into projectDir + into "${buildDir}/prob_examples" } clean { - delete "${projectDir}/public_examples" + delete "${projectDir}/public_examples" // now extracted into build, but previous versions placed it at top level delete "${projectDir}/states" delete "${projectDir}/temp" } diff --git a/src/test/java/de/tlc4b/coverage/CoverageTest.java b/src/test/java/de/tlc4b/coverage/CoverageTest.java index 11f0ab23eb5318201c2d764c87c28944e35d6c8c..f057576dac3754f634b3aceccd58048d8fd0eac5 100644 --- a/src/test/java/de/tlc4b/coverage/CoverageTest.java +++ b/src/test/java/de/tlc4b/coverage/CoverageTest.java @@ -40,7 +40,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("public_examples/TLC/"); + list.add("build/prob_examples/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 03b294910763772b6bdc0b6d1669d7896f9daea5..4f405b4476a061e80438526416d6fb3b563b706d 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/AssertionErrorTest.java @@ -1,21 +1,21 @@ package de.tlc4b.tlc.integration.probprivate; -import static de.tlc4b.tlc.TLCResults.TLCResult.*; -import static de.tlc4b.util.TestUtil.test; -import static org.junit.Assert.assertEquals; - import java.io.File; import java.util.ArrayList; -import org.junit.Test; -import org.junit.runner.RunWith; - import de.tlc4b.tlc.TLCResults.TLCResult; import de.tlc4b.util.AbstractParseMachineTest; import de.tlc4b.util.PolySuite; -import de.tlc4b.util.TestPair; import de.tlc4b.util.PolySuite.Config; import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestPair; + +import org.junit.Test; +import org.junit.runner.RunWith; + +import static de.tlc4b.tlc.TLCResults.TLCResult.AssertionError; +import static de.tlc4b.util.TestUtil.test; +import static org.junit.Assert.assertEquals; @RunWith(PolySuite.class) public class AssertionErrorTest extends AbstractParseMachineTest { @@ -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, "public_examples/TLC/AssertionError")); + list.add(new TestPair(AssertionError, "build/prob_examples/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 bce24e39ce418ee58b83947c263ce5e8b1c71507..6d01d2a02ec6dab732efdce7bb7e081fba9d8698 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, - "public_examples/TLC/Deadlock")); + "build/prob_examples/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 8692465f62a6bc765abd6cf140749a2f905c9779..d026d9c9ecb8eb25c3353b71b6664562ab953265 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, - "public_examples/TLC/GOAL")); + "build/prob_examples/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 32b3aca18b90989cff6cc387419d0c6231f5d78a..c395f3908b0deebacfc50b1591c7a383f53b7b04 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, - "public_examples/TLC/InvariantViolation")); + "build/prob_examples/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 a837ff79cd2c67d8313f4dd66bd96f4e3b8890f5..fc8eb3208005a666981a864cd51e4e8280807a52 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/LawsTest.java @@ -1,86 +1,83 @@ package de.tlc4b.tlc.integration.probprivate; -import static de.tlc4b.tlc.TLCResults.TLCResult.*; -import static de.tlc4b.util.TestUtil.test; -import static org.junit.Assert.assertEquals; - - - - +import de.tlc4b.TLC4BGlobals; import org.junit.Test; -import de.tlc4b.TLC4BGlobals; +import static de.tlc4b.tlc.TLCResults.TLCResult.Goal; +import static de.tlc4b.tlc.TLCResults.TLCResult.NoError; +import static de.tlc4b.util.TestUtil.test; +import static org.junit.Assert.assertEquals; public class LawsTest { @Test public void BoolLaws() throws Exception { TLC4BGlobals.setDeleteOnExit(true); - String[] a = new String[] { "public_examples/TLC/Laws/BoolLaws.mch"}; + String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/BoolLaws.mch"}; assertEquals(NoError, test(a)); } @Test public void BoolWithArithLaws() throws Exception { TLC4BGlobals.setDeleteOnExit(true); - String[] a = new String[] { "public_examples/TLC/Laws/BoolWithArithLaws.mch", "-nodead"}; + String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/BoolWithArithLaws.mch", "-nodead"}; assertEquals(NoError, test(a)); } @Test public void FunLaws() throws Exception { TLC4BGlobals.setDeleteOnExit(true); - String[] a = new String[] { "public_examples/TLC/Laws/FunLaws.mch"}; + String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/FunLaws.mch"}; assertEquals(NoError, test(a)); } @Test public void FunLawsWithLambda() throws Exception { TLC4BGlobals.setDeleteOnExit(true); - String[] a = new String[] { "public_examples/TLC/Laws/FunLawsWithLambda.mch"}; + String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/FunLawsWithLambda.mch"}; assertEquals(NoError, test(a)); } @Test public void RelLaws_TLC() throws Exception { TLC4BGlobals.setDeleteOnExit(true); - String[] a = new String[] { "public_examples/TLC/Laws/RelLaws_TLC.mch"}; + String[] a = new String[] { "build/prob_examples/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[] { "public_examples/TLC/Laws/BoolLaws_SetCompr.mch"}; + String[] a = new String[] { "build/prob_examples/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[] { "public_examples/TLC/Laws/BoolLaws_SetComprCLPFD.mch"}; + String[] a = new String[] { "build/prob_examples/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[] { "public_examples/TLC/Laws/CardinalityLaws_TLC.mch", "-nodead"}; + String[] a = new String[] { "build/prob_examples/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[] { "public_examples/TLC/Laws/EqualityLaws.mch", "-nodead"}; + String[] a = new String[] { "build/prob_examples/public_examples/TLC/Laws/EqualityLaws.mch", "-nodead"}; assertEquals(NoError, test(a)); } @Test public void SubsetLaws() throws Exception { TLC4BGlobals.setDeleteOnExit(true); - String[] a = new String[] { "public_examples/TLC/Laws/SubsetLaws.mch", "-nodead"}; + String[] a = new String[] { "build/prob_examples/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 8605ab1f7c6196d2dd345385d36bb1d24f6b9c84..e5c0fe4d6c31cd8fe9f8b68deb26340bfcfa6615 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, - "public_examples/TLC/NoError")); + "build/prob_examples/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 f92a4e25538e6a9295ea9f1dede517f93846b66f..2004cd1f1d4e88bf6a9a2d450cd0f771b868db01 100644 --- a/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java +++ b/src/test/java/de/tlc4b/tlc/integration/probprivate/WellDefinednessTest.java @@ -1,21 +1,21 @@ package de.tlc4b.tlc.integration.probprivate; -import static de.tlc4b.tlc.TLCResults.TLCResult.*; -import static de.tlc4b.util.TestUtil.test; -import static org.junit.Assert.assertEquals; - import java.io.File; import java.util.ArrayList; -import org.junit.Test; -import org.junit.runner.RunWith; - import de.tlc4b.tlc.TLCResults.TLCResult; import de.tlc4b.util.AbstractParseMachineTest; import de.tlc4b.util.PolySuite; -import de.tlc4b.util.TestPair; import de.tlc4b.util.PolySuite.Config; import de.tlc4b.util.PolySuite.Configuration; +import de.tlc4b.util.TestPair; + +import org.junit.Test; +import org.junit.runner.RunWith; + +import static de.tlc4b.tlc.TLCResults.TLCResult.WellDefinednessError; +import static de.tlc4b.util.TestUtil.test; +import static org.junit.Assert.assertEquals; @RunWith(PolySuite.class) public class WellDefinednessTest extends AbstractParseMachineTest { @@ -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, "public_examples/TLC/WellDefinednessError")); + list.add(new TestPair(WellDefinednessError, "build/prob_examples/public_examples/TLC/WellDefinednessError")); return getConfiguration(list); } }