// ************************************************************************** // // // // 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 example is due to G. Berry [Berr99] and shows that constructiveness // // may depend on inputs. // // ************************************************************************** // module P08(event ?i,o1,o2) { weak immediate abort { { if(!i) w: pause; emit(o1); } || if(o1) emit(o2); } when(o2); emit(o1); } drivenby drv0 { // i=false is not constructive i = false; } drivenby drv1 { // i=true yields a constructive behavior i = true; assert(o1 & o2); }