model voiture {

var t, s, d;

states one,two,three,four;

transition t1 := {
 from   := one;
 to     := one;
 guard  := s<=1 && d<=8;
 action := s'=s+1,d'=d+1;
};

transition t2 := {
 from   := one;
 to     := one;
 guard  := t<=2;
 action := s'=0, t'=t+1;
};

transition t3 := {
 from   := one;
 to     := two;
 guard  := d>=9;
 action := s'=s+1, d'=d+1;
};

transition t4 := {
 from   := one;
 to     := three;
 guard  := s>=2;
 action := s'=s+1, d'=d+1;
};

transition t5 := {
 from   := one;
 to     := four;
 guard  := t>=3;
 action := t'=t+1, d'=d+1;
};

}

strategy s1 {

Region init := {state=one && t=0 && s=0 && d=0};

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


Region bad := {state=two};
}