const int k; // number of tokens
const int K; // number of steps

// labels
label "k_tokens" = num_tokens=k; // configurations with k tokens

// From any initial configuration, a stable configuration is reached with probability 1
P>=1 [ F "stable" ]

// The token is passed around fairly with probability 1 (for process 1)
P>=1 [ G F q1=1 ]

// Minimum probability a stable state is reached within K
Pmin=? [ F<=K "stable" {"init"}{min} ]

// Maximum expected number of tokens at step K
R{"tokens"}max=? [ I=K {"init"}{max} ]

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