// ************************************************************************** // // // // 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 module explains the semantics of weak immediate suspensions. // // ************************************************************************** // module suspwkim(event ?i,nat{8} x) { w0: weak immediate suspend { next(x) = x+1; w1: pause; next(x) = x+1; w2: pause; next(x) = x+1; } when(i); } drivenby { i = true; // weak suspension at initial state d0a : pause; // system is at w0 with x==1 i = true; // strong suspension takes place at w0 d0b : pause; // system is at w0 with x==2 i = false; // no suspension; system proceeds to w1 d1 : pause; // system is at w1 with x==3 i = true; // strong suspension takes place at w1 d2 : pause; // still at w1 with x==4 i = false; // no suspension d3 : pause; // system is at w2 with x==5 i = true; // strong suspension takes place at w2 d4 : pause; // still at w2 with x==6 i = false; // no suspension d5 : pause; // system terminated with x==7 }