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
715 B
19 lines
715 B
const int k;
|
|
|
|
// States with k tokens - where only k processes have the same value as the process to its left
|
|
label "k_tokens" = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x1?1:0) = k;
|
|
|
|
// Stable states - where only one process has a token
|
|
label "stable" = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x1?1:0) = 1;
|
|
|
|
// A stable state is reached with probability 1
|
|
"init" => P>=1 [ true U "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} ]
|