const int k;

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

// Stable states - where only one process has a token
label "stable" = num_tokens=1;

// A stable state is reached with probability 1
"init" => P>=1 [ F "stable" ]

// Maximum expected time to reach a stable state (for all configurations)
R=? [ F "stable" {"init"}{max} ]

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

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