model PRODUCER_CONSUMMER {

var   i,b,a,o1,o2;

states normal;

transition r1 := {
from := normal;
to := normal;
guard := i>=1;
action :=	b'=b+1, i'=i-1;
};
  	      
transition r2 := {
from := normal;
to := normal;
guard := b>=1;
action := o1'=o1+1, b'=b-1;
};

transition r3 := {
from := normal;
to := normal;
guard := b>=1;
action := o2'=o2+1, b'=b-1;
};

}



strategy s1 {

setMaxState(0);
setMaxAcc(100);

Region init := {o1=0 && state=normal && b=0 && o2=0 && a>=0 && a-i=0};
Transitions t := {r1,r2,r3};

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

}