diff --git a/.editorconfig b/.editorconfig new file mode 100644 index 0000000000000000000000000000000000000000..0b58118283eb694753962956f681536c96b161c2 --- /dev/null +++ b/.editorconfig @@ -0,0 +1,8 @@ +root = true + +[*.{gradle,java}] +indent_style = tab + +[*.yml] +indent_style = space +indent_size = 2 diff --git a/build.gradle b/build.gradle index c4320913f8f77d549479ea4d3a13bd8636f4fccb..e084e2c4f6c9b7aa1b9abe9535aea79c7c0c5e67 100644 --- a/build.gradle +++ b/build.gradle @@ -1,10 +1,10 @@ plugins { - id 'java' - id 'eclipse' - id 'maven' - id 'jacoco' - id 'findbugs' - id "de.undercouch.download" version "3.4.3" + id 'java' + id 'eclipse' + id 'maven' + id 'jacoco' + id 'findbugs' + id "de.undercouch.download" version "3.4.3" } project.version = '1.0.5-SNAPSHOT' @@ -14,15 +14,15 @@ project.sourceCompatibility = '1.7' project.targetCompatibility = '1.7' repositories { - mavenCentral() - maven { - name "sonatype snapshots" - url "https://oss.sonatype.org/content/repositories/snapshots" - } + mavenCentral() + maven { + name "sonatype snapshots" + url "https://oss.sonatype.org/content/repositories/snapshots" + } } configurations.all { - resolutionStrategy.cacheChangingModulesFor 0, 'seconds' + resolutionStrategy.cacheChangingModulesFor 0, 'seconds' } def parser_version = '2.9.14' @@ -45,17 +45,17 @@ dependencies { } jacoco { - toolVersion = "0.7.1.201405082137" - reportsDir = file("$buildDir/JacocoReports") + toolVersion = "0.7.1.201405082137" + reportsDir = file("$buildDir/JacocoReports") } jacocoTestReport { - reports { - xml.enabled false - csv.enabled false - html.destination file("${buildDir}/jacocoHtml") - } + reports { + xml.enabled false + csv.enabled false + html.destination file("${buildDir}/jacocoHtml") + } } @@ -66,18 +66,18 @@ test { } task downloadPublicExamples(type: Download) { - src 'https://www3.hhu.de/stups/downloads/prob/source/ProB_public_examples.tgz' - dest buildDir - onlyIfModified true + 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 + from tarTree(resources.gzip("${buildDir}/ProB_public_examples.tgz")) + into projectDir } clean { - delete "${projectDir}/public_examples" + delete "${projectDir}/public_examples" } task regressionTests(dependsOn: extractPublicExamples, type: Test){ @@ -100,10 +100,10 @@ tasks.withType(FindBugs) { // 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 - } + reports { + xml.enabled = false + html.enabled = true + } ignoreFailures = true } @@ -120,74 +120,73 @@ task createJar(type: Jar, dependsOn: build){ if (project.hasProperty('ossrhUsername') && project.hasProperty('ossrhPassword')) { + apply plugin: 'signing' -apply plugin: 'signing' - -signing { - sign configurations.archives -} + signing { + sign configurations.archives + } -javadoc { - failOnError = false -} + javadoc { + failOnError = false + } -task javadocJar(type: Jar) { - classifier = 'javadoc' - from javadoc -} + task javadocJar(type: Jar) { + classifier = 'javadoc' + from javadoc + } -task sourcesJar(type: Jar) { - classifier = 'sources' - from sourceSets.main.allSource -} + task sourcesJar(type: Jar) { + classifier = 'sources' + from sourceSets.main.allSource + } -artifacts { - archives javadocJar, sourcesJar -} + 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' - } - } - } - } - } -} + 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/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index b333bf60f4e7cae85e70ccf69a0242440876d5bd..4efe0950a58f11c2258fa6e9eb2d28223117bc55 100644 --- a/src/main/java/de/tlc4b/TLC4B.java +++ b/src/main/java/de/tlc4b/TLC4B.java @@ -377,7 +377,7 @@ public class TLC4B { filename = filename.replace("\\", File.separator); filename = filename.replace("/", File.separator); if (!filename.toLowerCase().endsWith(".mch") && - !filename.toLowerCase().endsWith(".sys")) { + !filename.toLowerCase().endsWith(".sys")) { filename = filename + ".mch"; } diff --git a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java index 16f357e61cd404e3d99b62c8f08caea900cd03fb..3831adefc9894707cb2605d5c0d5a5e8aa45a5ce 100644 --- a/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java +++ b/src/main/java/de/tlc4b/analysis/transformation/DefinitionsEliminator.java @@ -82,9 +82,9 @@ public class DefinitionsEliminator extends DepthFirstAdapter { String name = ((AExpressionDefinitionDefinition) e).getName() .getText().toString(); if (name.startsWith("ASSERT_LTL") - || name.startsWith("scope_") + || name.startsWith("scope_") || name.startsWith("SET_PREF_") - || name.equals("VISB_JSON_FILE") + || name.equals("VISB_JSON_FILE") || name.startsWith("ANIMATION_FUNCTION") || name.startsWith("ANIMATION_IMG")) continue; @@ -103,8 +103,8 @@ public class DefinitionsEliminator extends DepthFirstAdapter { if (name.startsWith("ASSERT_LTL") || name.startsWith("scope_") || name.startsWith("SET_PREF_") - || name.equals("VISB_JSON_FILE") - || name.startsWith("ANIMATION_FUNCTION") + || name.equals("VISB_JSON_FILE") + || name.startsWith("ANIMATION_FUNCTION") || name.startsWith("ANIMATION_IMG") || StandardMadules .isKeywordInModuleExternalFunctions(name)) { diff --git a/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java b/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java index 235e4456042a51012adec5b317308b55ed26bb03..8e4ead8e8d8ce6ff24aafb03f723f86f6a9b72e2 100644 --- a/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java +++ b/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java @@ -182,7 +182,7 @@ public class LTLFormulaTest { String machine = "MACHINE test\n" + "OPERATIONS foo = skip; bar = skip; bazz = skip\n" + "END"; - String expected = "((ENABLED(foo) => \\neg(ENABLED(bar) \\/ ENABLED(bazz))) /\\ (ENABLED(bar) => \\neg(ENABLED(bazz))))"; + String expected = "((ENABLED(foo) => \\neg(ENABLED(bar) \\/ ENABLED(bazz))) /\\ (ENABLED(bar) => \\neg(ENABLED(bazz))))"; compareLTLFormula(expected, machine, "deterministic(foo,bar,bazz)"); } @@ -192,7 +192,7 @@ public class LTLFormulaTest { String machine = "MACHINE test\n" + "OPERATIONS foo = skip; bar = skip; bazz = skip\n" + "END"; - String expected = "(ENABLED(foo) => \\neg(ENABLED(bar) \\/ ENABLED(bazz)))"; + String expected = "(ENABLED(foo) => \\neg(ENABLED(bar) \\/ ENABLED(bazz)))"; compareLTLFormula(expected, machine, "deterministic(foo)"); } @@ -201,7 +201,7 @@ public class LTLFormulaTest { String machine = "MACHINE test\n" + "OPERATIONS foo = skip; bar = skip; bazz = skip\n" + "END"; - String expected = "\\neg(ENABLED(Next))"; + String expected = "\\neg(ENABLED(Next))"; compareLTLFormula(expected, machine, "deadlock"); } @@ -210,7 +210,7 @@ public class LTLFormulaTest { String machine = "MACHINE test\n" + "OPERATIONS foo(a) = SELECT a : 1..3 THEN skip END\n" + "END"; - String expected = "\\neg(ENABLED(Next))"; + String expected = "\\neg(ENABLED(Next))"; compareLTLFormula(expected, machine, "deadlock"); } diff --git a/src/test/java/de/tlc4b/util/PolySuite.java b/src/test/java/de/tlc4b/util/PolySuite.java index 0fb12b7fd1c60f8083dd5e0339b76adc1efdc621..81574f75af9ba9e307da6a57697169a5392e5fad 100644 --- a/src/test/java/de/tlc4b/util/PolySuite.java +++ b/src/test/java/de/tlc4b/util/PolySuite.java @@ -20,121 +20,121 @@ import org.junit.runners.model.TestClass; public class PolySuite extends Suite { - // ////////////////////////////// - // Public helper interfaces - - /** - * Annotation for a method which returns a {@link Configuration} - * to be injected into the test class constructor - */ - @Retention(RetentionPolicy.RUNTIME) - @Target(ElementType.METHOD) - public static @interface Config { - } - - public static interface Configuration { - int size(); - Object getTestValue(int index); - Object getExpectedValue(int index); - String getTestName(int index); - } - - // ////////////////////////////// - // Fields - - private final List<Runner> runners; - - // ////////////////////////////// - // Constructor - - /** - * Only called reflectively. Do not use programmatically. - * @param c the test class - * @throws Throwable if something bad happens - */ - public PolySuite(Class<?> c) throws Throwable { - super(c, Collections.<Runner>emptyList()); - TestClass testClass = getTestClass(); - Class<?> jTestClass = testClass.getJavaClass(); - Configuration configuration = getConfiguration(testClass); - List<Runner> runners = new ArrayList<Runner>(); - for (int i = 0, size = configuration.size(); i < size; i++) { - SingleRunner runner = new SingleRunner(jTestClass, configuration.getTestValue(i), configuration.getTestName(i), configuration.getExpectedValue(i)); - runners.add(runner); - } - this.runners = runners; - } - - // ////////////////////////////// - // Overrides - - @Override - protected List<Runner> getChildren() { - return runners; - } - - // ////////////////////////////// - // Private - - private Configuration getConfiguration(TestClass testClass) throws Throwable { - return (Configuration) getConfigMethod(testClass).invokeExplosively(null); - } - - private FrameworkMethod getConfigMethod(TestClass testClass) { - List<FrameworkMethod> methods = testClass.getAnnotatedMethods(Config.class); - if (methods.isEmpty()) { - throw new IllegalStateException("@" + Config.class.getSimpleName() + " method not found"); - } - if (methods.size() > 1) { - throw new IllegalStateException("Too many @" + Config.class.getSimpleName() + " methods"); - } - FrameworkMethod method = methods.get(0); - int modifiers = method.getMethod().getModifiers(); - if (!(Modifier.isStatic(modifiers) && Modifier.isPublic(modifiers))) { - throw new IllegalStateException("@" + Config.class.getSimpleName() + " method \"" + method.getName() + "\" must be public static"); - } - return method; - } - - // ////////////////////////////// - // Helper classes - - private static class SingleRunner extends BlockJUnit4ClassRunner { - - private final Object testVal; - private final Object expectedVal; - private final String testName; - - SingleRunner(Class<?> testClass, Object testVal, String testName, Object expectedVal) throws InitializationError { - super(testClass); - this.testVal = testVal; - this.expectedVal = expectedVal; - this.testName = testName; - } - - @Override - protected Object createTest() throws Exception { - return getTestClass().getOnlyConstructor().newInstance(testVal, expectedVal); - } - - @Override - protected String getName() { - return testName; - } - - @Override - protected String testName(FrameworkMethod method) { - return testName + ": " + method.getName(); - } - - @Override - protected void validateConstructor(List<Throwable> errors) { - validateOnlyOneConstructor(errors); - } - - @Override - protected Statement classBlock(RunNotifier notifier) { - return childrenInvoker(notifier); - } - } - } \ No newline at end of file + // ////////////////////////////// + // Public helper interfaces + + /** + * Annotation for a method which returns a {@link Configuration} + * to be injected into the test class constructor + */ + @Retention(RetentionPolicy.RUNTIME) + @Target(ElementType.METHOD) + public static @interface Config { + } + + public static interface Configuration { + int size(); + Object getTestValue(int index); + Object getExpectedValue(int index); + String getTestName(int index); + } + + // ////////////////////////////// + // Fields + + private final List<Runner> runners; + + // ////////////////////////////// + // Constructor + + /** + * Only called reflectively. Do not use programmatically. + * @param c the test class + * @throws Throwable if something bad happens + */ + public PolySuite(Class<?> c) throws Throwable { + super(c, Collections.<Runner>emptyList()); + TestClass testClass = getTestClass(); + Class<?> jTestClass = testClass.getJavaClass(); + Configuration configuration = getConfiguration(testClass); + List<Runner> runners = new ArrayList<Runner>(); + for (int i = 0, size = configuration.size(); i < size; i++) { + SingleRunner runner = new SingleRunner(jTestClass, configuration.getTestValue(i), configuration.getTestName(i), configuration.getExpectedValue(i)); + runners.add(runner); + } + this.runners = runners; + } + + // ////////////////////////////// + // Overrides + + @Override + protected List<Runner> getChildren() { + return runners; + } + + // ////////////////////////////// + // Private + + private Configuration getConfiguration(TestClass testClass) throws Throwable { + return (Configuration) getConfigMethod(testClass).invokeExplosively(null); + } + + private FrameworkMethod getConfigMethod(TestClass testClass) { + List<FrameworkMethod> methods = testClass.getAnnotatedMethods(Config.class); + if (methods.isEmpty()) { + throw new IllegalStateException("@" + Config.class.getSimpleName() + " method not found"); + } + if (methods.size() > 1) { + throw new IllegalStateException("Too many @" + Config.class.getSimpleName() + " methods"); + } + FrameworkMethod method = methods.get(0); + int modifiers = method.getMethod().getModifiers(); + if (!(Modifier.isStatic(modifiers) && Modifier.isPublic(modifiers))) { + throw new IllegalStateException("@" + Config.class.getSimpleName() + " method \"" + method.getName() + "\" must be public static"); + } + return method; + } + + // ////////////////////////////// + // Helper classes + + private static class SingleRunner extends BlockJUnit4ClassRunner { + + private final Object testVal; + private final Object expectedVal; + private final String testName; + + SingleRunner(Class<?> testClass, Object testVal, String testName, Object expectedVal) throws InitializationError { + super(testClass); + this.testVal = testVal; + this.expectedVal = expectedVal; + this.testName = testName; + } + + @Override + protected Object createTest() throws Exception { + return getTestClass().getOnlyConstructor().newInstance(testVal, expectedVal); + } + + @Override + protected String getName() { + return testName; + } + + @Override + protected String testName(FrameworkMethod method) { + return testName + ": " + method.getName(); + } + + @Override + protected void validateConstructor(List<Throwable> errors) { + validateOnlyOneConstructor(errors); + } + + @Override + protected Statement classBlock(RunNotifier notifier) { + return childrenInvoker(notifier); + } + } +} \ No newline at end of file