// ************************************************************************** // // // // 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 non-constructive example is due to G. Berry [Berr99]. It is remarkable // that the guarded actions of the program o1 => o1 and o1&!o2 => o2 have a // unique solution (!o1 & !o2) that is however, not constructive. // ************************************************************************** // module P09(event o1,o2) { if(o1) emit(o1); || if(o1) if(o2) nothing; else emit(o2); } drivenby { nothing; }