model gb {

var l, t, x;

states ell,hen;

transition t1 := {
 from   := ell;
 to     := ell;
 guard  := x<=9;
 action := l'=l+1,x'=x+1,t'=t+1;
};

transition t2 := {
 from   := ell;
 to     := hen;
 guard  := true;
 action := x'=0;
};

transition t3 := {
 from   := hen;
 to     := hen;
 guard  := true;
 action := t'=t+1, x'=x+1;
};

transition t4 := {
 from   := hen;
 to     := ell;
 guard  := x>=50;
 action := x'=0;
};


}

strategy s1 {

Region init := {state=ell && t=0 && l=0 && x=0};

//Transitions ttt := {t1,t2,t3,t4};
//Region reach := post*(init, ttt,3);

Region bad := {6l>t+50};
}