Introduction
We report here how difficult models where for tools in general. Pleas find below the signification of icons.
: no tool could process any
instance of the model of this model for this examination.
: less than 33% of the
tools could process at least one instance of this model for this examination.
: 33-66% of the tools could
process at least one instance of this model for this examination.
: 66% or more tools
could process at least one instance of this model for this examination.
In the tables below, the first line of the header show the class of the verified formulas while the second one shows the type of atomic proposition formulas may contain: cardinality comparisonw, fireability, marking comparison, place comparison and a mix of these. For reachability formulas, we also refer to the presence of at least one deadlock. The last columns refer to state space generation.
Report for “Known” Models
| CTL | LTL | Reachability | |||||||||||||||
| model | Card. Comp. | Fire- ability | Marking Comp. | Mix | Place Comp. | Card. Comp. | Fire- ability | Mark. Comp. | Mix | Place Comp. | Card. Comp. | Deadlock | Fire- ability | Marking Comp. | Mix | Place Comp. | State Space |
| CSRepetitions (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| CSRepetitions (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Dekker (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| DotAndBoxes (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| DrinkVendingMachine (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| DrinkVendingMachine (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Echo (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Eratosthenes (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| FMS (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| GlobalRessAlloc (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| GlobalRessAlloc (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Kanban (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| LamportFastMutEx (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| LamportFastMutEx (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| MAPK (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| NeoElection (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| NeoElection (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| PermAdmissibility (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| PermAdmissibility (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Peterson (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Peterson (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Philosophers (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Philosophers (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| PhilosophersDyn (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| PhilosophersDyn (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Planning (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Railroad (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| RessAllocation (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Ring (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| RwMutex (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| SharedMemory (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| SharedMemory (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| SimpleLoadBal (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| SimpleLoadBal (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| TokenRing (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| TokenRing (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Report for “Surprise” Models
| CTL | LTL | Reachability | |||||||||||||||
| model | Card. Comp. | Fire- ability | Marking Comp. | Mix | Place Comp. | Card. Comp. | Fire- ability | Mark. Comp. | Mix | Place Comp. | Card. Comp. | Deadlock | Fire- ability | Marking Comp. | Mix | Place Comp. | State Space |
| HouseConstruction (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| IBMB2S565S3960 (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| QuasiCertifProtocol (colored) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| QuasiCertifProtocol (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| Vasy2003 (P/T) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|