Refactoring

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)

build.xml

+<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

src/test/java/testing/CompoundScopeTest.java

+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);
+			
+		}
+		
+		
+	}
+}

src/test/java/testing/CompoundTest.java

+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);
+	}
+
+}

src/test/java/testing/Testing.java

+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);
+	}
+}

src/test/java/testing/Testing2.java

+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));
+//	}
+}

src/test/resources/basics/ELSEIF.mch

+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

src/test/resources/basics/NumbersTest.mch

+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

src/test/resources/laws/SequencesAsRelationsTest.mch

 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