You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
19 lines
689 B
19 lines
689 B
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 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)
|
|
R=? [ F "stable" {"init"}{max} ]
|
|
|
|
// Maximum/minimum expected time to reach a stable configuration (for all k-token configurations)
|
|
R=? [ F "stable" {"k_tokens"}{max} ]
|
|
R=? [ F "stable" {"k_tokens"}{min} ]
|
|
|
|
// Minimum probability reached a stable configuration within K steps (for all configurations)
|
|
P=? [ F<=K "stable" {"init"}{min} ]
|
|
|