Official LSV Web Site
Experiments
- All examples
- The following table shows the time and memory needed for FAST to compute the reachability set of several protocols, using a forward algorithm and a basic strategy. Note that computing the whole reachability set is really harder than just checking on-the-fly if a configuration is reachable using a backward algorithm. Some tools are restricted to the second method, while FAST can perform both. Even if benchmarks for the backward algorithm are not complete (it takes time!!), experimentations show better results using backward algorithm.
Results using an Intel Pentium 933 Mhz with 512 Mbytes :
| Case study |  |
 |
 |
 |
 |
 |
 |
 |
| Bounded Petri Nets | ||||||||
| Producer/Consumer | 5 | 3 | 0.41 | 2.37 | 7 | 3 | 1 | 3 |
| Lamport ME | 11 | 9 | 2.70 | 2.88 | 5 | 11 | 1 | 9 |
| Dekker ME | 22 | 22 | 21.72 | 5.48 | 5 | 36 | 1 | 22 |
| RTP | 9 | 12 | 2.24 | 2.76 | 5 | 8 | 1 | 12 |
| Peterson ME | 14 | 12 | 4.97 | 3.78 | 5 | 12 | 1 | 12 |
| Reader/Writer | 13 | 9 | 9.68 | 23.14 | 9 | 23 | 1 | 9 |
| Petri Nets | ||||||||
| CSM - N | 13 | 13 | 45.57 | 6.31 | 6 | 32 | 2 | 35 |
| FMS | 22 | 20 | 157.48 | 8.02 | 21 | 23 | 2 | 46 |
| Multipoll | 17 | 20 | 22.96 | 5.13 | 35 | 13 | 1 | 20 |
| Kanban | 16 | 16 | 10.43 | 6.54 | 4 | 2 | 1 | 16 |
| Mesh2x2 | 32 | 32 | ≥ 1800 | - | - | - | - | - |
| Mesh3x2 | 52 | 54 | ≥ 1800 | - | - | - | - | - |
| Manufacturing system | 7 | 6 | ≥ 1800 | - | - | - | - | - |
| Manufacturing system (check deadlock freedom) | 13 | 6 | ≥ 1800 | - | - | - | - | - |
| PNCSA | 31 | 38 | ≥ 1800 | - | - | - | - | - |
| extended ReaderWriter | 24 | 22 | ≥ 1800 | - | - | - | - | - |
| SWIMMING POOL | 9 | 6 | 111 | 29.06 | 30 | 9 | 4 | 47 |
| Petri Nets with Transfer Arcs | ||||||||
| Last-in First-served | 17 | 10 | 1.89 | 2.74 | 9 | 12 | 1 | 10 |
| Esparza-Finkel-Mayr | 6 | 5 | 0.79 | 2.55 | 5 | 2 | 1 | 5 |
| Broadcast Protocols | ||||||||
| Inc/Dec | 32 | 28 | ≥ 1800 | - | - | - | - | - |
| Producer/Consumer with Java threads - 2 | 18 | 14 | 13.27 | 3.81 | 13 | 53 | 1 | 14 |
| Producer/Consumer with Java threads - N | 18 | 14 | 723.27 | 12.46 | 58 | 86 | 2 | 75 |
| 2-Producer/2-Consumer with Java threads | 44 | 38 | ≥ 1800 | - | - | - | - | - |
| Central Server system | 13 | 8 | 20.82 | 6.83 | 5 | 11 | 2 | 25 |
| Consistency Protocol | 12 | 8 | 275 | 7.35 | 7 | 9 | 3 | 98 |
| M.E.S.I. Cache Coherence Protocol | 4 | 4 | 0.42 | 2.44 | 6 | 3 | 1 | 4 |
| M.O.E.S.I. Cache Coherence Protocol | 4 | 5 | 0.56 | 2.49 | 7 | 3 | 1 | 5 |
| Synapse Cache Coherence Protocol | 3 | 3 | 0.30 | 2.23 | 6 | 2 | 1 | 3 |
| Illinois Cache Coherence Protocol | 4 | 6 | 0.97 | 2.64 | 6 | 4 | 1 | 6 |
| Berkeley Cache Coherence Protocol | 4 | 3 | 0.49 | 2.75 | 7 | 2 | 1 | 3 |
| Firefly Cache Coherence Protocol | 4 | 8 | 0.86 | 2.59 | 7 | 3 | 1 | 8 |
| Dragon Cache Coherence Protocol | 5 | 8 | 1.42 | 2.72 | 6 | 5 | 1 | 8 |
| Futurebus+ Cache Coherence Protocol | 9 | 10 | 2.19 | 3.38 | 12 | 8 | 1 | 10 |
| Others | ||||||||
| lift controller - N | 4 | 5 | 4.56 | 2.90 | 14 | 4 | 3 | 20 |
| bakery4 | 8 | 20 | ≥ 1800 | - | - | - | - | - |
| barber4 | 8 | 12 | 1.92 | 2.68 | 5 | 8 | 1 | 12 |
| ticket 2i | 6 | 6 | 0.88 | 2.54 | 22 | 5 | 1 | 6 |
| ticket 3i | 8 | 9 | 3.77 | 3.08 | 77 | 10 | 1 | 9 |
| TTP | 10 | 17 | 1186.24 | 73.24 | 1140 | 31 | 1 | 17 |
| TTP (ad hoc strategy) | 10 | 17 | 246.67 | 72.87 | 1140 | 16 | 1 | 17 |
Results using an Intel Pentium 933 Mhz with 512 Mbytes