// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// A module to test the correct transfer of values from surface to depth.     //
// ************************************************************************** //

module T07 (int !b) {
    ell0: pause;
    loop {
        event int x;
        next(x) = 1;
        assert(x==0);
        ell1: pause;
        if(x == 1) b = 3;
        else b = 5;
        assert(x==1);
        ell2: pause;
        x = 2;
        assert(x==2);
    }
} drivenby {
    for(i=0..7) pause;
}