// ************************************************************************** // // // // 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 program is similar to SurfaceSelection1.qrz. The difference is that // // the assignments to the local variable x are delayed. Again, the problem is // // that several surfaces of the local declaration of x overlap, and each of // // them makes an assignment to next(x). // // Note that this is no write conflict, since we have different scopes. The // // problem is thereby that the output variable y will obtain the correct value// // at the next point of time. The correct value has to be stored in x so that // // y can take it after entering the local declaration. // // ************************************************************************** // module SurfaceSelection2(event in1,in2,in3, bv{2} !y) { do { event x0; { pause; emit(x0); } || do { event x1; { pause; emit(x1); } || do { bv{2} x; case (!x1 & !x0) do x=0b00; (!x1 & x0) do x=0b01; ( x1 & !x0) do x=0b10; ( x1 & x0) do x=0b11; default nothing; pause; y = x; } while(in3); } while(in2); } while(in1); } satisfies { time00 : assert (y == 0b00); time01 : assert A X (y == 0b00); time02 : assert A X ( ( in3 -> A X (y == 0b11)) & (!in3 & in2 -> A X (y == 0b01)) & (!in3 & !in2 & in1 -> A X (y == 0b00)) & (!in3 & !in2 & !in1 -> A X (y == 0b00)) ); }