model lift {


var a,c,g,N;

states e0;

transition r1 := {
	from :=e0;
	to:=e0;
	guard :=
		c=g && g>1
	;
	action :=
		g'=g-1
	;
};


transition r2 := {
	from :=e0;
	to:=e0;
	guard :=
	c=g && g<N
	;
action :=
	g'=g+1
	;
};




transition r3 :=  {
	from :=e0;
	to:=e0;
	guard :=
	c>g && a=1
	;
	action :=
	a'=0
	;
};

transition r4  := {
	from :=e0;
	to:=e0;
	guard :=
		c<g && a=1
	;
	action :=
		a'= 2
	;
};

transition r5  :={
	from :=e0;
	to:=e0;
	guard :=
		!a=1
	;
action :=
	c'=c+a-1,
	a'=1
	;
};

}


strategy s1 {

setMaxState(0);
setMaxAcc(100);


Region init :=
	{state=e0 && c=0 && g=0 && a=1 && N>=0};

Transitions t := {r1,r2,r3,r4,r5};

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

	
}