// ************************************************************************** // // // // 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; }