// ************************************************************************** // // // // 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 shows that values of local variables that are assigned in the // // surface of the local declaration have to be carefully distinguished. The // // local variable x can several reincarnations that receive different values // // according to the current incarnations of the local events x0 and x1. // // 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 SurfaceSelection1(event ?in1,?in2,?in3, bv{2} y) { do { event x0; { w0: pause; emit(x0); } || do { event x1; { w1: 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; w: pause; y = x; } while(in3); } while(in2); } while(in1); } drivenby drv0 { pause; in1 = false; in2 = false; in3 = false; pause; } drivenby drv1 { pause; in1 = false; in2 = false; in3 = true; pause; } drivenby drv2 { pause; in1 = false; in2 = true; in3 = false; pause; } drivenby drv3 { in1 = false; in2 = false; in3 = false; pause; } drivenby drv4 { in1 = false; in2 = false; in3 = false; pause; }