// Mutual exclusion
num_procs_in_crit <= 1

// Liveness: If a process is trying, then eventually a process enters the critical section
"one_trying" => P>=1 [ true U "one_critical" ]