From 9f8184852f6b17745c0431006fc7964f6eb2f234 Mon Sep 17 00:00:00 2001
From: Cookiebowser <lucas.doering@live.de>
Date: Mon, 29 Aug 2022 14:09:52 +0200
Subject: [PATCH] filled MC benchmark table more and fixed some rust issues
---
benchmarks/model_checking/README.md | 116 +++++++++---------
.../hhu/stups/codegenerator/RustTemplate.stg | 20 +--
.../stups/codegenerator/rust/TestOthers.java | 25 ++++
.../hhu/stups/codegenerator/rust/TestRS.java | 13 +-
.../hhu/stups/codegenerator/StringLaws_MC.out | 3 +
.../hhu/stups/codegenerator/SubsetLaws_MC.out | 3 +
.../codegenerator/SubstitutionLaws_MC.out | 3 +
.../stups/codegenerator/TautologiesPL_MC.out | 3 +
.../de/hhu/stups/codegenerator/tictac_MC.out | 3 +
9 files changed, 118 insertions(+), 71 deletions(-)
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/StringLaws_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/SubsetLaws_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/TautologiesPL_MC.out
create mode 100644 src/test/resources/de/hhu/stups/codegenerator/tictac_MC.out
diff --git a/benchmarks/model_checking/README.md b/benchmarks/model_checking/README.md
index 4161725bf..d18c1b628 100644
--- a/benchmarks/model_checking/README.md
+++ b/benchmarks/model_checking/README.md
@@ -60,35 +60,35 @@ Executing benchmarks is done by executing ``make`` in each of the directories.
#### System B
-| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust |
-|-------------------|----------|---------|---------|------------------------|---------|-----------------------|-----------------------|
-| Lift_MC_Large | Runtime | | | 2.23 / 2.7 | | 0.74 / 00.96 | 00.42 / 00.50 |
-| | Speed-up | | | | | | |
-| | Memory | | | 700.824 / 721.548 | | 250.388 / 250.405 | 54.734 / 54.742 |
-| Cruise Controller | Runtime | | | 1.73 / 2.28 | | 0.11 / 00.12 | 00.07 / 00.18 |
-| | Speed-up | | | | | | |
-| | Memory | | | 159.292 / 161.860 | | 6.310 / 6.489 | 5011 / 5226 |
-| Landing Gear | Runtime | | | 11.16 / 13.52 | | 8.79 / 9.59 | 09.84 / 19.23 |
-| | Speed-up | | | | | | |
-| | Memory | | | 1.063.784 / 1.352.408 | | 329.672 / 332.976 | 734.749 / 854.914 |
-| CAN BUS | Runtime | | | 3.79 / 4.47 | | 1.71 / 2.02 | 02.3 / 02.45 |
-| | Speed-up | | | | | | |
-| | Memory | | | 542.680 / 1.080.708 | | 316.873 / 326.791 | 1.012.179 / 1.049.515 |
-| Train1_Lukas | Runtime | | | 13.0 / 12.25 | | 4.93 / 2.31 | 07.08 / 07.14 |
-| | Speed-up | | | | | | |
-| | Memory | | | 701.600 / 1.044.600 | | 59.299 / 62.798 | 187.201 / 255.626 |
-| Train_1_beebook | Runtime | | | 626.39 / 545.66 | | 311.83 / 135.69 | 445.79 / 416.89 |
-| | Speed-up | | | | | | |
-| | Memory | | | 1.451.340 / 3.110.416 | | 1.559.626 / 1.667.335 | 4.735.570 / 6.047.158 |
-| nota | Runtime | | | 10.75 / 9.58 | | 22.43 / 21.4 | 20.12 / 20.77 |
-| | Speed-up | | | | | | |
-| | Memory | | | 1.201.656 / 1.512.316 | | 280.518 / 413.597 | 1.321.891 / 1.269.008 |
-| sort_1000 | Runtime | | | 988.25 / 85.87 | | 1424.95 / 1251.89 | 516 / 95.12 |
-| | Speed-up | | | | | | |
-| | Memory | | | 1.202.264 / 1.361.680 | | 338.626 / 342.083 | 269.996 / 269.939 |
-| N Queens (N=4) | Runtime | | | 34.41 / 35.73 | | 27.79 / 27.16 | 22.34 / 22.74 |
-| | Speed-up | | | | | | |
-| | Memory | | | 511.568 / 503.032 | | 61.762 / 61.814 | 345.376 / 345.386 |
+| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust |
+|-------------------|----------|---------|---------|------------------------|-----------------------|-----------------------|-----------------------|
+| Lift_MC_Large | Runtime | | | 2.23 / 2.7 | 0.80 / 0.97 | 0.74 / 00.96 | 00.42 / 00.50 |
+| | Speed-up | | | | | | |
+| | Memory | | | 700.824 / 721.548 | 250.488 / 250.524 | 250.388 / 250.405 | 54.734 / 54.742 |
+| Cruise Controller | Runtime | | | 1.73 / 2.28 | 0.14 / 0.14 | 0.11 / 00.12 | 00.07 / 00.18 |
+| | Speed-up | | | | | | |
+| | Memory | | | 159.292 / 161.860 | 6.296 / 6.580 | 6.310 / 6.489 | 5011 / 5226 |
+| Landing Gear | Runtime | | | 11.16 / 13.52 | 10.95 / 10.58 | 8.79 / 9.59 | 09.84 / 19.23 |
+| | Speed-up | | | | | | |
+| | Memory | | | 1.063.784 / 1.352.408 | 329.680 / 333.076 | 329.672 / 332.976 | 734.749 / 854.914 |
+| CAN BUS | Runtime | | | 3.79 / 4.47 | 1.99 / 2.1 | 1.71 / 2.02 | 02.3 / 02.45 |
+| | Speed-up | | | | | | |
+| | Memory | | | 542.680 / 1.080.708 | 316.888 / 326.688 | 316.873 / 326.791 | 1.012.179 / 1.049.515 |
+| Train1_Lukas | Runtime | | | 13.0 / 12.25 | 5.29 / 2.39 | 4.93 / 2.31 | 07.08 / 07.14 |
+| | Speed-up | | | | | | |
+| | Memory | | | 701.600 / 1.044.600 | 59.408 / 62.912 | 59.299 / 62.798 | 187.201 / 255.626 |
+| Train_1_beebook | Runtime | | | 626.39 / 545.66 | 338.03 / 140.84 | 311.83 / 135.69 | 445.79 / 416.89 |
+| | Speed-up | | | | | | |
+| | Memory | | | 1.451.340 / 3.110.416 | 1.559.736 / 1.667.508 | 1.559.626 / 1.667.335 | 4.735.570 / 6.047.158 |
+| nota | Runtime | | | 10.75 / 9.58 | 26.55 / 23.1 | 22.43 / 21.4 | 20.12 / 20.77 |
+| | Speed-up | | | | | | |
+| | Memory | | | 1.201.656 / 1.512.316 | 280.532 / 413.696 | 280.518 / 413.597 | 1.321.891 / 1.269.008 |
+| sort_1000 | Runtime | | | 988.25 / 85.87 | 1650.41 / 1317.36 | 1424.95 / 1251.89 | 516 / 95.12 |
+| | Speed-up | | | | | | |
+| | Memory | | | 1.202.264 / 1.361.680 | 338.680 / 342.100 | 338.626 / 342.083 | 269.996 / 269.939 |
+| N Queens (N=4) | Runtime | | | 34.41 / 35.73 | 28.81 / 32.6 | 27.79 / 27.16 | 22.34 / 22.74 |
+| | Speed-up | | | | | | |
+| | Memory | | | 511.568 / 503.032 | 61.684 / 61.980 | 61.762 / 61.814 | 345.376 / 345.386 |
### Multi-threaded (6 Threads)
@@ -140,35 +140,35 @@ Current implementation requires an additional coordinator thread.
#### System B
-| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust |
-|-------------------|----------|---------|---------|-----------------------|---------|-----------------------|-----------------------|
-| Lift_MC_Large | Runtime | | | 67.14 / 67.37 | | 64.37 / 61.59 | 09.82 / 09.96 |
-| | Speed-up | | | | | | |
-| | Memory | | | 548.128 / 522.388 | | 250.822 / 250.832 | 38.637 / 38.590 |
-| Cruise Controller | Runtime | | | 1.76 / 1.78 | | 0.05 / 00.06 | 00.04 / 00.06 |
-| | Speed-up | | | | | | |
-| | Memory | | | 171.916 / 180.132 | | 6.697 / 7.018 | 6.978 / 6.959 |
-| Landing Gear | Runtime | | | 6.42 / 6.69 | | 7.03 / 6.76 | 03.41 / 04.56 |
-| | Speed-up | | | | | | |
-| | Memory | | | 1.405.280 / 2.043.336 | | 341.353 / 345.930 | 727.461 / 847.765 |
-| CAN BUS | Runtime | | | 3.52 / 4.29 | | 4.12 / 4.35 | 01.64 / 01.64 |
-| | Speed-up | | | | | | |
-| | Memory | | | 550.004 / 1.159.472 | | 317.437 / 326.536 | 1.047.918 / 1.050.520 |
-| Train1_Lukas | Runtime | | | 5.96 / 5.44 | | 4.36 / 1.91 | 01.61 / 01.46 |
-| | Speed-up | | | | | |
-| | Memory | | | 1.468.360 / 1.772.524 | | 60.320 / 64.956 | 189.500 / 250.548 |
-| Train_1_beebook | Runtime | | | 174.56 / 147.29 | | 250.92 / 111.71 | 89.65 / 76.61 |
-| | Speed-up | | | | | | |
-| | Memory | | | 2.555.344 / 3.094.376 | | 1.572.735 / 1.814.287 | 4.998.943 / 5.484.696 |
-| nota | Runtime | | | 5.12 / 4.74 | | 26.12 / 21.58 | 05.02 / 05.24 |
-| | Speed-up | | | | | | |
-| | Memory | | | 2.185.468 / 2.464.928 | | 299.167 / 433.206 | 1.390.200 / 1.369.317 |
-| sort_1000 | Runtime | | | 208.82 / 37.32 | | 336.3 / 273.14 | 110.91 / 27.47 |
-| | Speed-up | | | | | | |
-| | Memory | | | 2.359.820 / 2.420.428 | | 323.596 / 341.784 | 243.784 / 243.330 |
-| N Queens (N=4) | Runtime | | | 32.87 / 32.2 | | 30.88 / 25.98 | 21.34 / 22.46 |
-| | Speed-up | | | | | | |
-| | Memory | | | 508.736 / 499.924 | | 62.630 / 62.742 | 345.888 / 345.855 |
+| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust |
+|-------------------|----------|---------|---------|-----------------------|-----------------------|-----------------------|-----------------------|
+| Lift_MC_Large | Runtime | | | 67.14 / 67.37 | 63.33 / 64.33 | 64.37 / 61.59 | 09.82 / 09.96 |
+| | Speed-up | | | | | | |
+| | Memory | | | 548.128 / 522.388 | 250.840 / 250.926 | 250.822 / 250.832 | 38.637 / 38.590 |
+| Cruise Controller | Runtime | | | 1.76 / 1.78 | 0.06 / 0.06 | 0.05 / 00.06 | 00.04 / 00.06 |
+| | Speed-up | | | | | | |
+| | Memory | | | 171.916 / 180.132 | 6.544 / 7.112 | 6.697 / 7.018 | 6.978 / 6.959 |
+| Landing Gear | Runtime | | | 6.42 / 6.69 | 7.28 / 7.59 | 7.03 / 6.76 | 03.41 / 04.56 |
+| | Speed-up | | | | | | |
+| | Memory | | | 1.405.280 / 2.043.336 | 340.408 / 345.720 | 341.353 / 345.930 | 727.461 / 847.765 |
+| CAN BUS | Runtime | | | 3.52 / 4.29 | 3.92 / 4.51 | 4.12 / 4.35 | 01.64 / 01.64 |
+| | Speed-up | | | | | | |
+| | Memory | | | 550.004 / 1.159.472 | 317.140 / 326.652 | 317.437 / 326.536 | 1.047.918 / 1.050.520 |
+| Train1_Lukas | Runtime | | | 5.96 / 5.44 | 4.46 / 2.02 | 4.36 / 1.91 | 01.61 / 01.46 |
+| | Speed-up | | | | | |
+| | Memory | | | 1.468.360 / 1.772.524 | 60.412 / 65.012 | 60.320 / 64.956 | 189.500 / 250.548 |
+| Train_1_beebook | Runtime | | | 174.56 / 147.29 | 257.59 / 115.41 | 250.92 / 111.71 | 89.65 / 76.61 |
+| | Speed-up | | | | | | |
+| | Memory | | | 2.555.344 / 3.094.376 | 1.573.868 / 1.812.972 | 1.572.735 / 1.814.287 | 4.998.943 / 5.484.696 |
+| nota | Runtime | | | 5.12 / 4.74 | 25.91 / 25.63 | 26.12 / 21.58 | 05.02 / 05.24 |
+| | Speed-up | | | | | | |
+| | Memory | | | 2.185.468 / 2.464.928 | 300.208 / 438.692 | 299.167 / 433.206 | 1.390.200 / 1.369.317 |
+| sort_1000 | Runtime | | | 208.82 / 37.32 | 327.81 / 279.46 | 336.3 / 273.14 | 110.91 / 27.47 |
+| | Speed-up | | | | | | |
+| | Memory | | | 2.359.820 / 2.420.428 | 323.472 / 341.740 | 323.596 / 341.784 | 243.784 / 243.330 |
+| N Queens (N=4) | Runtime | | | 32.87 / 32.2 | 30.02 / 28.66 | 30.88 / 25.98 | 21.34 / 22.46 |
+| | Speed-up | | | | | | |
+| | Memory | | | 508.736 / 499.924 | 62696 / 62.832 | 62.630 / 62.742 | 345.888 / 345.855 |
diff --git a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
index a2416fcad..23d2c09e9 100644
--- a/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+++ b/src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
@@ -88,20 +88,22 @@ fn main() {
};
let mut no_dead = false;
+ let mut no_inv = false;
if args.len() > 4 {
for arg in args.iter().skip(4) {
match arg.as_str() {
"-nodead" => no_dead = true,
+ "-noinv" => no_inv = true,
_ => {}
}
}
}
if threads == 1 {
- <machine>::model_check_single_threaded(mc_type, is_caching, no_dead);
+ <machine>::model_check_single_threaded(mc_type, is_caching, no_dead, no_inv);
} else {
- <machine>::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead);
+ <machine>::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
}
}
<endif>
@@ -428,7 +430,7 @@ if_expression_predicate(predicate, ifThen, ifElse) ::= <<
>>
set_enumeration(leftType, type, rightType, enums, isRelation) ::= <<
-/*set_enum <leftType>*/<if(isRelation)>BRelation<if(!enums)>::\<<if(!leftType)>Dummy, Dummy<else><leftType>, <rightType><endif>\><endif><else>BSet<if(!enums)>::\<<if(!type)>Dummy<else><type><endif>\><endif><endif>::new(vec![<if(isRelation)><enums; separator=", "><else><enums:{e | <e>.clone()}; separator=", "><endif>])
+<if(isRelation)>BRelation<if(!enums)>::\<<if(!leftType)>Dummy, Dummy<else><leftType>, <rightType><endif>\><endif><else>BSet<if(!enums)>::\<<if(!type)>Dummy<else><type><endif>\><endif><endif>::new(vec![<if(isRelation)><enums; separator=", "><else><enums:{e | <e>.clone()}; separator=", "><endif>])
>>
seq_enumeration(type, elements) ::= <<
@@ -916,7 +918,7 @@ fn get_invariant_dependencies(op: &'static str) -> Vec\<&str> {
}
}
-fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool) {
+fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool, no_inv: bool) {
let mut machine = <machine>::new();
let mut all_states = HashSet::\<<machine>\>::new();
@@ -934,7 +936,7 @@ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool
let next_states = Self::generateNextStates(&mut state, is_caching, Arc::clone(&num_transitions));
- if !Self::checkInvariants(&state, last_op, is_caching) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
println!("INVARIANT VIOLATED");
stop_threads = true;
}
@@ -956,7 +958,7 @@ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool
Self::print_result(all_states.len(), num_transitions.load(Ordering::Acquire), stop_threads);
}
-fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool) {
+fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, no_dead: bool, no_inv: bool) {
let threadPool = ThreadPool::new(threads);
let machine = <machine>::new();
@@ -992,7 +994,7 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, n
.filter(|(next_state, _)| states.insert((*next_state).clone()))
.for_each(|(next_state, last_op)| states_to_process.lock().unwrap().push_back((next_state, last_op)));
- if !Self::checkInvariants(&state, last_op, is_caching) {
+ if !no_inv && !Self::checkInvariants(&state, last_op, is_caching) {
let _ = tx.send(Err("INVARIANT VIOLATED"));
}
//println!("Thread {:?} done", thread::current().id());
@@ -1039,10 +1041,10 @@ pre_assert(isModelChecking, isTopLevel, iterationConstruct, predicate, then) ::=
//pre_assert
<if(isModelChecking && !isTopLevel)>
<iterationConstruct; separator="\n">
-if((<predicate>).booleanValue()) {
+if (<predicate>).booleanValue() {
<then>
} else {
- throw new PreconditionOrAssertionViolation("Precondition or Assertion Error occured.");
+ panic!("Precondition or Assertion Error occurred.");
}
<else>
<then>
diff --git a/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java b/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
index c2ebe2102..927930325 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
+++ b/src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
@@ -98,4 +98,29 @@ public class TestOthers extends TestRS{
public void test_SetLawsPowPowCart() throws Exception {
testRSMC("SetLawsPowPowCart", PROB_OTHER_PATH, false);
}
+
+ @Test
+ public void test_StringLaws() throws Exception {
+ testRSMC("StringLaws", PROB_OTHER_PATH, true);
+ }
+
+ @Test
+ public void test_SubsetLaws() throws Exception {
+ testRSMC("SubsetLaws", PROB_OTHER_PATH, true, true);
+ }
+
+ @Test //cnt:INT test takes to long, since it creates the max integer intervall (could probably be optimized)
+ public void test_SubstitutionLaws() throws Exception {
+ testRSMC("SubstitutionLaws", PROB_OTHER_PATH, false);
+ }
+
+ @Test
+ public void test_TautologiesPL() throws Exception {
+ testRSMC("TautologiesPL", PROB_OTHER_PATH, true);
+ }
+
+ @Test
+ public void test_tictac() throws Exception {
+ testRSMC("tictac", PROB_OTHER_PATH, true, true, true);
+ }
}
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 a21b97cac..2abe2ab17 100644
--- a/src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java
+++ b/src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java
@@ -37,11 +37,11 @@ public class TestRS {
}
public void testRS(String machine) throws Exception {
- testRS(machine, machine, "DefaultAddition.strs", false);
+ testRS(machine, null, "DefaultAddition.strs", false);
}
public void testRS(String machine, String machineName, String addition, boolean execute) throws Exception {
- testRS(machine, machineName, addition, execute, false, false);
+ testRS(machine, machineName, addition, execute, false, false, false);
}
public void testRSMC(String machine) throws Exception {
@@ -57,10 +57,14 @@ public class TestRS {
}
public void testRSMC(String machine, String machinePath, boolean execute, boolean noDead) throws Exception {
- testRS(machine, machinePath, null, execute, true, noDead);
+ testRSMC(machine, machinePath, execute, noDead, false);
}
- public void testRS(String machine, String machinePath, String addition, boolean execute, boolean modelChecking, boolean noDead) throws Exception {
+ public void testRSMC(String machine, String machinePath, boolean execute, boolean noDead, boolean noInv) throws Exception {
+ testRS(machine, machinePath, null, execute, true, noDead, noInv);
+ }
+
+ public void testRS(String machine, String machinePath, String addition, boolean execute, boolean modelChecking, boolean noDead, boolean noInv) throws Exception {
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();
@@ -110,6 +114,7 @@ public class TestRS {
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();
diff --git a/src/test/resources/de/hhu/stups/codegenerator/StringLaws_MC.out b/src/test/resources/de/hhu/stups/codegenerator/StringLaws_MC.out
new file mode 100644
index 000000000..35dcb70d3
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/StringLaws_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 64
+Number of Transitions: 768
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/SubsetLaws_MC.out b/src/test/resources/de/hhu/stups/codegenerator/SubsetLaws_MC.out
new file mode 100644
index 000000000..7cc013a4b
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/SubsetLaws_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 373248
+Number of Transitions: 3172608
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws_MC.out b/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws_MC.out
new file mode 100644
index 000000000..4c6a42f0f
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 3
+Number of Transitions: 18
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/TautologiesPL_MC.out b/src/test/resources/de/hhu/stups/codegenerator/TautologiesPL_MC.out
new file mode 100644
index 000000000..e6a403318
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/TautologiesPL_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 8
+Number of Transitions: 64
\ No newline at end of file
diff --git a/src/test/resources/de/hhu/stups/codegenerator/tictac_MC.out b/src/test/resources/de/hhu/stups/codegenerator/tictac_MC.out
new file mode 100644
index 000000000..e7997f32b
--- /dev/null
+++ b/src/test/resources/de/hhu/stups/codegenerator/tictac_MC.out
@@ -0,0 +1,3 @@
+MODEL CHECKING SUCCESSFUL
+Number of States: 6046
+Number of Transitions: 19107
\ No newline at end of file
--
GitLab