From b450e1a5925e17abbac700389b3bff87d88d7df1 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 17 Jul 2015 16:21:07 +0200
Subject: [PATCH] Refactoring
---
build.gradle | 19 +++++---
src/main/java/de/tlc4b/TLC4B.java | 9 ++--
src/main/java/de/tlc4b/TLCRunner.java | 4 ++
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 2 -
src/main/java/de/tlc4b/tlc/TLCOutputInfo.java | 2 -
src/main/java/de/tlc4b/tlc/TLCResults.java | 14 ++----
...tlFormulaTest.java => LTLFormulaTest.java} | 2 +-
.../de/tlc4b/prettyprint/NumbersTest.java | 2 -
.../de/tlc4b/tlc/integration/LTLTest.java | 10 +++-
src/test/java/de/tlc4b/util/TestUtil.java | 2 +-
src/test/java/testing/CompoundScopeTest.java | 47 +++++++++----------
src/test/java/testing/CompoundTest.java | 1 -
src/test/resources/ltl/CounterError.mch | 4 +-
.../resources/ltl/StatePropertyViolation.mch | 15 ++++++
14 files changed, 74 insertions(+), 59 deletions(-)
rename src/test/java/de/tlc4b/ltl/{LtlFormulaTest.java => LTLFormulaTest.java} (99%)
create mode 100644 src/test/resources/ltl/StatePropertyViolation.mch
diff --git a/build.gradle b/build.gradle
index 7639ef0..b1d5964 100644
--- a/build.gradle
+++ b/build.gradle
@@ -6,7 +6,7 @@ apply plugin: 'jacoco'
project.version = '1.0.0-SNAPSHOT'
project.group = 'de.prob'
-sourceCompatibility = 1.5
+//sourceCompatibility = 1.5
repositories {
mavenCentral()
@@ -38,7 +38,7 @@ dependencies {
- testCompile (group: 'junit', name: 'junit', version: '4.7')
+ testCompile (group: 'junit', name: 'junit', version: '4.11')
testCompile (group: 'de.prob', name: 'tla2bAST', version: '1.0.5-SNAPSHOT')
releaseJars (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT')
@@ -49,8 +49,8 @@ dependencies {
}
jacoco {
- toolVersion = "0.6.2.201302030002"
- reportsDir = file("$buildDir/customJacocoReportDir")
+ toolVersion = "0.7.1.201405082137"
+ reportsDir = file("$buildDir/JacocoReports")
}
jacocoTestReport {
@@ -69,13 +69,20 @@ test {
}
-task integrationtests(type: Test){
+task integrationTests(type: Test){
doFirst{ println("Running integration tests") }
scanForTestClasses = true
//include('de/tlc4b/tlc/integration/probprivate/**')
- include('de/tlc4b/**')
+ 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")
+ }
+
jar { from sourceSets.main.allJava }
jar {
from configurations.releaseJars.collect { it.isDirectory() ? it : zipTree(it) }
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 30a634d..820977c 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -10,11 +10,8 @@ import java.io.InputStream;
import java.io.OutputStreamWriter;
import java.io.UnsupportedEncodingException;
import java.util.LinkedHashMap;
-import java.util.Map;
-import java.util.Set;
import java.util.Map.Entry;
-import tlc2.TLCGlobals;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.UsedStandardModules.STANDARD_MODULES;
@@ -45,7 +42,7 @@ public class TLC4B {
// windows
TLC4B tlc4b = new TLC4B();
try {
- tlc4b.progress(args);
+ tlc4b.process(args);
} catch (BException e) {
System.err.println("***** Parsing Error *****");
System.err.println(e.getMessage());
@@ -159,7 +156,7 @@ public class TLC4B {
// B2TLAGlobals.setCleanup(true);
TLC4B tlc4b = new TLC4B();
try {
- tlc4b.progress(args);
+ tlc4b.process(args);
} catch (Exception e) {
e.printStackTrace();
System.err.println(e.getMessage());
@@ -272,7 +269,7 @@ public class TLC4B {
}
}
- public void progress(String[] args) throws IOException, BException {
+ public void process(String[] args) throws IOException, BException {
handleParameter(args);
System.out.print("Arguments: ");
diff --git a/src/main/java/de/tlc4b/TLCRunner.java b/src/main/java/de/tlc4b/TLCRunner.java
index 611bd49..48aec1e 100644
--- a/src/main/java/de/tlc4b/TLCRunner.java
+++ b/src/main/java/de/tlc4b/TLCRunner.java
@@ -109,6 +109,10 @@ public class TLCRunner {
list.add("-coverage");
list.add("" + 60);
}
+
+ list.add("-maxSetSize");
+ list.add("100000000");
+
// list.add("-config");
// list.add(machineName + ".cfg");
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index ecfda97..acf0f04 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -7,11 +7,9 @@ import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
-import tlc2.TLCGlobals;
import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.*;
-import de.tlc4b.TLC4B;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.analysis.MachineContext;
import de.tlc4b.analysis.PrecedenceCollector;
diff --git a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
index ef0c9e7..318f463 100644
--- a/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
+++ b/src/main/java/de/tlc4b/tlc/TLCOutputInfo.java
@@ -12,8 +12,6 @@ import de.tlc4b.analysis.Typechecker;
import de.tlc4b.btypes.BType;
import de.tlc4b.tla.ConfigFile;
import de.tlc4b.tla.TLAModule;
-import de.tlc4b.tla.config.ConfigFileAssignment;
-import de.tlc4b.tla.config.ModelValueAssignment;
public class TLCOutputInfo {
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index cfc8ad3..cdabda9 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -233,14 +233,6 @@ public class TLCResults implements ToolGlobals {
}
private void evalErrorMessage(Message m) {
- // System.out.println(------------------);
- // System.out.print(m.getMessageCode() + " " +
- // m.getParameters().length);
- // for (int i = 0; i < m.getParameters().length; i++) {
- // System.out.print(" " + m.getParameters()[i]);
- // }
- // System.out.println();
-
switch (m.getMessageCode()) {
case EC.TLC_INVARIANT_VIOLATED_INITIAL:
case EC.TLC_INVARIANT_VIOLATED_BEHAVIOR:
@@ -306,6 +298,8 @@ public class TLCResults implements ToolGlobals {
}
private TLCResult evaluatingParameter(String[] params) {
+ System.out.println(params.length);
+ System.out.println(params[0]);
for (int i = 0; i < params.length; i++) {
String s = params[i];
if (s.contains("not enumerable")) {
@@ -319,11 +313,13 @@ public class TLCResults implements ToolGlobals {
} else if (s.contains("which is not in the domain of the function")) {
return WellDefinednessError;
} else if (s.contains("tlc2.module.TLC.Assert")) {
- return tlcResult = WellDefinednessError;
+ return WellDefinednessError;
} else if (s
.contains("CHOOSE x \\in S: P, but no element of S satisfied P")
&& s.contains("module FunctionsAsRelations")) {
return tlcResult = WellDefinednessError;
+ } else if (s.contains("The property of ASSERT_LTL")) {
+ return TemporalPropertyViolation;
}
}
diff --git a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java b/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java
similarity index 99%
rename from src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
rename to src/test/java/de/tlc4b/ltl/LTLFormulaTest.java
index 574e89b..235e445 100644
--- a/src/test/java/de/tlc4b/ltl/LtlFormulaTest.java
+++ b/src/test/java/de/tlc4b/ltl/LTLFormulaTest.java
@@ -14,7 +14,7 @@ import de.tlc4b.exceptions.ScopeException;
import de.tlc4b.exceptions.TypeErrorException;
-public class LtlFormulaTest {
+public class LTLFormulaTest {
@BeforeClass
public static void setUp(){
diff --git a/src/test/java/de/tlc4b/prettyprint/NumbersTest.java b/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
index 69b6292..11f5d92 100644
--- a/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/NumbersTest.java
@@ -4,8 +4,6 @@ import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
-import de.tlc4b.TLC4BGlobals;
-
public class NumbersTest {
diff --git a/src/test/java/de/tlc4b/tlc/integration/LTLTest.java b/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
index a17f149..8cbe47c 100644
--- a/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
@@ -1,5 +1,7 @@
package de.tlc4b.tlc.integration;
-
+/**
+ * If the result is not correctly detected in the TLC output, @see de.tlc4b.tlc.TLCResult .
+ * */
import static org.junit.Assert.assertEquals;
import org.junit.BeforeClass;
@@ -51,5 +53,11 @@ public class LTLTest {
String[] a = new String[] { ".\\src\\test\\resources\\ltl\\Fairness_Parameter.mch" };
assertEquals(NoError, test(a));
}
+
+ @Test
+ public void testLTLStatePropertyViolation() throws Exception{
+ String[] a = new String[] { ".\\src\\test\\resources\\ltl\\StatePropertyViolation.mch" };
+ assertEquals(TemporalPropertyViolation, test(a));
+ }
}
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 7986ad8..12a628e 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -208,7 +208,7 @@ public class TestUtil {
// B2TLAGlobals.setCleanup(true);
TLC4B tlc4b = new TLC4B();
try {
- tlc4b.progress(args);
+ tlc4b.process(args);
} catch (Exception e) {
e.printStackTrace();
System.err.println(e.getMessage());
diff --git a/src/test/java/testing/CompoundScopeTest.java b/src/test/java/testing/CompoundScopeTest.java
index efdb18b..89bf8f0 100644
--- a/src/test/java/testing/CompoundScopeTest.java
+++ b/src/test/java/testing/CompoundScopeTest.java
@@ -1,26 +1,19 @@
package testing;
-
import java.io.File;
import java.io.IOException;
import java.util.ArrayList;
-import java.util.Hashtable;
import java.util.List;
import java.util.Map;
import org.junit.Ignore;
import org.junit.Test;
-
-
-
-
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.analysis.pragma.Pragma;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
-import de.tlc4b.analysis.MachineContext;
import de.tlc4b.util.Ast2String;
public class CompoundScopeTest {
@@ -33,39 +26,41 @@ public class CompoundScopeTest {
}
public void checkScope(String filename) throws BException, IOException {
-
+
final File machineFile = new File(filename);
-
+
BParser parser = new BParser(filename);
Start tree = parser.parseFile(machineFile, false);
- RecursiveMachineLoader r = new RecursiveMachineLoader(machineFile.getParent(), parser.getContentProvider());
-
-
+ RecursiveMachineLoader r = new RecursiveMachineLoader(
+ machineFile.getParent(), parser.getContentProvider());
+
List<Pragma> pragmas = new ArrayList<Pragma>();
pragmas.addAll(parser.getPragmas());
- r.loadAllMachines(machineFile, tree, parser.getSourcePositions(), parser.getDefinitions(), pragmas);
- //r.printAsProlog(new PrintWriter(System.out), false);
-
+ r.loadAllMachines(machineFile, tree, parser.getSourcePositions(),
+ parser.getDefinitions(), pragmas);
+ // r.printAsProlog(new PrintWriter(System.out), false);
+
Map<String, Start> map = r.getParsedMachines();
ArrayList<String> list = new ArrayList<String>(map.keySet());
-
-
- //Hashtable<String, MachineContext> machineContextsTable = new Hashtable<String, MachineContext>();
- //Hashtable<String, Typechecker> typecheckerTable = new Hashtable<String, Typechecker>();
+
+ // Hashtable<String, MachineContext> machineContextsTable = new
+ // Hashtable<String, MachineContext>();
+ // Hashtable<String, Typechecker> typecheckerTable = new
+ // Hashtable<String, Typechecker>();
for (int i = 0; i < list.size(); i++) {
String name = list.get(i);
- //System.out.println(name);
+ // System.out.println(name);
Start start = map.get(name);
final Ast2String ast2String2 = new Ast2String();
start.apply(ast2String2);
System.out.println(ast2String2.toString());
-
- //MachineContext c = new MachineContext(start, machineContextsTable);
- //machineContextsTable.put(name, c);
-
+
+ // MachineContext c = new MachineContext(start,
+ // machineContextsTable);
+ // machineContextsTable.put(name, c);
+
}
-
-
+
}
}
diff --git a/src/test/java/testing/CompoundTest.java b/src/test/java/testing/CompoundTest.java
index 4548075..769fff7 100644
--- a/src/test/java/testing/CompoundTest.java
+++ b/src/test/java/testing/CompoundTest.java
@@ -2,7 +2,6 @@ package testing;
import java.io.File;
import java.io.IOException;
-import java.io.PrintWriter;
import java.util.ArrayList;
import java.util.List;
diff --git a/src/test/resources/ltl/CounterError.mch b/src/test/resources/ltl/CounterError.mch
index ca93bec..cf73b82 100644
--- a/src/test/resources/ltl/CounterError.mch
+++ b/src/test/resources/ltl/CounterError.mch
@@ -1,4 +1,4 @@
-MACHINE CounterLTL
+MACHINE CounterError
DEFINITIONS
ASSERT_LTL_1 == "F {x = 12}"
VARIABLES x
@@ -8,4 +8,4 @@ INITIALISATION x:=1
OPERATIONS
Inc = PRE x < 10 THEN x:= x + 1 END;
Reset = PRE x = 10 THEN x := 1 END
-END
\ No newline at end of file
+END
diff --git a/src/test/resources/ltl/StatePropertyViolation.mch b/src/test/resources/ltl/StatePropertyViolation.mch
new file mode 100644
index 0000000..5e8a4c3
--- /dev/null
+++ b/src/test/resources/ltl/StatePropertyViolation.mch
@@ -0,0 +1,15 @@
+MACHINE StatePropertyViolation
+DEFINITIONS
+ ASSERT_LTL_1 == "!a.({a:ID} => {1=2})"
+SETS
+ ID={aa,bb}
+CONSTANTS iv
+PROPERTIES
+ iv:ID
+VARIABLES xx
+INVARIANT
+ xx:POW(ID)
+INITIALISATION xx:={}
+OPERATIONS
+ Set(yy) = SELECT yy:ID & yy /:xx THEN xx:= xx \/ {yy} END
+END
--
GitLab