Expand, Enlarge and CheckVerification Group -- Université Libre de Bruxelles |
Lamport | |||
#Places:11 | #Transitions:9 | [Download] | |
The mutual exclusion protocol by Leslie Lamport, with two threads. |
newDekker | |||
#Places:16 | #Transitions:14 | [Download] | |
The Dekker mutual exclusion protocol, with two threads |
newRTP | |||
#Places:9 | #Transitions:12 | [Download] | |
A very basic communication protocol |
Peterson | |||
#Places:14 | #Transitions:12 | [Download] | |
The Peterson mutual exclusion protocol, with two threads |
Read-Write | |||
#Places:13 | #Transitions:9 | [Download] | |
A simple "reader/writer" mutual exclusion example. |
basicME | |||
#Places:5 | #Transitions:4 | [Download] | |
A basic mutual exclusion protocol, with an unbound number of threads. The Petri net can be found as Fig. 1 of Giorgio Delzanno, Jean-François Raskin an Laurent Van Begin, Attacking Symbolic State Explosion, in Proc. CAV'01, LNCS 2102. [Download this paper] |
CSM | |||
#Places:14 | #Transitions:13 | [Download] | |
This example describes a concurrent production system. It is taken from Fig. 76 of M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis, Modelling with generalized stochastic Petri nets, John Wiley Series in Parallel Computing - Chichester, 1995. [Petri net] |
FMS | |||
#Places:22 | #Transitions:20 | [Download] | |
A concurrent production system. [Petri net] |
Kanban | |||
#Places:16 | #Transitions:16 | [Download] | |
A concurrent production system. [Petri net] |
Mesh2x2 | |||
#Places:32 | #Transitions:32 | [Download] | |
This example describes a system in which a set of processors share the execution of various processes. It is taken from Fig. 130 of M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis, Modelling with generalized stochastic Petri nets, John Wiley Series in Parallel Computing - Chichester, 1995. [Petri net] |
Mesh3x2 | |||
#Places:52 | #Transitions:54 | [Download] | |
This example is an extension of the former one. |
Multipoll | |||
#Places:18 | #Transitions:21 | [Download] | |
This example comes from Andrew S. Miner and Gianfranco Ciardo, Efficient Reachability Set Generation and Storage Using Decision Diagrams, in Proc. ICATPN'99, LNCS 1639. It describes a concurrent production system. [Petri net] |
PNCSAcover | |||
#Places:31 | #Transitions:36 | [Download] | |
This is the PNCSA protocol as described in example 4.7 of Alain Finkel, The minimal coverability graph for Petri nets, Proc. APN'93, LNCS 674 |
CSMBroad | |||
#Places:13 | #Transitions:8 | [Download] | |
The Control Server Monitor. A consistency protocol with atomic syncronization actions. [Image] |
MOESI | |||
#Places:9 | #Transitions:11 | [Download] | |
A cache coherency protocol. |
German | |||
#Places:12 | #Transitions:8 | [Download] | |
Steve German's cache coherency protocol. |
Java | |||
#Places:44 | #Transitions:37 | [Download] | |
The counting abstraction of a Consumer/Producer multithread Java program, with two different kinds of consumers and producers. Buggy. [Java source code] |
Javasanserreur | |||
#Places:44 | #Transitions:38 | [Download] | |
The counting abstraction of a Consumer/Producer multithread Java program. Same as the previous example but without the bug. [Java source code] |
ConsProd | |||
#Places:18 | #Transitions:14 | [Download] | |
The counting abstraction of a Consumer/Producer multithreaded Java Program, taken from the [Sun tutorial]. |
ConsProd2 | |||
#Places:18 | #Transitions:14 | [Download] | |
Same as the former example, with another property. |
DelegateBuffer | |||
#Places:50 | #Transitions:52 | [Download] | |
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000 |
ExempleLea | |||
#Places:48 | #Transitions:42 | [Download] | |
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000 |
LeaBasicApproach | |||
#Places:16 | #Transitions:12 | [Download] | |
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000 |
QueuedBusyFlag | |||
#Places:80 | #Transitions:104 | [Download] | |
An example of counting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000 |
SimpleJavaExample | |||
#Places:32 | #Transitions:28 | [Download] | |
An example of Java program where two threads share an object describing a point in 2-dimensional space, and increment or decrement its coordinates. [Java source code] |
TransThesis | |||
#Places:90 | #Transitions:117 | [Download] | |
An example of conting abstraction of a Java program from Doug Lea, Concurrent Programming in Java (TM): Design, Principles and Patterns, second edition, Adison Wesley, 2000 |
EFM | |||
#Places:6 | #Transitions:5 | [Download] | |
The Esparza-Finkel-Mayr counter machine. Can be found at Fig. 2 of Javier Esparza, Alain Finkel, Richard Mayr, On the verification of broadcast protocols, in Proc. LICS'99. IEEE Computer Society, 352--359. |