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

// labels
label "k_tokens" = num_tokens=k; // configurations with k tokens
label "stable" = num_tokens=1;   // stable configurations (1 token)

// From any configuration, a stable configuration is reached with probability 1
filter(forall, "init" => P>=1 [ F "stable" ])

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

// Maximum/minimum expected time to reach a stable configuration (for all k-token configurations)
Rmax=? [ F "stable" {"k_tokens"}{max} ]
Rmin=? [ F "stable" {"k_tokens"}{min} ]

// Minimum probability reached a stable configuration within K steps (for all configurations)
Pmin=? [ F<=K "stable" {"init"}{min} ]