Graded-CTL NuSMV
Test Results for "SyncArb5"
E>k X e2.Token
|
k | Time | #BDD |
- | 0,000 | 1236 |
0 | 0,000 | 1236 |
1 | 0,000 | 1579 |
2 | 0,000 | 1581 |
3 | 0,000 | 1582 |
5 | 0,000 | 1585 |
8 | 0,000 | 1588 |
10 | 0,000 | 1589 |
15 | 0,000 | 1589 |
20 | 0,000 | 1594 |
50 | 0,000 | 1588 |
E>k (!e2.Token) U e2.Token
|
k | Time | #BDD |
- | 0,000 | 1255 |
0 | 0,000 | 1255 |
1 | 0,000 | 1765 |
2 | 0,000 | 1830 |
3 | 0,000 | 1831 |
5 | 0,000 | 1838 |
8 | 0,000 | 1850 |
10 | 0,000 | 1852 |
15 | 0,000 | 1857 |
20 | 0,000 | 1830 |
50 | 0,000 | 1938 |
A≤k1 X A≤k2 F (e1.ack-out ∧ e-1.Persistent)
|
k1 | k2 | Time | #BDD |
- | - | 0,000 | 1321 |
0 | 0 | 0,000 | 1321 |
1 | 0 | 0,000 | 1893 |
2 | 0 | 0,000 | 1912 |
5 | 0 | 0,000 | 1945 |
10 | 0 | 0,000 | 1983 |
0 | 1 | 0,000 | 1951 |
1 | 1 | 0,000 | 1951 |
2 | 1 | 0,000 | 2040 |
5 | 1 | 0,000 | 2073 |
10 | 1 | 0,000 | 2111 |
0 | 2 | 0,000 | 1993 |
1 | 2 | 0,000 | 2060 |
2 | 2 | 0,000 | 1993 |
5 | 2 | 0,000 | 2115 |
10 | 2 | 0,000 | 2153 |
0 | 5 | 0,000 | 2099 |
1 | 5 | 0,000 | 2166 |
2 | 5 | 0,000 | 2182 |
5 | 5 | 0,000 | 2099 |
10 | 5 | 0,000 | 2226 |
0 | 10 | 0,000 | 2262 |
1 | 10 | 0,000 | 2329 |
2 | 10 | 0,000 | 2345 |
5 | 10 | 0,000 | 2344 |
10 | 10 | 0,000 | 2262 |
50 | 10 | 0,000 | 2374 |
50 | 50 | 0,004 | 3401 |