// ************************************************************************** //
//                                                                            //
//    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 |-----o------->|     | x5 +--------+             //
//                   +-------+     |        | Add |----| CpyOut |---> y       //
//                                 |  +---->|     |    +--------+             //
//                   +-----+   x2  |  |     +-----+                           //
//                +->| Buf |---+   |  +--------+                              //
//                |  +-----+   |   |  +-----+  | x4                           //
//             x3 |            |   +->|     |  |                              //
//                |  +-----+   |      | Whn |--+                              //
//                +--| Not |<--o----->|     |                                 //
//                   +-----+          +-----+                                 //
//                                                                            //
// This program can be used to study various phenomena: First of all, observe //
// that x2 will produce a stream of boolean values that toggle (if that stream//
// will be generated at all). Thus, x4 requires values from x1 in every even  //
// step. Thus, if x has values in other steps than these, the program will not//
// be clock-consistent, and this is seen in that output driven execution of   //
// the When node will enforce clk(x2)=val(x2)=true while the negation assigns //
// val(x2)=false, thus yielding a write conflict.                             //
// On the other hand, using an input stream where x has values only at even   //
// points of time, we will see an underspecified behavior: Then, neither x1   //
// nor x5, nor y, and neither x4 will then have values at these points of time//
// and that leaves clk(x2) unknown.                                           //
// ************************************************************************** //

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

module Signal03(event(int* bool) ?x,event ?clk_y,event int !val_y) {
    event(int * bool) x1,x4,x5;
    event(bool * bool) x2,x3;
       CpyIn(x,x1);
    || BufBool(x3,x2,true);
    || Not(x2,x3);
    || When(x1,x2,x4);
    || Add(x1,x4,x5);
    || CpyOut(clk(x5),clk_y,val(x5),val_y);
    || loop {
            // check clock consistency
            assert(clk(x)   -> clk(x1));
            assert(clk(x3) <-> clk(x2));
            assert(clk(x4) <-> (clk(x1) & clk(x2) & val(x2)));
            assert(clk(x5) <-> clk(x1));
            assert(clk(x5) <-> clk(x4));
            assert(clk_y    -> clk(x5));
            asp: pause;
       }
}
// ************************************************************************** //
// This input trace is not clock consistent and will lead to val(x2)=⊤ in the //
// second macro step of the Quartz program.                                   //
// ************************************************************************** //
drivenby t1 {
    val(x) = 1;
    clk(x) = true;
    clk_y  = true;
    pause;
    val(x) = 2;
    clk(x) = true;
    clk_y  = true;
    pause;
    val(x) = 3;
    clk(x) = true;
    clk_y  = true;
    pause;
    val(x) = 4;
    clk(x) = true;
    clk_y  = true;
    pause;
    val(x) = 5;
    clk(x) = true;
    clk_y  = true;
}
// ************************************************************************** //
// This input trace is clock consistent, and could produce (in theory) values //
// at every even point of time (with finite memory). However, clk(x2) will be //
// unknown, since if neither clk(x1) nor clk(x4) holds, then clk(x2) is not   //
// determined (only by the mutually dependent assignments of Buf and Not).    //
// Thus, we have a lack of causality here.                                    //                               
// ************************************************************************** //
drivenby t2 {
    val(x) = 1;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = false;
    pause;
    val(x) = 3;
    clk(x) = true;
    clk_y  = true;
    pause;
    clk(x) = false;
    clk_y  = false;
    pause;
    val(x) = 5;
    clk(x) = true;
    clk_y  = true;
}