// ************************************************************************** //
//                                                                            //
//    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.       // 
//                                                                            //
//                                                                            //
//        +---------+ push                                                    //
//        | vehicle | --->                                                    //
//        +---------+                                                         //
//          O     O                  goal area                                //
//                              |--------|--------|                           //
//            |--------|--------|--------|--------|--------|--------|----->   //
//            0        1        2        3        4        5        6         //
//                                                                            //
// The program below stops the vehicle as soon as sensedDist>=3 is seen. Note //
// that the following holds in the different cases where sensedDist is either //
// exactDist-1, exactDist, or exactDist+1 for the condition sensedDist>=3 and //
// its negation:                                                              //
//                                                                            //
//      +---------------+--------------+--------------+--------------+        //
//      |      err      |     <0       |      =0      +      >0      |        //
//      +---------------+--------------+--------------+--------------+        //
//      | sensedDist    | exactDist-1  | exactDist    | exactDist+1  |        //
//      +---------------+--------------+--------------+--------------+        //
//      | sensedDist<3  | exactDist<4  | exactDist<3  | exactDist<2  |        //
//      +---------------+--------------+--------------+--------------+        //
//      | sensedDist>=3 | exactDist>=4 | exactDist>=3 | exactDist>=2 |        //
//      +---------------+--------------+--------------+--------------+        //
//                                                                            //
// Hence, if at some time t we have sensedDist<3, which changed at time t+1,  //
// thus changedsensedDist<3 holds at t+1, then we definitely had exactDist<2  //
// at time t, and have exactDist>=4 at time t+1. Thus, we can prove that the  //
// vehicle correctly stops in the desired area.                               //
// ************************************************************************** //


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

    // note that exactDist is made local and therefore hidden to the vehicle
    {int{3} 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;
}