// ************************************************************************** // // // // 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 program is due to Gerard Berry. The "emit o1" statement is executed // // twice at the second point of time, where the threads are resumed from // // locations loc1 and loc3, respectively. It may become a problem when // // "emit o1" is replaced with another instantaneous statement. // // ************************************************************************** // module Schizo05(event !o1,!o2) { event x; loop { event t; weak immediate abort { event s; { if(x) emit(s); else pause; if(s) pause; || emit(o1); emit(o2); } || { pause; emit(x); emit(t); } } when(t); } } satisfies { s0 : assert !o1 & !o2; s1 : assert A X A G (o1 & o2); }