mdp
const int N=2;
const int K;
const int range = 2*(K+1)*N;
const int counter_init = (K+1)*N;
const int left = N;
const int right= 2*(K+1)*N -N;
global counter : [0..range] init counter_init;
module process1
pc1 : [0..3];
coin1 : [0..1];
[] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
[] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0);
[] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0);
[] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0);
[] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1);
[] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0);
[done] (pc1=3) -> (pc1'=3);
endmodule
module process2 = process1[pc1=pc2,coin1=coin2] endmodule