You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
18 lines
450 B
18 lines
450 B
// Theorem 1 (mutual exclusion)
|
|
|
|
num_crit <= 1
|
|
|
|
// Lemma C
|
|
// If the crical section is occupied then eventually it becomes clear
|
|
|
|
num_crit > 0 => P>=1 [ F num_crit = 0 ]
|
|
|
|
// Lemma D
|
|
// If a process is between 4 and 13 (in our version) then eventually some process gets to 14
|
|
|
|
"some_4_13" => P>=1 [ F "some_14" ]
|
|
|
|
// Theorem 2 (liveness)
|
|
// If process 1 tries then eventually it enters the critical section
|
|
|
|
p1=1 => P>=1 [ F p1=10 ]
|