// liveness property (eventually a process is made the leader)
"init" => P>=1[ true U (s=9) ]