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

add tests for instance transformation

parent 07f341f6
No related branches found
No related tags found
No related merge requests found
package de.tla2b.examples; package de.tla2b.examples;
import org.junit.Ignore;
import org.junit.Test; import org.junit.Test;
import static de.tla2b.util.TestUtil.runModule; import static de.tla2b.util.TestUtil.runModule;
...@@ -13,8 +14,46 @@ public class InstanceTest { ...@@ -13,8 +14,46 @@ public class InstanceTest {
} }
@Test @Test
public void testInstance() throws Exception { public void testConstantSubstitution1() throws Exception {
String file = "src/test/resources/examples/instance/constantSubstitution/InstanceOpArg3.tla";
runModule(file);
}
@Test
public void testConstantSubstitution2() throws Exception {
String file = "src/test/resources/examples/instance/constantSubstitution/InstanceValue2.tla";
runModule(file);
}
@Test
public void testOneInstanced() throws Exception {
String file = "src/test/resources/examples/instance/Counter/OneInstanced.tla"; String file = "src/test/resources/examples/instance/Counter/OneInstanced.tla";
runModule(file); runModule(file);
} }
@Test
public void testTwoInstanced() throws Exception {
String file = "src/test/resources/examples/instance/Counter/TwoInstanced.tla";
runModule(file);
}
@Test
public void testLetInstanced() throws Exception {
String file = "src/test/resources/examples/instance/let/InstanceLet.tla";
runModule(file);
}
@Test
public void testOpArgInstanced() throws Exception {
String file = "src/test/resources/examples/instance/OpArg/OpArgInstanced.tla";
runModule(file);
}
@Ignore
@Test
public void testSimpleTwoInstanced() throws Exception {
// TODO: implement in Typechecker
String file = "src/test/resources/examples/instance/twoInstanced/first.tla";
runModule(file);
}
} }
-------------------------- MODULE first ----------------------------- -------------------------- MODULE second -----------------------------
EXTENDS Naturals EXTENDS Naturals
CONSTANTS c1 CONSTANTS c1
......
-------------------------- MODULE first ----------------------------- -------------------------- MODULE second -----------------------------
EXTENDS Naturals EXTENDS Naturals
CONSTANTS c1 CONSTANTS c1
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment