```// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// This module implements an example for using knowledge-based reasoning. We  //
// consider a vehicle that is either pushed by the environment one step to the//
// right or is left where it is. The vehicle has a sensor to detect where it  //
// currently is, but this sensor is not precise and can signal the position   //
// only with an error of +/-1. The problem is now to implement a program for  //
// the vehicle that stops the vehicle via emission of the stop signal within  //
// so that the vehicle is in the goal area 2<=exactDist & exactDist<=4.       //
// Clearly, if sensedDist==3 holds, then the vehicle can safely stop since it //
// is definitely sure to be in the goal area, because 2<=exactDist<=4 holds.  //
// However, checking sensedDist==3 to emit the stop signal is not correct as  //
// shown by driver t1 below.                                                  //
//                                                                            //
//                                                                            //
//        +---------+ push                                                    //
//        | vehicle | --->                                                    //
//        +---------+                                                         //
//          O     O                  goal area                                //
//                              |--------|--------|                           //
//            |--------|--------|--------|--------|--------|--------|----->   //
//            0        1        2        3        4        5        6         //
//                                                                            //
// ************************************************************************** //

module Robot01(event ?push, int{2} ?err, event stop) {
int sensedDist; // distance determined by vehicle's sensor

// note that exactDist is made local and therefore hidden to the vehicle
{int exactDist;
// this thread maintains the exact distance
loop {
if(push & !stop)
next(exactDist) = exactDist + 1;
assert(stop -> 2<=exactDist & exactDist<=4);
w1: pause;
}
|| // this thread models the sensor which determines sensedDist with error
loop {
case
(err>0) do sensedDist = exactDist + 1;
(err<0) do sensedDist = exactDist - 1;
default
sensedDist = exactDist;
w2: pause;
}
} // end of scope of exactDist
|| // This thread models the vehicle's program whose aim is to emit stop
// when it is sure that 2<=exactDist<=4 holds only based on sensedDist.
// The program below is not correct (see driver t1)
loop {
if(sensedDist==3)
immediate always{ emit(stop); }
w3: pause;
}
}
satisfies {
goal1: assert A F stop;
}

// this driver demonstrates a counterexample to show that the above vehicle
// control is not correct
drivenby t1 {
push = true;
err = 0;
pause;
push = true;
err = 0;
pause;
push = true;
err = -1;
pause;
push = true;
err = +1;
pause;
push = true;
err = +1;
pause;
}
```