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