// ************************************************************************** //
//                                                                            //
//    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
}