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 |