// ************************************************************************** // // // // 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: True => o2 and o1&!o2 => o1. // The program is constructive with the behavior specified in the assertions. // ************************************************************************** // module P15(event o1,o2) { emit(o2); if(o1) if(!o2) emit(o1); assert(!o1 & o2); } drivenby { nothing; }