Skip to content
Snippets Groups Projects
Commit 2e73d65c authored by dgelessus's avatar dgelessus
Browse files

Replace TestUtil.tryTranslating with .translate

The extra TLC4B and TLC settings aren't relevant for tests that only
check that translation fails.
parent 2e4ac202
No related branches found
No related tags found
No related merge requests found
......@@ -11,12 +11,12 @@ public class UnsupportedConstructsTest {
@Test(expected = NotSupportedException.class)
public void testExtends() throws Exception {
final String machine = "MACHINE test\n" + "EXTENDS foo\n PROMOTES bar\n" + "END";
tryTranslating(machine);
translate(machine);
}
@Test(expected = NotSupportedException.class)
public void testImplementation() throws Exception {
final String machine = "IMPLEMENTATION test REFINES foo END";
tryTranslating(machine);
translate(machine);
}
}
......@@ -79,13 +79,6 @@ public class TestUtil {
assertEquals(expectedB, actualB);
}
public static void tryTranslating(final String machineString) throws BCompoundException {
TLC4BGlobals.setForceTLCToEvalConstants(false);
ToolIO.setMode(ToolIO.TOOL);
Translator b2tlaTranslator = new Translator(machineString);
b2tlaTranslator.translate();
}
public static String translateTLA2B(String moduleName, String tlaString, String configString)
throws TLA2BException {
return de.tla2bAst.Translator.translateModuleString(moduleName, tlaString, configString);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment