Skip to content
Snippets Groups Projects
Commit ef1b03db authored by Cookiebowser's avatar Cookiebowser
Browse files

added generator tests for Sets/Relations in embedded mode

parent fa3aec31
No related branches found
No related tags found
No related merge requests found
Showing
with 625 additions and 41 deletions
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);
}
}
...@@ -2,6 +2,7 @@ package de.hhu.stups.codegenerator.rust; ...@@ -2,6 +2,7 @@ package de.hhu.stups.codegenerator.rust;
import de.hhu.stups.codegenerator.CodeGenerator; import de.hhu.stups.codegenerator.CodeGenerator;
import de.hhu.stups.codegenerator.GeneratorMode; import de.hhu.stups.codegenerator.GeneratorMode;
import de.hhu.stups.codegenerator.TestHelper;
import java.io.*; import java.io.*;
import java.nio.file.Files; import java.nio.file.Files;
...@@ -15,27 +16,6 @@ import static org.junit.Assert.assertEquals; ...@@ -15,27 +16,6 @@ import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertTrue; import static org.junit.Assert.assertTrue;
public class TestRS { 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 { public void testRS(String machine) throws Exception {
testRS(machine, null, "DefaultAddition.strs", false); testRS(machine, null, "DefaultAddition.strs", false);
} }
...@@ -68,21 +48,7 @@ public class TestRS { ...@@ -68,21 +48,7 @@ public class TestRS {
if (machinePath == null) { machinePath = "../../../resources/test/de/hhu/stups/codegenerator/"; } if (machinePath == null) { machinePath = "../../../resources/test/de/hhu/stups/codegenerator/"; }
if (!machinePath.endsWith("/")) { machinePath += "/"; } if (!machinePath.endsWith("/")) { machinePath += "/"; }
Path mchPath = Paths.get(CodeGenerator.class.getClassLoader().getResource("").toURI()).resolve(machinePath + machine + ".mch").normalize(); Path mchPath = Paths.get(CodeGenerator.class.getClassLoader().getResource("").toURI()).resolve(machinePath + machine + ".mch").normalize();
CodeGenerator codeGenerator = new CodeGenerator(); List<Path> rsFilePaths = TestHelper.generateCode(mchPath, GeneratorMode.RS, modelChecking, addition, false);
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);
Path typesPath = Paths.get(this.getClass().getClassLoader().getResource("./").toURI()).getParent().getParent().getParent().getParent().resolve(Paths.get("btypes_primitives/src/main/rust/bmachine/src")); 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); Files.createDirectories(typesPath);
...@@ -99,8 +65,8 @@ public class TestRS { ...@@ -99,8 +65,8 @@ public class TestRS {
File newMainFile = typesPath.resolve(Paths.get("main.rs")).toFile(); File newMainFile = typesPath.resolve(Paths.get("main.rs")).toFile();
mainPath.toFile().renameTo(newMainFile); mainPath.toFile().renameTo(newMainFile);
Process process = runtime.exec("cargo build --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml"); Process process = runtime.exec("cargo build --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml");
writeInputToSystem(process.getErrorStream()); TestHelper.writeInputToSystem(process.getErrorStream());
writeInputToOutput(process.getErrorStream(), process.getOutputStream()); TestHelper.writeInputToOutput(process.getErrorStream(), process.getOutputStream());
process.waitFor(); process.waitFor();
if (process.exitValue() != 0) { if (process.exitValue() != 0) {
throw new Exception("cargo build failed, exitcode: " + process.exitValue()); throw new Exception("cargo build failed, exitcode: " + process.exitValue());
...@@ -119,15 +85,15 @@ public class TestRS { ...@@ -119,15 +85,15 @@ public class TestRS {
Process executeProcess = runtime.exec("cargo run --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml" + progArgs); Process executeProcess = runtime.exec("cargo run --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml" + progArgs);
executeProcess.waitFor(); executeProcess.waitFor();
String error = streamToString(executeProcess.getErrorStream()); String error = TestHelper.streamToString(executeProcess.getErrorStream());
if(executeProcess.exitValue() != 0) { if(executeProcess.exitValue() != 0) {
throw new RuntimeException(error); throw new RuntimeException(error);
} }
String result = streamToString(executeProcess.getInputStream()); String result = TestHelper.streamToString(executeProcess.getInputStream());
if (modelChecking && !machine.contains("MC")) machine += "_MC"; if (modelChecking && !machine.contains("MC")) machine += "_MC";
File outFile = Paths.get(CodeGenerator.class.getClassLoader().getResource("de/hhu/stups/codegenerator/" + machine + ".out").toURI()).toFile(); 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", ""); result = result.replaceAll("\n", "");
if (!modelChecking) { if (!modelChecking) {
......
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());
}
}
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());
}
}
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
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
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
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
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
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
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
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
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
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
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
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
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment