From 001129f2a794328b1e09b7b7df69831ac7c2941c Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Thu, 13 Mar 2014 11:05:50 +0100
Subject: [PATCH] Refactoring
---
build.gradle | 2 +-
build.xml | 5 +
src/test/java/testing/CompoundScopeTest.java | 69 +++++++++++
src/test/java/testing/CompoundTest.java | 41 +++++++
src/test/java/testing/Testing.java | 47 ++++++++
src/test/java/testing/Testing2.java | 61 ++++++++++
src/test/resources/basics/ELSEIF.mch | 8 ++
.../FunctionsAsRelationsTest.mch | 0
src/test/resources/basics/NumbersTest.mch | 5 +
.../laws/SequencesAsRelationsTest.mch | 107 ++++++++----------
src/test/resources/testing/.DS_Store | Bin 0 -> 6148 bytes
11 files changed, 286 insertions(+), 59 deletions(-)
create mode 100644 build.xml
create mode 100644 src/test/java/testing/CompoundScopeTest.java
create mode 100644 src/test/java/testing/CompoundTest.java
create mode 100644 src/test/java/testing/Testing.java
create mode 100644 src/test/java/testing/Testing2.java
create mode 100644 src/test/resources/basics/ELSEIF.mch
rename src/test/resources/{laws => basics}/FunctionsAsRelationsTest.mch (100%)
create mode 100644 src/test/resources/basics/NumbersTest.mch
create mode 100644 src/test/resources/testing/.DS_Store
diff --git a/build.gradle b/build.gradle
index 790ad11..3093b35 100644
--- a/build.gradle
+++ b/build.gradle
@@ -29,7 +29,7 @@ dependencies {
//compile(group: 'de.prob', name: 'de.prob.core.kernel', version: '2.0.0-milestone-13-SNAPSHOT')
testCompile (group: 'junit', name: 'junit', version: '4.+')
- testCompile (group: 'de.prob', name: 'tla2b', version: '1.0.3-SNAPSHOT')
+ testCompile (group: 'de.prob', name: 'tla2b', version: '1.0.4-SNAPSHOT')
releaseJars (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT')
releaseJars (group: 'de.prob', name: 'prologlib', version: parser_version)
diff --git a/build.xml b/build.xml
new file mode 100644
index 0000000..009f6d6
--- /dev/null
+++ b/build.xml
@@ -0,0 +1,5 @@
+<project default="copy">
+ <target name="copy">
+ <copy file="build/b2tla/B2TLA.jar" tofile="../../Desktop/ProB/lib/B2TLA.jar"/>
+ </target>
+</project>
\ No newline at end of file
diff --git a/src/test/java/testing/CompoundScopeTest.java b/src/test/java/testing/CompoundScopeTest.java
new file mode 100644
index 0000000..e47962d
--- /dev/null
+++ b/src/test/java/testing/CompoundScopeTest.java
@@ -0,0 +1,69 @@
+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.b2tla.analysis.Ast2String;
+import de.b2tla.analysis.MachineContext;
+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;
+
+public class CompoundScopeTest {
+
+ @Ignore
+ @Test
+ public void test() throws BException, IOException {
+ String filename = "src/test/resources/M1.mch";
+ checkScope(filename);
+ }
+
+ 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());
+
+
+ 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);
+
+ 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>();
+ for (int i = 0; i < list.size(); i++) {
+ String name = list.get(i);
+ //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);
+
+ }
+
+
+ }
+}
diff --git a/src/test/java/testing/CompoundTest.java b/src/test/java/testing/CompoundTest.java
new file mode 100644
index 0000000..d008f86
--- /dev/null
+++ b/src/test/java/testing/CompoundTest.java
@@ -0,0 +1,41 @@
+package testing;
+
+import java.io.File;
+import java.io.IOException;
+import java.io.PrintWriter;
+import java.util.ArrayList;
+import java.util.List;
+
+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;
+
+public class CompoundTest {
+
+ @Test
+ public void test() throws IOException, BException {
+ String filename = "src/test/resources/compound/M1.mch";
+ //final int dot = filename.lastIndexOf('.');
+ final File machineFile = new File(filename);
+ //final String probfilename = filename.substring(0, dot) + ".prob";
+
+
+
+ BParser parser = new BParser(filename);
+ Start tree = parser.parseFile(machineFile, false);
+
+ 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);
+ }
+
+}
diff --git a/src/test/java/testing/Testing.java b/src/test/java/testing/Testing.java
new file mode 100644
index 0000000..415a4ad
--- /dev/null
+++ b/src/test/java/testing/Testing.java
@@ -0,0 +1,47 @@
+package testing;
+
+import static de.b2tla.tlc.TLCResults.TLCResult.*;
+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.b2tla.B2TLA;
+import de.b2tla.tlc.TLCResults.TLCResult;
+import de.b2tla.util.AbstractParseMachineTest;
+import de.b2tla.util.PolySuite;
+import de.b2tla.util.TestPair;
+import de.b2tla.util.PolySuite.Config;
+import de.b2tla.util.PolySuite.Configuration;
+
+
+
+@RunWith(PolySuite.class)
+public class Testing extends AbstractParseMachineTest{
+
+
+ private final File machine;
+ private final TLCResult error;
+
+ public Testing(File machine, TLCResult result) {
+ this.machine = machine;
+ this.error = result;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ String[] a = new String[] { machine.getPath()};
+ //B2TLA.main(a);
+ //assertEquals(error, B2TLA.test(a,false));
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<TestPair> list = new ArrayList<TestPair>();
+ list.add(new TestPair(NoError, "./src/test/resources/Testing"));
+ return getConfiguration(list);
+ }
+}
diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java
new file mode 100644
index 0000000..57230da
--- /dev/null
+++ b/src/test/java/testing/Testing2.java
@@ -0,0 +1,61 @@
+package testing;
+
+
+import static de.b2tla.tlc.TLCResults.TLCResult.NoError;
+import static org.junit.Assert.*;
+import static de.b2tla.util.TestUtil.test;
+import java.io.File;
+import java.util.ArrayList;
+
+import org.junit.Test;
+import org.junit.runner.RunWith;
+
+import de.b2tla.B2TLA;
+import de.b2tla.tlc.TLCResults.TLCResult;
+import de.b2tla.util.AbstractParseMachineTest;
+import de.b2tla.util.PolySuite;
+import de.b2tla.util.TestPair;
+import de.b2tla.util.PolySuite.Config;
+import de.b2tla.util.PolySuite.Configuration;
+
+@RunWith(PolySuite.class)
+public class Testing2 extends AbstractParseMachineTest{
+
+ private final File machine;
+ private final TLCResult error;
+
+ public Testing2(File machine, TLCResult result) {
+ this.machine = machine;
+ this.error = result;
+ }
+
+ @Test
+ public void testRunTLC() throws Exception {
+ String[] a = new String[] {machine.getPath()};
+
+ B2TLA.main(a);
+ //B2TLA.test(a,true);
+ //test(a);
+ //assertEquals(error, B2TLA.test(a,true));
+ //assertEquals(1,2);
+ }
+
+ @Config
+ public static Configuration getConfig() {
+ final ArrayList<TestPair> list = new ArrayList<TestPair>();
+ list.add(new TestPair(NoError, "./src/test/resources/testing"));
+ return getConfiguration(list);
+ }
+
+// @Test
+// public void testInvariantError() throws Exception {
+// String[] a = new String[] { "./src/test/resources/laws/RelationsTest.mch", "-tmp" };
+// B2TLA.main(a);
+// }
+
+// @Test
+// public void testInvariantError() throws Exception {
+// String[] a = new String[] { "./src/test/resources/errors/InvariantError.mch" };
+// assertEquals(InvariantViolation, B2TLA.test(a,false));
+// }
+}
diff --git a/src/test/resources/basics/ELSEIF.mch b/src/test/resources/basics/ELSEIF.mch
new file mode 100644
index 0000000..dab2ad5
--- /dev/null
+++ b/src/test/resources/basics/ELSEIF.mch
@@ -0,0 +1,8 @@
+MACHINE ELSEIF
+VARIABLES x,y,z,c
+INVARIANT x : {1,4} & y : {1,2} & z : {1,3} & c : 1..3
+INITIALISATION x,y,z,c := 1,1,1,1
+OPERATIONS
+ foo = IF c=1 THEN x:= 1 ELSIF c=2 THEN y:= 2 ELSIF c=3 THEN z:= 3 ELSE x:= 4 END;
+ set2 = BEGIN c :: 1..3 END
+END
\ No newline at end of file
diff --git a/src/test/resources/laws/FunctionsAsRelationsTest.mch b/src/test/resources/basics/FunctionsAsRelationsTest.mch
similarity index 100%
rename from src/test/resources/laws/FunctionsAsRelationsTest.mch
rename to src/test/resources/basics/FunctionsAsRelationsTest.mch
diff --git a/src/test/resources/basics/NumbersTest.mch b/src/test/resources/basics/NumbersTest.mch
new file mode 100644
index 0000000..886f1fd
--- /dev/null
+++ b/src/test/resources/basics/NumbersTest.mch
@@ -0,0 +1,5 @@
+MACHINE NumbersTest
+PROPERTIES
+SIGMA(x).( x :{ 1, 2, 3 } | x + 1 ) = 9
+& SIGMA(x).( x :{ 1, 2, 3 } | 1 ) = 3
+END
\ No newline at end of file
diff --git a/src/test/resources/laws/SequencesAsRelationsTest.mch b/src/test/resources/laws/SequencesAsRelationsTest.mch
index 524d239..73bb926 100644
--- a/src/test/resources/laws/SequencesAsRelationsTest.mch
+++ b/src/test/resources/laws/SequencesAsRelationsTest.mch
@@ -1,30 +1,20 @@
MACHINE SequencesAsRelationsTest
-CONSTANTS s, s2, s3, empty
PROPERTIES
-s = {(1,1)}
-& s2 = {(1,2)}
-& s3 = {(1,1),(2,2), (3,3)}
-& empty = {}
-& s \/ {} = s /* force the typechecker to use sequences as relations */
-& s2 \/ {} = s2 /* force the typechecker to use sequences as relations */
-& s3 \/ {} = s3 /* force the typechecker to use sequences as relations */
-& empty \/ {} = empty /* force the typechecker to use sequences as relations */
-
-& empty = []
-& s = [1]
+ {} = []
+& {(1,1)} = [1]
/* Set of sequences */
-& s : seq({1})
-& s2 /: seq({1})
-& not(s /: seq({1}))
-& empty : seq({1})
-& empty : seq({})
+& {(1,1)} : seq({1})
+& {(1,2)} /: seq({1})
+& not({(1,1)} /: seq({1}))
+& {} : seq({1})
+& {} : seq({})
/* Set of sequences */
-& s : seq1({1})
-& empty /: seq1({})
-& s2 /: seq1({1})
+& {(1,1)} : seq1({1})
+& {} /: seq1({})
+& {(1,2)} /: seq1({1})
& not({} : seq1({1}))
& not({} : seq1({}))
@@ -33,66 +23,67 @@ s = {(1,1)}
& iseq({1}) = {{},{(1,1)}}
/* Set of non empty injective sequences */
-& iseq1({}) /= {{}}
-& iseq1({1}) = {s}
+& iseq1({}) = {}
+& iseq1({1}) = {{(1,1)}}
/* Size */
-& size(empty) = 0
-& size(s3) = 3
+& size({}) = 0
+& size({(1,1),(2,2)}) = 2
/* Concatenation */
-& s^{(1,2)} = {(1,1),(2,2)}
-& s^{} = {(1,1)}
-& {}^s3 = {(1,1),(2,2),(3,3)}
-& {}^{} = empty
+& {(1,1),(2,2)}^{(1,3)} = {(1,1),(2,2),(3,3)}
+& {(1,1),(2,2)}^{} = {(1,1),(2,2)}
+& {}^{(1,1),(2,2)} = {(1,1),(2,2)}
+& {}^{} = {}
/* Prepand */
-& 1 -> {(1,2),(2,3)} = s3
-& 1 -> {} = s
+& 1 -> {(1,2),(2,3)} = {(1,1),(2,2),(3,3)}
+& 1 -> {} = {(1,1)}
/* Append */
-& {(1,1),(2,2)} <- 3 = s3
-& empty <- 1 = {(1,1)}
+& {(1,1),(2,2)} <- 3 = {(1,1),(2,2),(3,3)}
+& {} <- 1 = {(1,1)}
/* Front */
-& front({(1,1)}) = empty
-& front(s3) = {(1,1),(2,2)}
+& front({(1,1)}) = {}
+& front({(1,1),(2,2),(3,3)}) = {(1,1),(2,2)}
/* First */
-& first(s) = 1
-& first(s3) = 1
+& first({(1,1)}) = 1
+& first({(1,1),(2,2)}) = 1
/* Tail */
-& tail(s) = {}
-& tail(s3) = {(1,2),(2,3)}
+& tail({(1,1)}) = {}
+& tail({(1,1),(2,2),(3,3)}) = {(1,2),(2,3)}
/* Last */
-& last(s) = 1
-& last(s3) = 3
+& last({(1,1)}) = 1
+& last({(1,1),(2,2)}) = 2
/* Reverse */
-& rev(empty) = {}
-& rev(s) = {(1,1)}
-& rev(s3) = {(1,3),(2,2),(3,1)}
+& rev({}) = {}
+& rev({(1,1)}) = {(1,1)}
+& rev({(1,1),(2,2),(3,3)}) = {(1,3),(2,2),(3,1)}
/* Generalized Concatenation */
-& conc({(1,{(1,1),(2,2)}),(2,{(1,3)})}) = s3
-& conc({(1,s3),(2,{})}) = s3
-& conc({(1,{}), (2,s3)}) = s3
-& conc({(1,empty),(2,{})}) = {}
+& conc({(1,{(1,1),(2,2)}),(2,{(1,3)})}) = {(1,1),(2,2),(3,3)}
+& conc({(1,{(1,1),(2,2)}),(2,{})}) = {(1,1),(2,2)}
+& conc({(1,{}), (2,{(1,1),(2,2)})}) = {(1,1),(2,2)}
+& conc({(1,{}),(2,{})}) = {}
+& conc([{}, {(1,1),(2,2)}]) = {(1,1),(2,2)}
/* Perm */
-& perm({3,4}) = {{(1,3)}\/ {(2,4)},{(1,4),(2,3)}}
-& perm(empty) = {{}}
+& perm({3,4}) = {{(1,3),(2,4)},{(1,4),(2,3)}}
+& perm({}) = {{}}
/* Take first elements */
-& s3 /|\ 1 = {(1,1)}
-& s3 /|\ 3 = s3
-& s /|\ 0 = {}
-& empty /|\ 0 = {}
-
-& s3 \|/ 2 = {(1,3)}
-& s3 \|/ 0 = s3
-& s \|/ 1 = {}
-& empty \|/ 0 = {}
+& {(1,1),(2,2)} /|\ 1 = {(1,1)}
+& {(1,1),(2,2)} /|\ 2 = {(1,1),(2,2)}
+& {(1,1)} /|\ 0 = {}
+& {} /|\ 0 = {}
+
+& {(1,1),(2,2)} \|/ 1 = {(1,2)}
+& {(1,1),(2,2)} \|/ 0 = {(1,1),(2,2)}
+& {(1,1)} \|/ 1 = {}
+& {} \|/ 0 = {}
END
\ No newline at end of file
diff --git a/src/test/resources/testing/.DS_Store b/src/test/resources/testing/.DS_Store
new file mode 100644
index 0000000000000000000000000000000000000000..5008ddfcf53c02e82d7eee2e57c38e5672ef89f6
GIT binary patch
literal 6148
zcmZQzU|@7AO)+F(5MW?n;9!8z45|!R0Z1N%F(jFgL>QrFAPJ2!M?+vV1V%$(Gz3ON
zU^D~<VF)ln+{D2Rp-0Kl5Eu=C(GY-#0H}OW0QD6Z7#JL&bOVG2Nii@oFo3%Nj0_Ac
zFio(203!nfNGnJUNGpg2X=PvpvA|}4wK6b5wK9UcAq)(R;4TS>25V<v1ltVagS9g-
zf^BACV1#IAV1(Mt2<@RTf_gL{^C8+97{Ru~TsKOOhQMeDz(Rl-!Vmz}|E>%SxcdJP
zRior+2#kinunYl47MEZbCs3t{!+W4QHvuXKVuPw;Mo^s$(F3lEVT}ML$bg~*R5_@+
b2Uo?6kTwK}57Iu`5P${HC_Nei0}uiLNUI8I
literal 0
HcmV?d00001
--
GitLab