From ef1b03dbab2e6971bf1ec6b135f3c8d7ef0bc14f Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Thu, 9 Feb 2023 13:04:05 +0100
Subject: [PATCH] added generator tests for Sets/Relations in embedded mode
---
.../hhu/stups/codegenerator/TestHelper.java | 50 +++++
.../hhu/stups/codegenerator/rust/TestRS.java | 48 +----
.../rust_embedded/TestGenerator.java | 202 ++++++++++++++++++
.../codegenerator/rust_embedded/TestSets.java | 86 ++++++++
.../embedded/ConstNestedRelation.mch | 21 ++
.../embedded/ConstPowRelation.mch | 21 ++
.../codegenerator/embedded/ConstPowSet.mch | 20 ++
.../embedded/MaxPowEnumeratedSet.mch | 24 +++
.../codegenerator/embedded/NestedRelation.mch | 31 +++
.../codegenerator/embedded/PowRelation.mch | 26 +++
.../embedded/RedundantConstRelation.mch | 21 ++
.../embedded/RedundantConstSet.mch | 20 ++
.../embedded/SimpleEnumeratedSet.mch | 23 ++
.../embedded/SimplePowEnumeratedSet.mch | 23 ++
.../embedded/SimplePowPowEnumeratedSet.mch | 23 ++
.../codegenerator/embedded/SimpleRelation.mch | 27 +++
16 files changed, 625 insertions(+), 41 deletions(-)
create mode 100644 src/test/java/de/hhu/stups/codegenerator/TestHelper.java
create mode 100644 src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestGenerator.java
create mode 100644 src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestSets.java
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/ConstNestedRelation.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/ConstPowRelation.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/ConstPowSet.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/MaxPowEnumeratedSet.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/NestedRelation.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/PowRelation.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/RedundantConstRelation.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/RedundantConstSet.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/SimpleEnumeratedSet.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/SimplePowEnumeratedSet.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/SimplePowPowEnumeratedSet.mch
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/embedded/SimpleRelation.mch
diff --git a/src/test/java/de/hhu/stups/codegenerator/TestHelper.java b/src/test/java/de/hhu/stups/codegenerator/TestHelper.java
new file mode 100644
index 000000000..a3036fae9
--- /dev/null
+++ b/src/test/java/de/hhu/stups/codegenerator/TestHelper.java
@@ -0,0 +1,50 @@
+package de.hhu.stups.codegenerator;
+
+import java.io.ByteArrayOutputStream;
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.OutputStream;
+import java.nio.file.Path;
+import java.util.List;
+
+public class TestHelper {
+ public static void writeInputToOutput(InputStream inputStream, OutputStream outputStream) throws IOException {
+ int size;
+ byte[] buffer = new byte[1024];
+ while ((size = inputStream.read(buffer)) != -1)
+ outputStream.write(buffer, 0, size);
+ }
+
+ public static void writeInputToSystem(InputStream inputStream) throws IOException {
+ writeInputToOutput(inputStream, System.err);
+ }
+
+ public static String streamToString(InputStream inputStream) throws IOException {
+ ByteArrayOutputStream result = new ByteArrayOutputStream();
+ byte[] buffer = new byte[1024];
+ int length;
+ while ((length = inputStream.read(buffer)) != -1) {
+ result.write(buffer, 0, length);
+ }
+ return result.toString();
+ }
+
+ public static List<Path> generateCode(Path machinePath, GeneratorMode mode, boolean forModelChecking, String addition, boolean embedded) throws IOException {
+ CodeGenerator codeGenerator = new CodeGenerator();
+ return codeGenerator.generate(machinePath,
+ mode,
+ false,
+ String.valueOf(Integer.MIN_VALUE),
+ String.valueOf(Integer.MAX_VALUE),
+ "10",
+ forModelChecking,
+ false,
+ true,
+ addition,
+ false,
+ false,
+ null,
+ null,
+ embedded);
+ }
+}
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java b/src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java
index 2abe2ab17..39cdb6bba 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java
+++ b/src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java
@@ -2,6 +2,7 @@ package de.hhu.stups.codegenerator.rust;
import de.hhu.stups.codegenerator.CodeGenerator;
import de.hhu.stups.codegenerator.GeneratorMode;
+import de.hhu.stups.codegenerator.TestHelper;
import java.io.*;
import java.nio.file.Files;
@@ -15,27 +16,6 @@ import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertTrue;
public class TestRS {
- public static void writeInputToOutput(InputStream inputStream, OutputStream outputStream) throws IOException {
- int size;
- byte[] buffer = new byte[1024];
- while ((size = inputStream.read(buffer)) != -1)
- outputStream.write(buffer, 0, size);
- }
-
- public static void writeInputToSystem(InputStream inputStream) throws IOException {
- writeInputToOutput(inputStream, System.err);
- }
-
- private static String streamToString(InputStream inputStream) throws IOException {
- ByteArrayOutputStream result = new ByteArrayOutputStream();
- byte[] buffer = new byte[1024];
- int length;
- while ((length = inputStream.read(buffer)) != -1) {
- result.write(buffer, 0, length);
- }
- return result.toString();
- }
-
public void testRS(String machine) throws Exception {
testRS(machine, null, "DefaultAddition.strs", false);
}
@@ -68,21 +48,7 @@ public class TestRS {
if (machinePath == null) { machinePath = "../../../resources/test/de/hhu/stups/codegenerator/"; }
if (!machinePath.endsWith("/")) { machinePath += "/"; }
Path mchPath = Paths.get(CodeGenerator.class.getClassLoader().getResource("").toURI()).resolve(machinePath + machine + ".mch").normalize();
- CodeGenerator codeGenerator = new CodeGenerator();
- List<Path> rsFilePaths = codeGenerator.generate(mchPath,
- GeneratorMode.RS,
- false,
- String.valueOf(Integer.MIN_VALUE),
- String.valueOf(Integer.MAX_VALUE),
- "10",
- modelChecking,
- false,
- true,
- addition,
- false,
- false,
- null,
- null);
+ List<Path> rsFilePaths = TestHelper.generateCode(mchPath, GeneratorMode.RS, modelChecking, addition, false);
Path typesPath = Paths.get(this.getClass().getClassLoader().getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust/bmachine/src"));
Files.createDirectories(typesPath);
@@ -99,8 +65,8 @@ public class TestRS {
File newMainFile = typesPath.resolve(Paths.get("main.rs")).toFile();
mainPath.toFile().renameTo(newMainFile);
Process process = runtime.exec("cargo build --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml");
- writeInputToSystem(process.getErrorStream());
- writeInputToOutput(process.getErrorStream(), process.getOutputStream());
+ TestHelper.writeInputToSystem(process.getErrorStream());
+ TestHelper.writeInputToOutput(process.getErrorStream(), process.getOutputStream());
process.waitFor();
if (process.exitValue() != 0) {
throw new Exception("cargo build failed, exitcode: " + process.exitValue());
@@ -119,15 +85,15 @@ public class TestRS {
Process executeProcess = runtime.exec("cargo run --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml" + progArgs);
executeProcess.waitFor();
- String error = streamToString(executeProcess.getErrorStream());
+ String error = TestHelper.streamToString(executeProcess.getErrorStream());
if(executeProcess.exitValue() != 0) {
throw new RuntimeException(error);
}
- String result = streamToString(executeProcess.getInputStream());
+ String result = TestHelper.streamToString(executeProcess.getInputStream());
if (modelChecking && !machine.contains("MC")) machine += "_MC";
File outFile = Paths.get(CodeGenerator.class.getClassLoader().getResource("de/hhu/stups/codegenerator/" + machine + ".out").toURI()).toFile();
- String expectedOutput = streamToString(new FileInputStream(outFile)).replaceAll("[\n\r]", "");
+ String expectedOutput = TestHelper.streamToString(new FileInputStream(outFile)).replaceAll("[\n\r]", "");
result = result.replaceAll("\n", "");
if (!modelChecking) {
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestGenerator.java b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestGenerator.java
new file mode 100644
index 000000000..d63b8ba78
--- /dev/null
+++ b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestGenerator.java
@@ -0,0 +1,202 @@
+package de.hhu.stups.codegenerator.rust_embedded;
+
+import de.hhu.stups.codegenerator.CodeGenerator;
+import de.hhu.stups.codegenerator.GeneratorMode;
+import de.hhu.stups.codegenerator.definitions.SetDefinition;
+import de.hhu.stups.codegenerator.definitions.SetDefinitions;
+import de.hhu.stups.codegenerator.generators.MachineGenerator;
+import de.prob.parser.antlr.BProject;
+import de.prob.parser.ast.types.EnumeratedSetElementType;
+import org.junit.Test;
+
+import java.io.File;
+import java.util.List;
+import java.util.Map;
+
+import static org.junit.Assert.*;
+
+
+public class TestGenerator {
+
+ private MachineGenerator getMachineGenerator(String machine) {
+ ClassLoader classLoader = this.getClass().getClassLoader();
+ File file = new File(classLoader.getResource("de/hhu/stups/codegenerator/embedded/"+machine).getFile());
+ assertTrue(file.exists());
+ MachineGenerator machineGenerator = new MachineGenerator(GeneratorMode.RS, false, "-2147483648", "2147483647",
+ "10", false, false, null, false, false, null, true);
+
+ BProject bProject = CodeGenerator.parseProject(file.toPath());
+ machineGenerator.generateMachine(bProject.getMainMachine(), GeneratorMode.RS);
+ return machineGenerator;
+ }
+
+ @Test
+ public void test_SimpleEnumeratedSet() {
+ MachineGenerator machineGenerator = getMachineGenerator("SimpleEnumeratedSet.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(1, setDefinitions.size());
+
+ SetDefinition setCounters = setDefinitions.getDefinition(new EnumeratedSetElementType("Counters", null));
+ assertNotNull(setCounters);
+ assertEquals(3, setCounters.getElements().size());
+ }
+
+ @Test
+ public void test_SimplePowEnumeratedSet() {
+ MachineGenerator machineGenerator = getMachineGenerator("SimplePowEnumeratedSet.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(2, setDefinitions.size());
+
+ SetDefinition setCounters = setDefinitions.getDefinition(new EnumeratedSetElementType("POW(Counters)", null));
+ assertNotNull(setCounters);
+ assertEquals(8, setCounters.getElements().size());
+ }
+
+ @Test
+ public void test_SimplePowPowEnumeratedSet() {
+ MachineGenerator machineGenerator = getMachineGenerator("SimplePowPowEnumeratedSet.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(3, setDefinitions.size());
+
+ SetDefinition setCounters = setDefinitions.getDefinition(new EnumeratedSetElementType("POW(POW(Counters))", null));
+ assertNotNull(setCounters);
+ assertEquals(16, setCounters.getElements().size());
+ }
+
+ @Test
+ public void test_MaxPowEnumeratedSet() {
+ MachineGenerator machineGenerator = getMachineGenerator("MaxPowEnumeratedSet.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(4, setDefinitions.size());
+
+ SetDefinition setCounters = setDefinitions.getDefinition(new EnumeratedSetElementType("POW(POW(POW(Counters)))", null));
+ assertNotNull(setCounters);
+ assertEquals(16, setCounters.getElements().size());
+ }
+
+ @Test
+ public void test_SimpleRelation() {
+ MachineGenerator machineGenerator = getMachineGenerator("SimpleRelation.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ //relation itself does not need an enum, only when its needed as an SetItem (i.e. powerset/nested relation)
+ assertEquals(2, setDefinitions.size());
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Counters", null)));
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Persons", null)));
+ }
+
+ @Test
+ public void test_PowRelation() {
+ MachineGenerator machineGenerator = getMachineGenerator("PowRelation.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(4, setDefinitions.size());
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Counters", null)));
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Persons", null)));
+ SetDefinition rel = setDefinitions.getDefinition(new EnumeratedSetElementType("Counters*Persons", null));
+ assertNotNull(rel);
+ assertEquals(6, rel.getElements().size());
+ SetDefinition powRel = setDefinitions.getDefinition(new EnumeratedSetElementType("POW(Counters*Persons)", null));
+ assertNotNull(powRel);
+ assertEquals(64, powRel.getElements().size());
+ }
+
+ @Test
+ public void test_NestedRelation() {
+ MachineGenerator machineGenerator = getMachineGenerator("NestedRelation.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(5, setDefinitions.size());
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Counters", null)));
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Persons", null)));
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Shift", null)));
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Counters*Persons", null)));
+ SetDefinition powRel = setDefinitions.getDefinition(new EnumeratedSetElementType("POW(Counters*Persons)", null));
+ assertNotNull(powRel);
+ assertEquals(16, powRel.getElements().size());
+ }
+
+ @Test
+ public void test_RedundantConstSet() {
+ MachineGenerator machineGenerator = getMachineGenerator("RedundantConstSet.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(1, setDefinitions.size());
+ SetDefinition personsSet = setDefinitions.getDefinition(new EnumeratedSetElementType("Persons", null));
+ assertNotNull(personsSet);
+ assertEquals(3, personsSet.getElements().size());
+ }
+
+ @Test
+ public void test_ConstPowSet() {
+ MachineGenerator machineGenerator = getMachineGenerator("ConstPowSet.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(2, setDefinitions.size());
+ SetDefinition groupsSet = setDefinitions.getDefinition(new EnumeratedSetElementType("POW(Persons)", null));
+ assertNotNull(groupsSet);
+ assertTrue(groupsSet.isConstant());
+ List<String> groupElements = groupsSet.getElements();
+ assertEquals(2, groupElements.size());
+ Integer p1_p3_Idx = null;
+ Integer p2_Idx = null;
+ for (int i = 0; i < groupElements.size(); i++) {
+ switch (groupElements.get(i)) {
+ case "SET_P1__P3_TES": p1_p3_Idx = i; break;
+ case "SET_P2_TES": p2_Idx = i; break;
+ }
+ }
+ assertNotNull(p1_p3_Idx);
+ assertNotNull(p2_Idx);
+ Map<Integer, boolean[]> idxToBitarr = groupsSet.bitArrIndexed();
+ assertArrayEquals(new boolean[]{true, false, true}, idxToBitarr.get(p1_p3_Idx));
+ assertArrayEquals(new boolean[]{false, true, false}, idxToBitarr.get(p2_Idx));
+ }
+
+ @Test
+ public void test_RedundantConstRelation() {
+ MachineGenerator machineGenerator = getMachineGenerator("RedundantConstRelation.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(2, setDefinitions.size());
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Counters", null)));
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Persons", null)));
+ }
+
+ @Test
+ public void test_ConstPowRelation() {
+ MachineGenerator machineGenerator = getMachineGenerator("ConstPowRelation.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(4, setDefinitions.size());
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Counters", null)));
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Persons", null)));
+ SetDefinition rel = setDefinitions.getDefinition(new EnumeratedSetElementType("Counters*Persons", null));
+ assertNotNull(rel);
+ assertEquals(6, rel.getElements().size());
+ SetDefinition powRel = setDefinitions.getDefinition(new EnumeratedSetElementType("POW(Counters*Persons)", null));
+ assertNotNull(powRel);
+ assertEquals(2, powRel.getElements().size());
+ }
+
+ @Test
+ public void test_ConstNestedRelation() {
+ MachineGenerator machineGenerator = getMachineGenerator("ConstNestedRelation.mch");
+ SetDefinitions setDefinitions = machineGenerator.getSetDefinitions();
+
+ assertEquals(5, setDefinitions.size());
+ //TODO?: currently, setDef for 'Persons*POW(Counters*Counters)' is generated, not sure if that is necessary
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Counters", null)));
+ assertTrue(setDefinitions.containsDefinition(new EnumeratedSetElementType("Persons", null)));
+ SetDefinition rel = setDefinitions.getDefinition(new EnumeratedSetElementType("Counters*Counters", null));
+ assertNotNull(rel);
+ assertEquals(36, rel.getElements().size());
+ SetDefinition powRel = setDefinitions.getDefinition(new EnumeratedSetElementType("POW(Counters*Counters)", null));
+ assertNotNull(powRel);
+ assertEquals(2, powRel.getElements().size());
+ }
+}
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestSets.java b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestSets.java
new file mode 100644
index 000000000..0602051d6
--- /dev/null
+++ b/src/test/java/de/hhu/stups/codegenerator/rust_embedded/TestSets.java
@@ -0,0 +1,86 @@
+package de.hhu.stups.codegenerator.rust_embedded;
+
+import de.hhu.stups.codegenerator.CodeGenerator;
+import de.hhu.stups.codegenerator.GeneratorMode;
+import de.hhu.stups.codegenerator.TestHelper;
+import org.junit.Before;
+import org.junit.Test;
+
+import java.io.File;
+import java.io.IOException;
+import java.net.URISyntaxException;
+import java.net.URL;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.Arrays;
+import java.util.List;
+import java.util.stream.Collectors;
+
+import static org.junit.Assert.assertNotNull;
+
+public class TestSets {
+ final ClassLoader classLoader = this.getClass().getClassLoader();
+ final Path rustSrcPath = Paths.get(classLoader.getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust_embedded/bmachine/src"));
+ final Runtime runtime = Runtime.getRuntime();
+
+ public TestSets() throws URISyntaxException, IOException {
+ Files.createDirectories(rustSrcPath);
+ }
+
+ @Before
+ public void beforeEach() {
+ File[] oldFiles = rustSrcPath.toFile().listFiles();
+ if (oldFiles != null) Arrays.stream(oldFiles).forEach(File::delete);
+ }
+
+ @Test
+ public void test_SimpleEnumeratedSet() throws IOException, InterruptedException {
+ boolean execute = true;
+ boolean modelChecking = false;
+ boolean noInv = false;
+ boolean noDead = false;
+
+ String machineFile = "";
+ URL machineURL = classLoader.getResource("de/hhu/stups/codegenerator/embedded/" + machineFile);
+ assertNotNull(machineURL);
+ Path machinePath = Paths.get(machineURL.getPath());
+ List<Path> rsFilePaths = TestHelper.generateCode(machinePath, GeneratorMode.RS, false, "DefaultAddition.strs", true);
+ rsFilePaths = rsFilePaths.stream().map(path -> {
+ Path dest = rustSrcPath.resolve(Paths.get(path.toFile().getName()));
+ path.toFile().renameTo(dest.toFile());
+ return dest;
+ }).collect(Collectors.toList());
+
+ Path mainPath = rsFilePaths.get(rsFilePaths.size() - 1);
+ File newMainFile = rustSrcPath.resolve(Paths.get("main.rs")).toFile();
+ mainPath.toFile().renameTo(newMainFile);
+
+ Process process = runtime.exec("cargo build --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml");
+ TestHelper.writeInputToSystem(process.getErrorStream());
+ TestHelper.writeInputToOutput(process.getErrorStream(), process.getOutputStream());
+ process.waitFor();
+ if (process.exitValue() != 0) {
+ throw new RuntimeException("cargo build failed, exitcode: " + process.exitValue());
+ }
+
+ if(!execute) {
+ rsFilePaths.forEach(p -> p.toFile().delete());
+ return;
+ }
+
+ String progArgs = "";
+ if (modelChecking) { progArgs = " -- mixed 2 true"; }
+ if (noDead) { progArgs += " -nodead"; }
+ if (noInv) { progArgs += " -noinv"; }
+
+ Process executeProcess = runtime.exec("cargo run --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml" + progArgs);
+ executeProcess.waitFor();
+
+ String error = TestHelper.streamToString(executeProcess.getErrorStream());
+ if(executeProcess.exitValue() != 0) {
+ throw new RuntimeException(error);
+ }
+ String result = TestHelper.streamToString(executeProcess.getInputStream());
+ }
+}
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/ConstNestedRelation.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/ConstNestedRelation.mch
new file mode 100644
index 000000000..ff54c75a4
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/ConstNestedRelation.mch
@@ -0,0 +1,21 @@
+MACHINE ConstNestedRelation
+
+SETS
+ Counters={C1, C2, C3, C4, C5, C6}
+ ;Persons={P1, P2}
+
+CONCRETE_CONSTANTS
+ nxt
+
+PROPERTIES
+ nxt : Persons --> (Counters >+> Counters)
+ & nxt = {P1 |-> { C1 |-> C3, C3 |-> C5 }, P2 |-> {C2 |-> C6, C6 |-> C2}}
+
+INVARIANT /* Machine without Invariant crashes MC-generator (even if MC is disabled...) */
+ 1 = 1
+
+
+OPERATIONS
+
+ out <-- relCount = out := card(nxt)
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/ConstPowRelation.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/ConstPowRelation.mch
new file mode 100644
index 000000000..7c01e5617
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/ConstPowRelation.mch
@@ -0,0 +1,21 @@
+MACHINE ConstPowRelation
+
+SETS
+ Counters={C1, C2, C3}
+ ;Persons={P1, P2}
+
+CONCRETE_CONSTANTS
+ Counter2Person
+
+PROPERTIES
+ Counter2Person : POW(Counters <-> Persons)
+ & Counter2Person = {{(C1|->P1), (C3|->P2)}, {(C1|->P1), (C2|->P2)}}
+
+INVARIANT /* Machine without Invariant crashes MC-generator (even if MC is disabled...) */
+ 1 = 1
+
+
+OPERATIONS
+
+ out <-- relCount = out := card(Counter2Person)
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/ConstPowSet.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/ConstPowSet.mch
new file mode 100644
index 000000000..7392a8b96
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/ConstPowSet.mch
@@ -0,0 +1,20 @@
+MACHINE ConstPowSet
+
+SETS
+ Persons={P1, P2, P3}
+
+CONCRETE_CONSTANTS
+ Groups
+
+PROPERTIES
+ Groups <: POW(Persons)
+ & Groups = {{P1, P3}, {P2}}
+
+INVARIANT /* Machine without Invariant crashes MC-generater (even if MC is disabled...) */
+ 1 = 1
+
+
+OPERATIONS
+
+ out <-- groupsCount = out := card(Groups)
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/MaxPowEnumeratedSet.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/MaxPowEnumeratedSet.mch
new file mode 100644
index 000000000..78e0a054f
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/MaxPowEnumeratedSet.mch
@@ -0,0 +1,24 @@
+MACHINE MaxPowEnumeratedSet
+
+SETS
+ Counters={C1}
+
+VARIABLES
+ AvailableCounters
+
+INVARIANT
+ AvailableCounters : POW(POW(POW(POW(Counters))))
+
+INITIALISATION
+ AvailableCounters := {}
+
+OPERATIONS
+
+ AddCounter(c) =
+ PRE
+ /* @grd1 */ c <: POW(POW(Counters))
+ THEN
+ AvailableCounters := AvailableCounters \/ { c }
+ END
+
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/NestedRelation.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/NestedRelation.mch
new file mode 100644
index 000000000..56bb286d1
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/NestedRelation.mch
@@ -0,0 +1,31 @@
+MACHINE NestedRelation
+
+SETS
+ Counters={C1, C2}
+ ;Persons={P1, P2}
+ ;Shift={S1, S2}
+
+VARIABLES
+ Shift2Counter2Person
+
+INVARIANT
+ Shift2Counter2Person : Shift <-> (Counters <-> Persons)
+
+INITIALISATION
+ Shift2Counter2Person := {}
+
+OPERATIONS
+
+ ManCounter(c, p, s) =
+ PRE
+ /* @grd1 */ c : Counters
+ & /* @grd2 */ p : Persons
+ & s : Shift
+ & s : dom(Shift2Counter2Person) => (
+ c /: dom(Shift2Counter2Person(s))
+ & p /: ran(Shift2Counter2Person(s))
+ )
+ THEN
+ Shift2Counter2Person(s) := {(c |-> p)}
+ END
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/PowRelation.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/PowRelation.mch
new file mode 100644
index 000000000..7d2fee85e
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/PowRelation.mch
@@ -0,0 +1,26 @@
+MACHINE PowRelation
+
+SETS
+ Counters={C1, C2, C3}
+ ;Persons={P1, P2}
+
+VARIABLES
+ Counter2Person
+
+INVARIANT
+ Counter2Person : POW(Counters <-> Persons)
+
+INITIALISATION
+ Counter2Person := {}
+
+OPERATIONS
+
+ ManCounter(c, p) =
+ PRE
+ /* @grd1 */ c : Counters
+ & /* @grd2 */ p : Persons
+ & {(c |-> p)} /: Counter2Person
+ THEN
+ Counter2Person := Counter2Person \/ {{(c |-> p)}}
+ END
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/RedundantConstRelation.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/RedundantConstRelation.mch
new file mode 100644
index 000000000..dbd96cc36
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/RedundantConstRelation.mch
@@ -0,0 +1,21 @@
+MACHINE RedundantConstRelation
+
+SETS
+ Persons={P1, P2, P3}
+ ;Counters={C1, C2}
+
+CONCRETE_CONSTANTS
+ Counter2Persons
+
+PROPERTIES
+ Counter2Persons : Counters <-> Persons
+ & Counter2Persons = {(C1|->P1), (C2|->P3)}
+
+INVARIANT /* Machine without Invariant crashes MC-generator (even if MC is disabled...) */
+ 1 = 1
+
+
+OPERATIONS
+
+ out <-- relCount = out := card(Counter2Persons)
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/RedundantConstSet.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/RedundantConstSet.mch
new file mode 100644
index 000000000..4a42c0330
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/RedundantConstSet.mch
@@ -0,0 +1,20 @@
+MACHINE RedundantConstSet
+
+SETS
+ Persons={P1, P2, P3}
+
+CONCRETE_CONSTANTS
+ Managers
+
+PROPERTIES
+ Managers <: Persons
+ & Managers = {P1, P3}
+
+INVARIANT /* Machine without Invariant crashes MC-generator (even if MC is disabled...) */
+ 1 = 1
+
+
+OPERATIONS
+
+ out <-- workerCount = out := card(Persons - Managers)
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/SimpleEnumeratedSet.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/SimpleEnumeratedSet.mch
new file mode 100644
index 000000000..e51d430d6
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/SimpleEnumeratedSet.mch
@@ -0,0 +1,23 @@
+MACHINE SimpleEnumeratedSet
+
+SETS
+ Counters={C1, C2, C3}
+
+VARIABLES
+ AvailableCounters
+
+INVARIANT
+ AvailableCounters <: Counters
+
+INITIALISATION
+ AvailableCounters := {}
+
+OPERATIONS
+
+ AddCounter(c) =
+ PRE
+ /* @grd1 */ c : Counters
+ THEN
+ AvailableCounters := AvailableCounters \/ { c }
+ END
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/SimplePowEnumeratedSet.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/SimplePowEnumeratedSet.mch
new file mode 100644
index 000000000..5201c2cad
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/SimplePowEnumeratedSet.mch
@@ -0,0 +1,23 @@
+MACHINE SimplePowEnumeratedSet
+
+SETS
+ Counters={C1, C2, C3}
+
+VARIABLES
+ AvailableCounters
+
+INVARIANT
+ AvailableCounters <: POW(Counters)
+
+INITIALISATION
+ AvailableCounters := {}
+
+OPERATIONS
+
+ AddCounter(c) =
+ PRE
+ /* @grd1 */ c <: Counters
+ THEN
+ AvailableCounters := AvailableCounters \/ { c }
+ END
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/SimplePowPowEnumeratedSet.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/SimplePowPowEnumeratedSet.mch
new file mode 100644
index 000000000..6691df00a
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/SimplePowPowEnumeratedSet.mch
@@ -0,0 +1,23 @@
+MACHINE SimplePowPowEnumeratedSet
+
+SETS
+ Counters={C1, C2}
+
+VARIABLES
+ AvailableCounters
+
+INVARIANT
+ AvailableCounters <: POW(POW(Counters))
+
+INITIALISATION
+ AvailableCounters := {}
+
+OPERATIONS
+
+ AddCounter(c) =
+ PRE
+ /* @grd1 */ c <: POW(Counters)
+ THEN
+ AvailableCounters := AvailableCounters \/ { c }
+ END
+END
diff --git a/src/test/resources/de/hhu/stups/codegenerator/embedded/SimpleRelation.mch b/src/test/resources/de/hhu/stups/codegenerator/embedded/SimpleRelation.mch
new file mode 100644
index 000000000..fd9a21ee4
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/embedded/SimpleRelation.mch
@@ -0,0 +1,27 @@
+MACHINE SimpleRelation
+
+SETS
+ Counters={C1, C2, C3}
+ ;Persons={P1, P2}
+
+VARIABLES
+ Counter2Person
+
+INVARIANT
+ Counter2Person : Counters <-> Persons
+
+INITIALISATION
+ Counter2Person := {}
+
+OPERATIONS
+
+ ManCounter(c, p) =
+ PRE
+ /* @grd1 */ c : Counters
+ & /* @grd2 */ p : Persons
+ & c /: dom(Counter2Person)
+ & p /: ran(Counter2Person)
+ THEN
+ Counter2Person(c) := p
+ END
+END
--
GitLab