// ************************************************************************** //
//                                                                            //
//    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 example (adapted from [TOBG08]) demonstrates that endochrony is not   //
// compositional, i.e., systems built of endochronous modules may not be      //
// endochronous. To this end, the drivers given below represent synchronous   //
// that are not clock equivalent, even though their inputs are flow           // 
// equivalent.                                                                //
//                                                                            //
//                                                     +-------+              //
//        x1 ----------------------------------------->|       |              //
//                                                     |       |              //
//                                        +------+     |       |              //
//                 +-----+ z1  +-----+ 1->|      | z3  |       |              //
//        x2 --o-->| Buf |---->|     |    | When |---->| Merge |----> y1      //
//             |   +-----+     | !=  |--->|      |     |       |              //
//             +-------------->|     | z2 +------+     |       |              //
//                             +-----+                 |       |              //
//        x3 ----------------------------------------->|       |              //
//                                                     +-------+              //
//                                                                            //
// This system can run at least the following behaviors t1,t2 and t3 which are//
// not clock equivalent, but their input streams are flow equivalent (thus a  //
// clock generator cannot know which of the two behaviors should be used, and //
// thus, the system is not endochronous even though all used modules are so): //
//                                                                            //
//    --------------          ----------------          ----------------      //
//      behavior t1             behavior t2               behavior t3         //
//    --------------          ----------------          ----------------      //
//    x1 : 0 1 - 1 0          x1 : - 0 1 - 1 0          x1 : 0 - 1 - 1 0      //
//    x2 : 1 0 0 1 -          x2 : 1 - 0 0 1 -          x2 : - 1 0 0 1 -      //
//    x3 : 1 - - - 0          x3 : - 1 - - - 0          x3 : 1 - - - - 0      //
//    z1 : 1 1 0 0 -          z1 : 1 - 1 0 0 -          z1 : - 1 1 0 0 -      //
//    z2 : 0 1 0 1 -          z2 : 0 - 1 0 1 -          z2 : - 0 1 0 1 -      //
//    z3 : - 1 - 1 -          z3 : - - 1 - 1 -          z3 : - - 1 - 1 -      //
//    y  : 1 1 - 1 0          y  : - 1 1 - 1 0          y  : 1 - 1 - 1 0      //
//    --------------          ----------------          ----------------      //
//    act:AB C D E F          act: A B C D E F          act: B A C D E F      //
//    --------------          ----------------          ----------------      //
//                                                                            //
// Having a closer look at the three behaviors reveals that they are not that //
// different: As shown above, we denoted the basic synchronous actions with   //
// capital letters A,…,F, so that one can see that behaviors t2 and t3 differ //
// in that the actions A and B are swapped, and behavior t1 is obtained by    //
// executing these two actions at the same point of time. This is possible,   //
// since these actions are independent as will be explained below.            //
// The Merge node is driven by input x1 which is always read by this node: It //
// therefore reads a value from x1 and if that is "true" then at the same time//
// a value from z3 is read, otherwise a value from x3 is read. While values of//
// input streams like x1 and x3 can be considered available at any desired    //
// point of time, the value to be read from z3 must be first produced by the  //
// other nodes. Now, to produce a value at z3 (which is always 1), one has to //
// read values from x2 until there will be a change, i.e., z3 is 1 if and only//
// if x2 has a value at that point of time that is different to the previous  //
// value read from x2. Therefore, reading a sequence of equal values from x2  //
// does not produce a value at z3, and does therefore not trigger the Merge   //
// node. Thus, this can be done independent of the other actions, but must be //
// done before a value "true" is read from x1. Running the above program thus //
// requires a "lookahead" of the tokens read from x1, and in case a true token//
// is next, one has to read values from x2 until a value is produced at z3.   //
// ************************************************************************** //

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

module Signal04(event(bool * bool) ?x1,event(int * bool) ?x2,?x3,y) {
    event(int * bool) v2,v3,v4,z1,z3;
    event(bool * bool) v1,z2;
       CpyInBool(x1,v1);
    || CpyIn(x2,v2);
    || CpyIn(x3,v3);
    || Buf(v2,z1,1);
    || NotEqual(z1,v2,z2);
    || When(v4,z2,z3);
    || Merge(v1,z3,v3,y);
    || loop {
            clk(v4) = true;
            val(v4) = 1;
            pause;
       }
}
drivenby t1 {
// driver t1 yields the following behavior:
//
//    x1 : 0 1 - 1 0
//    x2 : 1 0 0 1 -
//    x3 : 1 - - - 0
//    z1 : 1 1 0 0 -
//    z2 : 0 1 0 1 -
//    z3 : - 1 - 1 -
//    y  : 1 1 - 1 0
//
    val(x1) = false;
    val(x2) = 1;
    val(x3) = 1;
    clk(x1) = true;
    clk(x2) = true;
    clk(x3) = true;
    pause;
    val(x1) = true;
    val(x2) = 0;
    clk(x1) = true;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x2) = 0;
    clk(x1) = false;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x1) = true;
    val(x2) = 1;
    clk(x1) = true;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x1) = false;
    val(x3) = 0;
    clk(x1) = true;
    clk(x2) = false;
    clk(x3) = true;    
}
drivenby t2 {
// driver t2 yields the following behavior:
//
//    x1 : - 0 1 - 1 0 
//    x2 : 1 - 0 0 1 -
//    x3 : - 1 - - - 0
//    z1 : 1 - 1 0 0 -
//    z2 : 0 - 1 0 1 -
//    z3 : - - 1 - 1 - 
//    y  : - 1 1 - 1 0
//
    val(x2) = 1;
    clk(x1) = false;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x1) = false;
    val(x3) = 1;
    clk(x1) = true;
    clk(x2) = false;
    clk(x3) = true;
    pause;
    val(x1) = true;
    val(x2) = 0;
    clk(x1) = true;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x2) = 0;
    clk(x1) = false;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x1) = true;
    val(x2) = 1;
    clk(x1) = true;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x1) = false;
    val(x3) = 0;
    clk(x1) = true;
    clk(x2) = false;
    clk(x3) = true;
}
drivenby t3 {
// driver t3 yields the following behavior:
//
//    x1 : 0 - 1 - 1 0 
//    x2 : - 1 0 0 1 -
//    x3 : 1 - - - - 0
//    z1 : - 1 1 0 0 -
//    z2 : - 0 1 0 1 -
//    z3 : - - 1 - 1 - 
//    y  : 1 - 1 - 1 0
//
    val(x1) = false;
    val(x3) = 1;
    clk(x1) = true;
    clk(x2) = false;
    clk(x3) = true;
    pause;
    val(x2) = 1;
    clk(x1) = false;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x1) = true;
    val(x2) = 0;
    clk(x1) = true;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x2) = 0;
    clk(x1) = false;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x1) = true;
    val(x2) = 1;
    clk(x1) = true;
    clk(x2) = true;
    clk(x3) = false;
    pause;
    val(x1) = false;
    val(x3) = 0;
    clk(x1) = true;
    clk(x2) = false;
    clk(x3) = true;
}