// ************************************************************************** //
//                                                                            //
//    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 implements the following SIGNAL program:                       //
//                                                                            //
//                x  +-------+   x1   +-----+                                 //
//              ---->| CpyIn |------->|     | x4 +--------+                   //
//                   +-------+        | Add |----| CpyOut |---> y             //
//                                 +->|     |    +--------+                   //
//                   +-----+   x3  |  +-----+                                 //
//                +->| Buf |---o---+                                          //
//                |  +-----+   |                                              //
//             x2 |            |                                              //
//                |  +-----+   |                                              //
//                +--| Inc |<--+                                              //
//                   +-----+                                                  //
//                                                                            //
// Note here that the mutual recursive definition of x2 and x3 alone would not//
// have a reason to compute anything at all. However, the definition of Add is//
// made such that the clock tick of one input also demands a clock tick of the//
// other one, and that also a clock tick of the output stream demands clock   //
// ticks of the argument streams.                                             //
// ************************************************************************** //

import BasicNodes.*;
macro val(x) = x.0;
macro clk(x) = x.1;

module Signal01(event(int* bool) ?x,event ?clk_y,event int !val_y) {
    event(int * bool) x1,x2,x3,x4;
       CpyIn(x,x1);
    || Buf(x2,x3,0);
    || Inc(x3,x2);
    || Add(x1,x3,x4);
    || CpyOut(clk(x4),clk_y,val(x4),val_y);
    || loop {
            // check clock consistency
            assert(clk(x1) <-> clk(x3));
            assert(clk(x1) <-> clk(x4));
            assert(clk(x3) <-> clk(x2));
            assert(clk(x4) <-> clk_y);
            pause;
       }
}
// ************************************************************************** //
// The input driver below produces the following trace:                       //
//                                                                            //
//    --------------------------------------------                            //
//    step  : 0       1       2       3       4                               //
//    --------------------------------------------                            //
//    x.0   : 0       0       0       4       6                               //
//    x.1   : True    False   False   True    True                            //
//    x1.0  : 0       0       0       4       6                               //
//    x1.1  : True    True    True    True    True                            //
//    x2.0  : 1       2       3       4       5                               //
//    x2.1  : True    True    True    True    True                            //
//    x3.0  : 0       1       2       3       4                               //
//    x3.1  : True    True    True    True    True                            //
//    x4.0  : 0       1       2       7       10                              //
//    x4.1  : True    True    True    True    True                            //
//    val_y : 0       1       2       7       10                              //
//    clk_y : True    True    True    True    True                            //
//                                                                            //
// ************************************************************************** //
drivenby {
    val(x) = 0;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    val(x) = 4;
    clk(x) = true;
    clk_y  = true;
    pause;
    val(x) = 6;
    clk(x) = true;
    clk_y  = true;
}