Graded-CTL NuSMV
Test Results for "P_Queue"
| A≤k F (a1[1].out = 0) | ||
|---|---|---|
| k | Time | #BDD |
| - | 0,020 | 33717 |
| 0 | 0,020 | 33866 |
| 1 | 0,024 | 40459 |
| 2 | 0,024 | 40459 |
| 3 | 0,024 | 40459 |
| 5 | 0,024 | 40459 |
| 8 | 0,024 | 40460 |
| 10 | 0,024 | 40462 |
| 15 | 0,024 | 40467 |
| 20 | 0,028 | 40472 |
| 50 | 0,028 | 40502 |
| E>k G (out_1[1] = 0) | ||
|---|---|---|
| k | Time | #BDD |
| - | 0,024 | 33717 |
| 0 | 0,024 | 33866 |
| 1 | 0,040 | 71583 |
| 2 | 0,056 | 113117 |
| 3 | 0,072 | 128719 |
| 5 | 0,096 | 191680 |
| 8 | 0,096 | 197982 |
| 10 | 0,100 | 200801 |
| 15 | 0,116 | 208121 |
| 20 | 0,120 | 215927 |
| 50 | 0,172 | 260058 |