Three integer variables are used: s as speed for the speed, t as time for the seconds and d as distance for the estimated distance that the model car travels after loosing its track.

When the model car is erring, the maximum speed allowed is 2 meters per second and the maximum time is 3 seconds. The maximal distance travelled is 3 times 2 plus 3 for the last iteration. If the wall is 10 meter away from the track, the model car will never crash into it.

These numerical constants could be changed, but have to be known numerically at analysis time to keep the invariants in the affine relationship set.

program voiture02 C Test de l'arret de la voiture propose par Nicolas Halbwachs, 15 C mars 2005 integer s, t, d s = 0 t = 0 d = 0 do while(s.le.2.and.t.le.3) read *, x if(x.gt.0.) then t = t + 1 s = 0 else d = d + 1 s = s + 1 endif enddo print *, s, t, d read *, t, s if(d.le.10) then print *, "healthy" else print *, "crashed!" endif end