Exemples en Promela/Spin
C-1 : Introduction
Linear Search
C-2 : Proprietes et semantique des programmes concurrents
Lancement de processus
Lancement de processus incorrect
Affectations sans interference
Affectations avec interférence (
cours
,
TD-2, exo1
)
Semaphore
(TD-2, exo-5)
C-3 : Sections critiques
Solution simple mais fausse
Solution simple
et
sa formule LTL
Solution non-primitive avec lock
Solution primitive avec lock par Test-And-Set
et
sa formule
Solution de Peterson non-primitive, binaire
Solution de Peterson primitive, binaire
Solution de Peterson primitive, n-aire
et
sa formule LTS