// ************************************************************************** // // // // 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 checks that the depth of a local event variable does not see // // the actions of the surface even if these happen at the same time. // // ************************************************************************** // module Schizo11(event !x0,!x1,!x2,!x3) { loop { event x; if(x) emit(x1); else emit(x0); emit(x); w: pause; if(x) emit(x3); else emit(x2); } } satisfies { sx0 : assert A G !x0; sx1 : assert A G x1; sx2 : assert !x2 & A X A G x2; sx3 : assert A G !x3; }