// ************************************************************************** // // // // 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]. The guarded actions // of the program are: // initial // True => next(w) = True // o1 => o2 = True // True => __asrt011 : assert !o1&!o2 // main: // w&!o2 => o1 = True // // The program is constructive with the behavior specified in the assertions. // ************************************************************************** // module P14(event o1,o2) { if(o1) emit(o2); assert(!o1 & !o2); w: pause; if(!o2) emit(o1); assert(o1 & !o2); } drivenby { pause; }