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

filled MC benchmark table more and fixed some rust issues

parent e2676ecb
Branches
Tags
1 merge request!28Rust support
Show whitespace changes
Inline Side-by-side
Showing
with 118 additions and 71 deletions
benchmarks/model_checking/README.md
+ 58
− 58
View file @ 9f818485
...@@ -61,34 +61,34 @@ Executing benchmarks is done by executing ``make`` in each of the directories. ...@@ -61,34 +61,34 @@ Executing benchmarks is done by executing ``make`` in each of the directories.
#### System B #### System B
| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust | | 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 | | Lift_MC_Large | Runtime | | | 2.23 / 2.7 | 0.80 / 0.97 | 0.74 / 00.96 | 00.42 / 00.50 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 700.824 / 721.548 | | 250.388 / 250.405 | 54.734 / 54.742 | | | 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.11 / 00.12 | 00.07 / 00.18 | | Cruise Controller | Runtime | | | 1.73 / 2.28 | 0.14 / 0.14 | 0.11 / 00.12 | 00.07 / 00.18 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 159.292 / 161.860 | | 6.310 / 6.489 | 5011 / 5226 | | | Memory | | | 159.292 / 161.860 | 6.296 / 6.580 | 6.310 / 6.489 | 5011 / 5226 |
| Landing Gear | Runtime | | | 11.16 / 13.52 | | 8.79 / 9.59 | 09.84 / 19.23 | | Landing Gear | Runtime | | | 11.16 / 13.52 | 10.95 / 10.58 | 8.79 / 9.59 | 09.84 / 19.23 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 1.063.784 / 1.352.408 | | 329.672 / 332.976 | 734.749 / 854.914 | | | 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.71 / 2.02 | 02.3 / 02.45 | | CAN BUS | Runtime | | | 3.79 / 4.47 | 1.99 / 2.1 | 1.71 / 2.02 | 02.3 / 02.45 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 542.680 / 1.080.708 | | 316.873 / 326.791 | 1.012.179 / 1.049.515 | | | 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 | | 4.93 / 2.31 | 07.08 / 07.14 | | Train1_Lukas | Runtime | | | 13.0 / 12.25 | 5.29 / 2.39 | 4.93 / 2.31 | 07.08 / 07.14 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 701.600 / 1.044.600 | | 59.299 / 62.798 | 187.201 / 255.626 | | | 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 | | 311.83 / 135.69 | 445.79 / 416.89 | | Train_1_beebook | Runtime | | | 626.39 / 545.66 | 338.03 / 140.84 | 311.83 / 135.69 | 445.79 / 416.89 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 1.451.340 / 3.110.416 | | 1.559.626 / 1.667.335 | 4.735.570 / 6.047.158 | | | 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 | | 22.43 / 21.4 | 20.12 / 20.77 | | nota | Runtime | | | 10.75 / 9.58 | 26.55 / 23.1 | 22.43 / 21.4 | 20.12 / 20.77 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 1.201.656 / 1.512.316 | | 280.518 / 413.597 | 1.321.891 / 1.269.008 | | | 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 | | 1424.95 / 1251.89 | 516 / 95.12 | | sort_1000 | Runtime | | | 988.25 / 85.87 | 1650.41 / 1317.36 | 1424.95 / 1251.89 | 516 / 95.12 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 1.202.264 / 1.361.680 | | 338.626 / 342.083 | 269.996 / 269.939 | | | 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 | | 27.79 / 27.16 | 22.34 / 22.74 | | N Queens (N=4) | Runtime | | | 34.41 / 35.73 | 28.81 / 32.6 | 27.79 / 27.16 | 22.34 / 22.74 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 511.568 / 503.032 | | 61.762 / 61.814 | 345.376 / 345.386 | | | Memory | | | 511.568 / 503.032 | 61.684 / 61.980 | 61.762 / 61.814 | 345.376 / 345.386 |
### Multi-threaded (6 Threads) ### Multi-threaded (6 Threads)
...@@ -141,34 +141,34 @@ Current implementation requires an additional coordinator thread. ...@@ -141,34 +141,34 @@ Current implementation requires an additional coordinator thread.
#### System B #### System B
| Machines | | ProB OP | ProB ST | Java | C++ -O1 | C++ -O2 | Rust | | 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 | | Lift_MC_Large | Runtime | | | 67.14 / 67.37 | 63.33 / 64.33 | 64.37 / 61.59 | 09.82 / 09.96 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 548.128 / 522.388 | | 250.822 / 250.832 | 38.637 / 38.590 | | | 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.05 / 00.06 | 00.04 / 00.06 | | Cruise Controller | Runtime | | | 1.76 / 1.78 | 0.06 / 0.06 | 0.05 / 00.06 | 00.04 / 00.06 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 171.916 / 180.132 | | 6.697 / 7.018 | 6.978 / 6.959 | | | 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.03 / 6.76 | 03.41 / 04.56 | | Landing Gear | Runtime | | | 6.42 / 6.69 | 7.28 / 7.59 | 7.03 / 6.76 | 03.41 / 04.56 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 1.405.280 / 2.043.336 | | 341.353 / 345.930 | 727.461 / 847.765 | | | 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 | | 4.12 / 4.35 | 01.64 / 01.64 | | CAN BUS | Runtime | | | 3.52 / 4.29 | 3.92 / 4.51 | 4.12 / 4.35 | 01.64 / 01.64 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 550.004 / 1.159.472 | | 317.437 / 326.536 | 1.047.918 / 1.050.520 | | | 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.36 / 1.91 | 01.61 / 01.46 | | Train1_Lukas | Runtime | | | 5.96 / 5.44 | 4.46 / 2.02 | 4.36 / 1.91 | 01.61 / 01.46 |
| | Speed-up | | | | | | | | Speed-up | | | | | |
| | Memory | | | 1.468.360 / 1.772.524 | | 60.320 / 64.956 | 189.500 / 250.548 | | | 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 | | 250.92 / 111.71 | 89.65 / 76.61 | | Train_1_beebook | Runtime | | | 174.56 / 147.29 | 257.59 / 115.41 | 250.92 / 111.71 | 89.65 / 76.61 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 2.555.344 / 3.094.376 | | 1.572.735 / 1.814.287 | 4.998.943 / 5.484.696 | | | 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 | | 26.12 / 21.58 | 05.02 / 05.24 | | nota | Runtime | | | 5.12 / 4.74 | 25.91 / 25.63 | 26.12 / 21.58 | 05.02 / 05.24 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 2.185.468 / 2.464.928 | | 299.167 / 433.206 | 1.390.200 / 1.369.317 | | | 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 | | 336.3 / 273.14 | 110.91 / 27.47 | | sort_1000 | Runtime | | | 208.82 / 37.32 | 327.81 / 279.46 | 336.3 / 273.14 | 110.91 / 27.47 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 2.359.820 / 2.420.428 | | 323.596 / 341.784 | 243.784 / 243.330 | | | 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.88 / 25.98 | 21.34 / 22.46 | | N Queens (N=4) | Runtime | | | 32.87 / 32.2 | 30.02 / 28.66 | 30.88 / 25.98 | 21.34 / 22.46 |
| | Speed-up | | | | | | | | | Speed-up | | | | | | |
| | Memory | | | 508.736 / 499.924 | | 62.630 / 62.742 | 345.888 / 345.855 | | | Memory | | | 508.736 / 499.924 | 62696 / 62.832 | 62.630 / 62.742 | 345.888 / 345.855 |
......
src/main/resources/de/hhu/stups/codegenerator/RustTemplate.stg
+ 11
− 9
View file @ 9f818485
...@@ -88,20 +88,22 @@ fn main() { ...@@ -88,20 +88,22 @@ fn main() {
}; };
let mut no_dead = false; let mut no_dead = false;
let mut no_inv = false;
if args.len() > 4 { if args.len() > 4 {
for arg in args.iter().skip(4) { for arg in args.iter().skip(4) {
match arg.as_str() { match arg.as_str() {
"-nodead" => no_dead = true, "-nodead" => no_dead = true,
"-noinv" => no_inv = true,
_ => {} _ => {}
} }
} }
} }
if threads == 1 { 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 { } else {
<machine>::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead); <machine>::modelCheckMultiThreaded(mc_type, threads, is_caching, no_dead, no_inv);
} }
} }
<endif> <endif>
...@@ -428,7 +430,7 @@ if_expression_predicate(predicate, ifThen, ifElse) ::= << ...@@ -428,7 +430,7 @@ if_expression_predicate(predicate, ifThen, ifElse) ::= <<
>> >>
set_enumeration(leftType, type, rightType, enums, isRelation) ::= << 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) ::= << seq_enumeration(type, elements) ::= <<
...@@ -916,7 +918,7 @@ fn get_invariant_dependencies(op: &'static str) -> Vec\<&str> { ...@@ -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 machine = <machine>::new();
let mut all_states = HashSet::\<<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 ...@@ -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)); 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"); println!("INVARIANT VIOLATED");
stop_threads = true; stop_threads = true;
} }
...@@ -956,7 +958,7 @@ fn model_check_single_threaded(mc_type: MC_TYPE, is_caching: bool, no_dead: bool ...@@ -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); 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 threadPool = ThreadPool::new(threads);
let machine = <machine>::new(); let machine = <machine>::new();
...@@ -992,7 +994,7 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, n ...@@ -992,7 +994,7 @@ fn modelCheckMultiThreaded(mc_type: MC_TYPE, threads: usize, is_caching: bool, n
.filter(|(next_state, _)| states.insert((*next_state).clone())) .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))); .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")); let _ = tx.send(Err("INVARIANT VIOLATED"));
} }
//println!("Thread {:?} done", thread::current().id()); //println!("Thread {:?} done", thread::current().id());
...@@ -1039,10 +1041,10 @@ pre_assert(isModelChecking, isTopLevel, iterationConstruct, predicate, then) ::= ...@@ -1039,10 +1041,10 @@ pre_assert(isModelChecking, isTopLevel, iterationConstruct, predicate, then) ::=
//pre_assert //pre_assert
<if(isModelChecking && !isTopLevel)> <if(isModelChecking && !isTopLevel)>
<iterationConstruct; separator="\n"> <iterationConstruct; separator="\n">
if((<predicate>).booleanValue()) { if (<predicate>).booleanValue() {
<then> <then>
} else { } else {
throw new PreconditionOrAssertionViolation("Precondition or Assertion Error occured."); panic!("Precondition or Assertion Error occurred.");
} }
<else> <else>
<then> <then>
......
src/test/java/de/hhu/stups/codegenerator/rust/TestOthers.java
+ 25
− 0
View file @ 9f818485
...@@ -98,4 +98,29 @@ public class TestOthers extends TestRS{ ...@@ -98,4 +98,29 @@ public class TestOthers extends TestRS{
public void test_SetLawsPowPowCart() throws Exception { public void test_SetLawsPowPowCart() throws Exception {
testRSMC("SetLawsPowPowCart", PROB_OTHER_PATH, false); 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);
}
} }
src/test/java/de/hhu/stups/codegenerator/rust/TestRS.java
+ 9
− 4
View file @ 9f818485
...@@ -37,11 +37,11 @@ public class TestRS { ...@@ -37,11 +37,11 @@ public class TestRS {
} }
public void testRS(String machine) throws Exception { 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 { 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 { public void testRSMC(String machine) throws Exception {
...@@ -57,10 +57,14 @@ public class TestRS { ...@@ -57,10 +57,14 @@ public class TestRS {
} }
public void testRSMC(String machine, String machinePath, boolean execute, boolean noDead) throws Exception { 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 == 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();
...@@ -110,6 +114,7 @@ public class TestRS { ...@@ -110,6 +114,7 @@ public class TestRS {
String progArgs = ""; String progArgs = "";
if (modelChecking) { progArgs = " -- mixed 2 true"; } if (modelChecking) { progArgs = " -- mixed 2 true"; }
if (noDead) { progArgs += " -nodead"; } 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); Process executeProcess = runtime.exec("cargo run --release --manifest-path " + mainPath.getParent().getParent().toFile().getAbsolutePath() + "/Cargo.toml" + progArgs);
executeProcess.waitFor(); executeProcess.waitFor();
......
src/test/resources/de/hhu/stups/codegenerator/StringLaws_MC.out 0 → 100644
+ 3
− 0
View file @ 9f818485
MODEL CHECKING SUCCESSFUL
Number of States: 64
Number of Transitions: 768
\ No newline at end of file
src/test/resources/de/hhu/stups/codegenerator/SubsetLaws_MC.out 0 → 100644
+ 3
− 0
View file @ 9f818485
MODEL CHECKING SUCCESSFUL
Number of States: 373248
Number of Transitions: 3172608
\ No newline at end of file
src/test/resources/de/hhu/stups/codegenerator/SubstitutionLaws_MC.out 0 → 100644
+ 3
− 0
View file @ 9f818485
MODEL CHECKING SUCCESSFUL
Number of States: 3
Number of Transitions: 18
\ No newline at end of file
src/test/resources/de/hhu/stups/codegenerator/TautologiesPL_MC.out 0 → 100644
+ 3
− 0
View file @ 9f818485
MODEL CHECKING SUCCESSFUL
Number of States: 8
Number of Transitions: 64
\ No newline at end of file
src/test/resources/de/hhu/stups/codegenerator/tictac_MC.out 0 → 100644
+ 3
− 0
View file @ 9f818485
MODEL CHECKING SUCCESSFUL
Number of States: 6046
Number of Transitions: 19107
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment