// ************************************************************************** // // 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 // // ************************************************************************** module SEFM_ExampleB2( int ?x, y, event !go ) { ell0 : await (x>=1); y = x; emit (go); always next(y) = y + 1; } satisfies { s1 : assert A G (y>=0); s2 : assert E X true; }