model consprodjava {

var initc, whilec, whileget, waitget, competec, notifyc, endc, initp, whilep, whileput, waitput, competep, notifyp, returnp, available, lock;

states normal;

transition r1 := {
from := normal;
to := normal;
guard := initc>=1;
action := initc'=initc-1, whilec'=whilec+1;
};

transition r2 := {
from := normal;
to := normal;
guard := whilec>=1 && lock=0; 
action := whilec'=whilec-1, whileget'=whileget+1, lock'=1;
};

transition r3 := {
from := normal;
to := normal;
guard := whileget>=1 && available=0 && lock=1;
action := whileget'=whileget-1, waitget'=waitget+1, lock'=0;
};

transition r4 := {
from := normal;
to := normal;
guard := competec>=1 && lock=0; 
action := competec'=competec-1, whileget'=whileget+1, lock'=1;
};

transition r5 := {
from := normal;
to := normal;
guard := whileget>=1 && available=1;
action := whileget'=whileget-1, notifyc'=notifyc+1 , available'=0;
};

transition r6 := {
from := normal;
to := normal;
guard := notifyc>=1;
action := notifyc'=notifyc-1, endc'=endc+1, competec'=competec+waitget , waitget'=0, competep'=competep+waitput , waitput'=0;
};

transition r7 := {
from := normal;
to := normal;
guard := endc>=1 && lock=1;
action := endc'=endc-1, whilec'=whilec+1, lock'=0;
};

transition r8 := {
from := normal;
to := normal;
guard := initp>=1;
action := initp' =initp-1, whilep'=whilep+1;
};

transition r9 := {
from := normal;
to := normal;
guard := whilep>=1 && lock=0 ;
action := whilep'=whilep-1, whileput'=whileput+1, lock'=1;
};

transition r10 := {
from := normal;
to := normal;
guard := whileput>=1 && lock=1 && available=1;
action := whileput'=whileput-1, waitput'=waitput+1, lock'=0;
};

transition r11 := {
from := normal;
to := normal;
guard := competep>=1 && lock=0; 
action := competep'=competep-1, whileput'=whileput+1, lock'=1;
};

transition r12 := {
from := normal;
to := normal;
guard := whileput>=1 && available=0; 
action := whileput'=whileput-1, notifyp'=notifyp+1, available'=1;
};

transition r13 := {
from := normal;
to := normal;
guard := notifyp>=1;
action := notifyp'=notifyp-1, returnp'=returnp+1, competec'=competec+waitget , waitget'=0, competep'=competep+waitput , waitput'=0;
};

transition r14 := {
from := normal;
to := normal;
guard := returnp>=1 && lock=1;
action := returnp'=returnp-1, whilep'=whilep+1, lock'=0;
};

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

Region init := {initc>=0 && state=normal && whilec=0 && whileget=0 && waitget=0 && competec=0 && notifyc=0 && endc=0 && initp-initc=0 && whilep=0 && whileput=0 && waitput=0 && competep=0 && notifyp=0 && returnp=0 && available=0 && lock=0};
Transitions t := {r1,r2,r3,r4,r5,r6,r7,r8,r9,r10,r11,r12,r13,r14};

Region reach := post*(init, t,2);

}