// ************************************************************************** //
//                                                                            //
//    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 (cf. module Counter in //
// [BGSS13]):                                                                 //
//                                                                            //
//                x  +-------+  x1  +-----+                                   //
//              ---->| CpyIn |----->|     | x4  +--------+                    //
//                   +-------+      | Def |--o--| CpyOut |---> y              //
//                               +->|     |  |  +--------+                    //
//                   +-----+ x3  |  +-----+  |                                //
//                +->| Dec |-----+           |                                //
//                |  +-----+                 |                                //
//             x2 |                          |                                //
//                |  +-----+                 |                                //
//                +--| Buf |<----------------+                                //
//                   +-----+                                                  //
//                                                                            //
// 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.                          //
// ************************************************************************** //

import BasicNodes.*;

macro val(x) = x.0;
macro clk(x) = x.1;

module Signal00(event(int* bool) ?x,event ?clk_y,event int !val_y) {
    event(int * bool) x1,x2,x3,x4;
       CpyIn(x,x1);
    || Dec(x2,x3);
    || Buf(x4,x2,0);
    || 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(x2) <-> clk(x4));
            assert(clk(x4) <-> (clk(x1) | clk(x3)));
            assert(clk_y    -> clk(x4));
            asp: pause;
       }
}
// ************************************************************************** //
// The input driver below produces the following trace:                       //
//                                                                            //
//    --------------------------------------------                            //
//    step  : 0       1       2       3       4                               //
//    --------------------------------------------                            //
//    x.0   : 2       0       0       1       0                               //
//    x.1   : True    False   False   True    False                           //
//    x1.0  : 2       0       0       1       0                               //
//    x1.1  : True    False   False   True    False                           //
//    x2.0  : 0       2       1       0       1                               //
//    x2.1  : True    True    True    True    True                            //
//    x3.0  : -1      1       0       -1      0                               //
//    x3.1  : True    True    True    True    True                            //
//    x4.0  : 2       1       0       1       0                               //
//    x4.1  : True    True    True    True    True                            //
//    val_y : 2       1       0       1       0                               //
//    clk_y : True    True    True    True    True                            //
//                                                                            //
// ************************************************************************** //
drivenby t1 {
    val(x) = 2;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
    pause;
    val(x) = 1;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = true;
}