// ************************************************************************** // // // // 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 constructive example is due to G. Berry [Berr99]. // // ************************************************************************** // module P01(event ?i,o1,o2,o3) { if(i) emit(o1); if(!o1) emit(o2); if(o2) emit(o3); // here is the unique behavior assert((o1 <-> i) & (o2 <-> !i) & (o3 <-> !i)); } drivenby d0 { i = false; } drivenby d1 { i = true; }