model voituresimple {//cf sas 06

var t, s, d;

states one;

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

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

}

strategy s1 {

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


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


//Region bad := {state=two};
}