// 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" ]