model subway {

var b, s, d;

states ontime, late, onbrake, stopped;

transition t2 := {
 from   := ontime;
 to     := ontime;
 guard  := b>s-9;
 action := s'=s+1;
};

transition t3 := {
 from   := ontime;
 to     := onbrake;
 guard  := b=s+9;
 action := b'=b+1, d'=0;
};

transition t4 := {
 from   := onbrake;
 to     := ontime;
 guard  := b=s+1;
 action := s'=s+1, d'=0;
};

transition t5 := {
 from   := late;
 to     := ontime;
 guard  := b=s-1;
 action := b'=b+1;
};

transition t6 := {
 from   := ontime;
 to     := late;
 guard  := b=s-9;
 action := s'=s+1;
};

transition t7 := {
 from   := late;
 to     := late;
 guard  := b<s-1;
 action := b'=b+1;
};

transition t8 := {
 from   := onbrake;
 to     := stopped;
 guard  := d=9;
 action := b'=b+1;
};

transition t9 := {
 from   := onbrake;
 to     := onbrake;
 guard  := b>s+1;
 action := s'=s+1;
};

transition t10 := {
 from   := onbrake;
 to     := onbrake;
 guard  := d<9;
 action := d'=d+1, b'=b+1;
};

transition t11 := {
 from   := stopped;
 to     := stopped;
 guard  := b>s+1;
 action := s'=s+1;
};

transition t12 := {
 from   := stopped;
 to     := ontime;
 guard  := b=s+1;
 action := s'=s+1, d'=0;
};

transition t13 := {
 from   := ontime;
 to     := ontime;
 guard  := b<s+9;
 action := b'=b+1;
};

}

strategy s1 {

Region init := {state=ontime && b=s && s=d && d=0};

Region bad := { s-b >29 && s>=b };
}