diff --git a/build.gradle b/build.gradle index 790ad1115073b0532b8c6023273cf350f82324e5..3093b35f35feda70f55f6b6325de02fb13811e79 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 0000000000000000000000000000000000000000..009f6d6a92672d4f50c5b66616ce2474726018ab --- /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 0000000000000000000000000000000000000000..e47962d77e5c6e385c037f5ba9f37531a0336895 --- /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 0000000000000000000000000000000000000000..d008f86f8b12a8caaabfbae390ae8e8bd9142c04 --- /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 0000000000000000000000000000000000000000..415a4ad47e37350d05e9dc9b9768bb9635dd6d7a --- /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 0000000000000000000000000000000000000000..57230dadbb389a1c51e9919f8a8bde1b2d1cf4e7 --- /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 0000000000000000000000000000000000000000..dab2ad5d3a2ef02d5c6072d9f50b4427da421313 --- /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 0000000000000000000000000000000000000000..886f1fd41ae9cfe67131a427e3b7cfbf2d39f85a --- /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 524d23943c6d682199074f7985e4985bf8917b8c..73bb9261827b90488d70979e96fba0fc0fe72e02 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 Binary files /dev/null and b/src/test/resources/testing/.DS_Store differ