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.
5 lines
256 B
5 lines
256 B
// Mutual exclusion: at any time t there is at most one process in its critical section phase
|
|
num_procs_in_crit <= 1
|
|
|
|
// Liveness: if a process is trying, then eventually a process enters the critical section
|
|
"one_trying" => P>=1 [ F "one_critical" ]
|