Graded-CTL NuSMV
Test Results for "Dekker"
A≤k G !((pr1.state=critical) ∧ (pr2.state=critical))
|
k | Time | #BDD |
- | 0,000 | 2169 |
0 | 0,000 | 2169 |
1 | 0,000 | 2339 |
2 | 0,000 | 2340 |
3 | 0,000 | 2341 |
5 | 0,000 | 2343 |
8 | 0,000 | 2346 |
10 | 0,000 | 2348 |
15 | 0,000 | 2353 |
20 | 0,000 | 2358 |
50 | 0,000 | 2388 |
A≤k1 G ((pr1.state=test_bj) ⇒ (A ≤k2 F (pr1.state=critical))
|
k1 | k2 | Time | #BDD |
- | - | 0,004 | 3940 |
0 | 0 | 0,004 | 3940 |
1 | 0 | 0,004 | 4110 |
2 | 0 | 0,004 | 4111 |
5 | 0 | 0,004 | 4114 |
10 | 0 | 0,004 | 4119 |
0 | 1 | 0,004 | 4110 |
1 | 1 | 0,004 | 4110 |
2 | 1 | 0,004 | 4111 |
5 | 1 | 0,004 | 4114 |
10 | 1 | 0,004 | 4119 |
0 | 2 | 0,004 | 4111 |
1 | 2 | 0,004 | 4111 |
2 | 2 | 0,004 | 4111 |
5 | 2 | 0,004 | 4114 |
10 | 2 | 0,004 | 4119 |
0 | 5 | 0,004 | 4114 |
1 | 5 | 0,004 | 4114 |
2 | 5 | 0,004 | 4114 |
5 | 5 | 0,004 | 4114 |
10 | 5 | 0,004 | 4119 |
0 | 10 | 0,004 | 4119 |
1 | 10 | 0,004 | 4119 |
2 | 10 | 0,004 | 4119 |
5 | 10 | 0,004 | 4119 |
10 | 10 | 0,004 | 4119 |
50 | 10 | 0,008 | 4159 |
50 | 50 | 0,008 | 4159 |