Skip to content
Snippets Groups Projects
Commit d47591e2 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

cleanup tests

parent 5d428bdc
No related branches found
No related tags found
No related merge requests found
Showing
with 586 additions and 589 deletions
package de.tla2b.examples; package de.tla2b.examples;
import static de.tla2b.util.TestUtil.runModule;
import org.junit.Ignore; import org.junit.Ignore;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.runModule;
public class InstanceTest { public class InstanceTest {
......
package de.tla2b.examples; package de.tla2b.examples;
import java.io.File;
import java.util.List;
import de.tla2b.util.TestUtil; import de.tla2b.util.TestUtil;
import org.junit.Test; import org.junit.Test;
import org.junit.runner.RunWith; import org.junit.runner.RunWith;
import org.junit.runners.Parameterized; import org.junit.runners.Parameterized;
import java.io.File;
import java.util.List;
@RunWith(Parameterized.class) @RunWith(Parameterized.class)
public class RegressionTests { public class RegressionTests {
private final File moduleFile; private final File moduleFile;
...@@ -17,13 +16,13 @@ public class RegressionTests { ...@@ -17,13 +16,13 @@ public class RegressionTests {
this.moduleFile = machine; this.moduleFile = machine;
} }
@Test
public void testRunTLC() throws Exception {
TestUtil.loadTlaFile(moduleFile.getPath());
}
@Parameterized.Parameters(name = "{0}") @Parameterized.Parameters(name = "{0}")
public static List<File> getConfig() { public static List<File> getConfig() {
return TestUtil.getModulesRecursively("./src/test/resources/regression"); return TestUtil.getModulesRecursively("./src/test/resources/regression");
} }
@Test
public void testRunTLC() throws Exception {
TestUtil.loadTlaFile(moduleFile.getPath());
}
} }
...@@ -79,16 +79,19 @@ public class ComplexExpressionTest { ...@@ -79,16 +79,19 @@ public class ComplexExpressionTest {
"r = [a |-> [x|->1,y|->TRUE], b |-> 1] " "r = [a |-> [x|->1,y|->TRUE], b |-> 1] "
+ "/\\ r2 = [r EXCEPT !.a.x = 2]"); + "/\\ r2 = [r EXCEPT !.a.x = 2]");
} }
@Test @Test
public void testConstraint1() throws Exception { public void testConstraint1() throws Exception {
compareExpr("x**3 - 20*x**2 + 7*x = 14388", compareExpr("x**3 - 20*x**2 + 7*x = 14388",
"x^3 - 20*x^2 + 7*x = 14388"); "x^3 - 20*x^2 + 7*x = 14388");
} }
@Test @Test
public void testConstraintCHOOSE() throws Exception { public void testConstraintCHOOSE() throws Exception {
compareExpr("CHOOSE({x|x:0..100 & x**3 - 20*x**2 + 7*x = 14388})", compareExpr("CHOOSE({x|x:0..100 & x**3 - 20*x**2 + 7*x = 14388})",
"CHOOSE x \\in 0..100: x^3 - 20*x^2 + 7*x = 14388"); "CHOOSE x \\in 0..100: x^3 - 20*x^2 + 7*x = 14388");
} }
@Test @Test
public void testConstraintCHOOSENested() throws Exception { public void testConstraintCHOOSENested() throws Exception {
compareExpr("CHOOSE({y|y : 0 .. 100 & y = CHOOSE({x|x : 0 .. 100 & x ** 3 - 20 * x ** 2 + 7 * x = 14388})})", compareExpr("CHOOSE({y|y : 0 .. 100 & y = CHOOSE({x|x : 0 .. 100 & x ** 3 - 20 * x ** 2 + 7 * x = 14388})})",
......
package de.tla2b.expression; package de.tla2b.expression;
import static de.tla2b.util.TestUtil.compareExprIncludingModel; import de.tla2b.exceptions.TypeErrorException;
import org.junit.Test; import org.junit.Test;
import de.tla2b.exceptions.TypeErrorException; import static de.tla2b.util.TestUtil.compareExprIncludingModel;
public class ModuleAndExpressionTest { public class ModuleAndExpressionTest {
......
package de.tla2b.expression; package de.tla2b.expression;
import static de.tla2b.util.TestUtil.compareExpr; import de.tla2b.exceptions.ExpressionTranslationException;
import org.junit.Test; import org.junit.Test;
import de.tla2b.exceptions.ExpressionTranslationException; import static de.tla2b.util.TestUtil.compareExpr;
public class TestError { public class TestError {
......
package de.tla2b.expression; package de.tla2b.expression;
import static de.tla2b.util.TestUtil.compareExpr;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.compareExpr;
public class TestSequences { public class TestSequences {
@Test @Test
......
package de.tla2b.main; package de.tla2b.main;
import java.io.File; import de.tla2b.TLA2B;
import org.junit.Test; import org.junit.Test;
import de.tla2b.TLA2B; import java.io.File;
public class MainTest { public class MainTest {
......
package de.tla2b.main; package de.tla2b.main;
import org.junit.Test;
import de.tla2b.util.TestUtil; import de.tla2b.util.TestUtil;
import org.junit.Test;
public class RenamerTest { public class RenamerTest {
......
package de.tla2b.prettyprintb; package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Ignore; import org.junit.Ignore;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.compare;
public class ActionsTest { public class ActionsTest {
@Ignore // changed UNCHANGED translation TODO fix test @Ignore // changed UNCHANGED translation TODO fix test
......
package de.tla2b.prettyprintb; package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Ignore; import org.junit.Ignore;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.compare;
public class BBuiltInsTest { public class BBuiltInsTest {
@Test @Test
......
package de.tla2b.prettyprintb; package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.compare;
public class DefinitionsTest { public class DefinitionsTest {
@Test @Test
......
package de.tla2b.prettyprintb; package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Ignore; import org.junit.Ignore;
import org.junit.Test; import org.junit.Test;
import util.ToolIO; import util.ToolIO;
import static de.tla2b.util.TestUtil.compare;
public class ExceptTest { public class ExceptTest {
@Test @Test
...@@ -68,6 +67,7 @@ public class ExceptTest { ...@@ -68,6 +67,7 @@ public class ExceptTest {
+ "END"; + "END";
compare(expected, module); compare(expected, module);
} }
@Test @Test
public void testNestedFunctionAt() throws Exception { public void testNestedFunctionAt() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n" final String module = "-------------- MODULE Testing ----------------\n"
......
package de.tla2b.prettyprintb; package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.compare;
public class ExtensibleRecordTest { public class ExtensibleRecordTest {
@Test @Test
......
package de.tla2b.prettyprintb; package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.compare;
public class ExternelFunctionsTest { public class ExternelFunctionsTest {
......
package de.tla2b.prettyprintb; package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Ignore; import org.junit.Ignore;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.compare;
public class FunctionTest { public class FunctionTest {
@Test @Test
......
package de.tla2b.prettyprintb; package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.compare;
public class MacroTest { public class MacroTest {
......
package de.tla2b.prettyprintb; package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.compare;
public class MiscellaneousConstructsTest { public class MiscellaneousConstructsTest {
@Test @Test
...@@ -132,7 +132,6 @@ public class MiscellaneousConstructsTest { ...@@ -132,7 +132,6 @@ public class MiscellaneousConstructsTest {
} }
@Test @Test
public void testUnBoundedChooseTuple() throws Exception { public void testUnBoundedChooseTuple() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n" final String module = "-------------- MODULE Testing ----------------\n"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment