// stable states - where only one process has the same value as the process to its left label "stable" = num_tokens=1; // from the initial state, a stable state is reached with probability 1 "init" => P>=1 [ F "stable" ]