Skip to content
Snippets Groups Projects
Commit 48161865 authored by hansen's avatar hansen
Browse files

removed old dependencies

parent 615a6961
Branches
Tags
No related merge requests found
......@@ -36,7 +36,6 @@ dependencies {
testCompile (group: 'junit', name: 'junit', version: '4.7')
testCompile (group: 'de.prob', name: 'tla2b', version: '1.0.4-SNAPSHOT')
testCompile (group: 'de.prob', name: 'tla2bAST', version: '1.0.5-SNAPSHOT')
releaseJars (group: 'de.tla', name: 'tlatools', version: '1.0.0-SNAPSHOT')
......
package de.tlc4b.analysis;
import static de.tlc4b.util.TestUtil.checkMachine;
import org.junit.Test;
import de.tlc4b.exceptions.NotSupportedException;
public class NotSupportedTest {
@Test(expected = NotSupportedException.class)
public void testDuplicateSeenMachine() throws Exception {
String machine = "MACHINE test \n" + "SEES M1 \n" + "END";
checkMachine(machine);
}
}
......@@ -28,8 +28,8 @@ public class RenamerTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES WITH_1 \n"
+ "Inv == WITH_1 = 1\n"
+ "Init == WITH_1 = 1 \n"
+ "Invariant1 == WITH_1 = 1\n"
+ "Init == WITH_1 = 1 \n\n"
+ "Next == 1 = 2 /\\ UNCHANGED <<WITH_1>>\n"
+ "====";
compare(expected, machine);
......@@ -47,7 +47,7 @@ public class RenamerTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Inv == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "WITH_1 == x' = 2\n"
+ "Next == WITH_1 \n"
......
......@@ -15,12 +15,6 @@ public class ScopeTest {
checkMachine(machine);
}
@Test(expected = ScopeException.class)
public void testDuplicateSeenMachine() throws Exception {
String machine = "MACHINE test \n" + "SEES M1, M1 \n" + "END";
checkMachine(machine);
}
@Test(expected = ScopeException.class)
public void testConstraintsMissingMachineParameter() throws Exception {
String machine = "MACHINE test \n" + "CONSTRAINTS k = 1 \n" + "END";
......
......@@ -18,7 +18,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Inv == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
......@@ -37,7 +37,7 @@ public class OperationsTest {
String expected = "---- MODULE test ----\n"
+ "VARIABLES x \n"
+ "Inv == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == x = 1 \n"
+ "foo == x' = 2\n"
+ "Next == foo \n"
......
......@@ -36,7 +36,7 @@ public class SubstitutionsTest {
String expected = "---- MODULE test ----\n"
+ "EXTENDS Naturals \n"
+ "VARIABLES x \n"
+ "Inv == x = 1\n"
+ "Invariant1 == x = 1\n"
+ "Init == \\E a \\in {1}, b \\in {2} : TRUE /\\ x = a + b \n"
+ "Next == 1 = 2 /\\ UNCHANGED <<x>>\n"
+ "====";
......
......@@ -11,14 +11,14 @@ import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.output.ASTPrettyPrinter;
import de.tla2b.output.Renamer;
import de.tlc4b.TLC4BGlobals;
import de.tlc4b.Translator;
import de.tlc4b.tlc.TLCResults.TLCResult;
......@@ -36,12 +36,17 @@ public class TestUtil {
* create standard modules BBuildins
*/
String name = b2tlaTranslator.getMachineName();
StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
.translateString(name, b2tlaTranslator.getModuleString(), null);
StringBuilder sb2 = de.tla2b.translation.Tla2BTranslator
.translateString(name, expectedModule, null);
if (!sb2.toString().equals(sb1.toString())) {
String moduleName = b2tlaTranslator.getMachineName();
String str1 = translateTLA2B(moduleName,
b2tlaTranslator.getModuleString());
String str2 = translateTLA2B(moduleName, expectedModule);
// StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
// .translateString(name, b2tlaTranslator.getModuleString(), null);
// StringBuilder sb2 = de.tla2b.translation.Tla2BTranslator
// .translateString(name, expectedModule, null);
if (!str1.equals(str2)) {
// assertEquals(expected, actual);
fail("expected:\n" + expectedModule + "\nbut was:\n"
......@@ -50,27 +55,38 @@ public class TestUtil {
// assertEquals(sb2.toString(), sb1.toString());
}
public static String translateTLA2B(String moduleName, String tlaString)
throws TLA2BException {
return de.tla2bAst.Translator.translateModuleString(moduleName,
tlaString, null);
}
public static void compareLTL(String expectedModule, String machine, String ltlFormula)
throws Exception {
public static String translateTLA2B(String moduleName, String tlaString,
String configString) throws TLA2BException {
return de.tla2bAst.Translator.translateModuleString(moduleName,
tlaString, configString);
}
public static void compareLTL(String expectedModule, String machine,
String ltlFormula) throws Exception {
Translator b2tlaTranslator = new Translator(machine, ltlFormula);
b2tlaTranslator.translate();
System.out.println(b2tlaTranslator.getModuleString());
String name = b2tlaTranslator.getMachineName();
de.tla2b.translation.Tla2BTranslator
.translateString(name, b2tlaTranslator.getModuleString(), null);
// de.tla2b.translation.Tla2BTranslator.translateString(name,
// b2tlaTranslator.getModuleString(), null);
assertEquals(expectedModule, b2tlaTranslator.getModuleString());
}
public static void checkMachine(String machine)
throws Exception {
public static void checkMachine(String machine) throws Exception {
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
System.out.println(b2tlaTranslator.getModuleString());
String name = b2tlaTranslator.getMachineName();
de.tla2b.translation.Tla2BTranslator
.translateString(name, b2tlaTranslator.getModuleString(), null);
String str1 = translateTLA2B(name, b2tlaTranslator.getModuleString());
// de.tla2b.translation.Tla2BTranslator.translateString(name,
// b2tlaTranslator.getModuleString(), null);
}
public static void print(Start start) {
......@@ -88,9 +104,13 @@ public class TestUtil {
System.out.println(b2tlaTranslator.getConfigString());
String name = b2tlaTranslator.getMachineName();
de.tla2b.translation.Tla2BTranslator
.translateString(name, b2tlaTranslator.getModuleString(),
//parse check
translateTLA2B(name, b2tlaTranslator.getModuleString(),
b2tlaTranslator.getConfigString());
// de.tla2b.translation.Tla2BTranslator.translateString(name,
// b2tlaTranslator.getModuleString(),
// b2tlaTranslator.getConfigString());
assertEquals(expectedModule, b2tlaTranslator.getModuleString());
assertEquals(expectedConfig, b2tlaTranslator.getConfigString());
......@@ -105,17 +125,17 @@ public class TestUtil {
System.out.println(b2tlaTranslator.getConfigString());
String name = b2tlaTranslator.getMachineName();
StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
.translateString(name, b2tlaTranslator.getModuleString(),
b2tlaTranslator.getConfigString());
StringBuilder sb2 = de.tla2b.translation.Tla2BTranslator
.translateString(name, expectedModule, expectedConfig);
if (!sb2.toString().equals(sb1.toString())) {
fail("expected:\n" + expectedModule + "\nbut was:\n"
+ b2tlaTranslator.getModuleString() + "\n\nexpected:\n"
+ expectedConfig + "\nbut was:\n"
+ b2tlaTranslator.getConfigString());
}
// StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
// .translateString(name, b2tlaTranslator.getModuleString(),
// b2tlaTranslator.getConfigString());
// StringBuilder sb2 = de.tla2b.translation.Tla2BTranslator
// .translateString(name, expectedModule, expectedConfig);
// if (!sb2.toString().equals(sb1.toString())) {
// fail("expected:\n" + expectedModule + "\nbut was:\n"
// + b2tlaTranslator.getModuleString() + "\n\nexpected:\n"
// + expectedConfig + "\nbut was:\n"
// + b2tlaTranslator.getConfigString());
// }
}
public static void compareEquals(String expected, String machine)
......@@ -135,7 +155,8 @@ public class TestUtil {
public static TLCResult test(String[] args) throws IOException {
System.out.println("Starting JVM...");
final Process p = startJVM("", TLC4BTester.class.getCanonicalName(), args);
final Process p = startJVM("", TLC4BTester.class.getCanonicalName(),
args);
StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
stdOut.start();
StreamGobbler errOut = new StreamGobbler(p.getErrorStream());
......@@ -160,10 +181,6 @@ public class TestUtil {
return null;
}
private static Process startJVM(final String optionsAsString,
final String mainClass, final String[] arguments)
throws IOException {
......@@ -188,8 +205,6 @@ public class TestUtil {
}
class StreamGobbler extends Thread {
private InputStream is;
private ArrayList<String> log;
......@@ -217,4 +232,3 @@ class StreamGobbler extends Thread {
}
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment