const int k;

// states with k tokens
label "k_tokens" = num_tokens=k;

// stable states - where only one process has the same value as the process to its left
label "stable" = num_tokens=1;

// maximum expected time to reach a stable state (for all k-token configurations)
R=? [ F "stable" {"k_tokens"}{max} ]