// ************************************************************************** //
//                                                                            //
//    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 +--------+                   //
//                   +-------+        | Def |----| 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 the   //
// Default node is made such that the clock tick of one input also demands a  //
// clock tick of the output, and that also a clock tick of the output stream  //
// demands a clock tick of one of the input streams. Thus, the output y may   //
// pull at x4 a value that forces in turn the Default node to pull at either  //
// x1 or x3, and if there should be no value at x1, x3 will trigger the nodes //
// Buf and Inc. As thereby the internal value stored in Buf is incremented, it//
// follows that values in the output stream y depend on the number of absent  //
// values in x1 that reach Def when x4 pulls a value.                         //
//   For example, the two drivers below both consider the input stream 9,8,7  //
// for input x, and stretching this input stream as in driver t1 or t2 yields //
// different output streams for y.                                            // 
// ************************************************************************** //

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

module Signal02(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);
    || Default(x1,x3,x4);
    || CpyOut(clk(x4),clk_y,val(x4),val_y);
    || loop {
            // check clock consistency
            assert(clk(x)   -> clk(x1));
            assert(clk(x2) <-> clk(x3));
            assert(clk(x4) <-> (clk(x1) | clk(x3)));
            assert(clk_y    -> clk(x4));
            asp: pause;
       }
}
// ************************************************************************** //
// Input driver t1 below produces the following trace:                        //
//                                                                            //
//    --------------------------------------------------------------          //
//    step  : 0      1      2      3      4     5       6      7              //
//    --------------------------------------------------------------          //
//    x.0   : 9      --     --     --     8      --     7      --             //
//    x.1   : True   False  False  False  True   False  True   False          //
//    x1.0  : 9      --     --     --     8      --     7      --             //
//    x1.1  : True   False  False  False  True   False  True   False          //
//    x2.0  :  --    1      2      3       --    4       --    5              //
//    x2.1  : udef   True   True   True   udef   True   udef   True           //
//    x3.0  :  --    0       1     2       --    3       --    4              //
//    x2.1  : udef   True   True   True   udef   True   udef   True           //
//    x4.0  : 9      0      1      2      8      3      7      4              //
//    x4.1  : True   True   True   True   True   True   True   True           //
//    val_y : 9      0      1      2      8      3      7      4              //
//    clk_y : True   True   True   True   True   True   True   True           //
//    --------------------------------------------------------------          //
//                                                                            //
// ************************************************************************** //
drivenby t1 {
    val(x) = 9;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    val(x) = 8;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    val(x) = 7;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
}
// ************************************************************************** //
// Input driver t2 below uses a flow (and even clock equivalent) input trace  //
// but yields an output trace for y that is neither clock nor flow equivalent://
//                                                                            //
//    --------------------------------------------                            //
//    step  : 0       1       2       3       4                               //
//    --------------------------------------------                            //
//    x.0   : 9      --     8      --     7                                   //
//    x.1   : True   False  True   False  True                                //
//    x1.0  : 9      --     8      --     7                                   //
//    x1.1  : True   False  True   False  True                                //
//    x2.0  :  --    1       --    2       --                                 //
//    x2.1  : udef   True   udef   True   udef                                //
//    x3.0  :  --    0       --    1       --                                 //
//    x3.1  : udef   True   udef   True   udef                                //
//    x4.0  : 9      0      8      1      7                                   //
//    x4.1  : True   True   True   True   True                                //
//    val_y : 9      0      8      1      7                                   //
//    clk_y : True   True   True   True   True                                //
//    --------------------------------------------                            //
//                                                                            //
// ************************************************************************** //
drivenby t2 {
    val(x) = 9;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    val(x) = 8;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    val(x) = 7;
    clk(x) = true;
    clk_y  = true;
}