Graded-CTL NuSMV
Test Results for "ABP8"
|
A≤k1 G (A≤k2 F (sender.state = get) ∧ A≤k3 F (receiver.state = deliver))
|
| k1 | k2 | k3 | Time | #BDD |
|---|
| - | - | - | 3,804 | 1743784 |
| 0 | 0 | 0 | 3,804 | 1743794 |
| 1 | 0 | 0 | 3,908 | 1750268 |
| 2 | 0 | 0 | 3,912 | 1750268 |
| 5 | 0 | 0 | 3,916 | 1750268 |
| 10 | 0 | 0 | 3,952 | 1750268 |
| 0 | 1 | 1 | 3,912 | 1750268 |
| 1 | 1 | 1 | 3,916 | 1750268 |
| 5 | 1 | 1 | 3,920 | 1750268 |
| 10 | 1 | 1 | 3,944 | 1750268 |
| 0 | 3 | 1 | 3,932 | 1750268 |
| 1 | 3 | 1 | 3,936 | 1750268 |
| 5 | 3 | 1 | 3,948 | 1750268 |
| 10 | 3 | 1 | 3,952 | 1750268 |
| 0 | 5 | 1 | 3,916 | 1750268 |
| 1 | 5 | 1 | 3,920 | 1750268 |
| 10 | 5 | 1 | 3,928 | 1750268 |
| 0 | 1 | 3 | 3,924 | 1750268 |
| 1 | 1 | 3 | 3,928 | 1750268 |
| 10 | 1 | 3 | 3,944 | 1750268 |
| 0 | 3 | 3 | 3,932 | 1750268 |
| 1 | 3 | 3 | 3,936 | 1750268 |
| 10 | 3 | 3 | 3,948 | 1750268 |
| 0 | 5 | 3 | 3,932 | 1750268 |
| 1 | 5 | 3 | 3,940 | 1750268 |
| 10 | 5 | 3 | 3,948 | 1750268 |
| 10 | 10 | 10 | 3,948 | 1750268 |
| 50 | 50 | 50 | 8,956 | 1750268 |
|
E>k1 G (E>k2 F (sender.state = get) ∧ E>k3 F (receiver.state = deliver))
|
| k1 | k2 | k3 | Time | #BDD |
|---|
| - | - | - | 3,052 | 1616154 |
| 0 | 0 | 0 | 3,296 | 1616164 |
| 1 | 0 | 0 | 5,316 | 679676 |
| 2 | 0 | 0 | 6,808 | 1541032 |
| 5 | 0 | 0 | 11,765 | 845117 |
| 10 | 0 | 0 | 22,321 | 845117 |
| 0 | 1 | 1 | 8,237 | 1345388 |
| 1 | 1 | 1 | 10,253 | 679137 |
| 5 | 1 | 1 | 17,177 | 845117 |
| 10 | 1 | 1 | 27,142 | 845117 |
| 0 | 3 | 1 | 11,929 | 1296220 |
| 1 | 3 | 1 | 13,957 | 679137 |
| 5 | 3 | 1 | 20,481 | 845117 |
| 10 | 3 | 1 | 31,722 | 845117 |
| 0 | 5 | 1 | 15,273 | 1320804 |
| 1 | 5 | 1 | 17,385 | 679137 |
| 10 | 5 | 1 | 34,058 | 845117 |
| 0 | 1 | 3 | 11,725 | 1345400 |
| 1 | 1 | 3 | 13,717 | 679137 |
| 10 | 1 | 3 | 30,718 | 845117 |
| 0 | 3 | 3 | 14,737 | 1658777 |
| 1 | 3 | 3 | 16,677 | 1026555 |
| 10 | 3 | 3 | 32,950 | 845117 |
| 0 | 5 | 3 | 18,141 | 1316462 |
| 1 | 5 | 3 | 20,145 | 679137 |
| 10 | 5 | 3 | 37,318 | 845117 |
| 10 | 10 | 10 | 61,120 | 845117 |
| 50 | 50 | 50 | 310,011 | 845117 |