// ************************************************************************** //
//                                                                            //
//    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 a constructive variant of the default operator of   //
// SIGNAL that allows input and output driven behaviors (see table below).    //
// ************************************************************************** //


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

module Default(event (int * bool) x1,x2,y) {
    loop {
        // await trigger event
        if(clk(x1) or clk(x2) or clk(y) and (!clk(x1) or !clk(x2))) {
            // ensure clock consistency
            emit(clk(y));
            if(!clk(x1)) emit(clk(x2));
            if(!clk(x2)) emit(clk(x1));
            // produce output values
            val(y) = (clk(x1)?val(x1):val(x2));
        }
        // negative clock information
        if(!clk(y) | !clk(x1) & !clk(x2)) {
            // ensure clock consistency
            clk(x1) = false;
            clk(x2) = false;
            clk(y)  = false;
        }
        pause;
    }
}


// ************************************************************************** //
// In the following table, cx1',cx2', and cy' denote the values after the     //
// fixpoint iteration of the causality analysis when we start with the listed //
// initial values. In case only values "-" are listed, the obtained fixpoint  //
// was inconsistent, i.e. changing an already available boolean value.        //
// In column "action", we note which action of the Default node is taken,     //
// where the following is possible:                                           //
//                                                                            //
//      x1->y:  x1 triggers the information flow from x1 to y                 //
//      x2->y:  x2 triggers the information flow from x2 to y                 //
//      x1<-y:   y triggers the information flow from x1 to y                 //
//      x2<-y:   y triggers the information flow from x2 to y                 //
//      x1<->y: x1 and y trigger the information flow from x1 to y            //
//      x2<->y: x2 and y trigger the information flow from x2 to y            //
//      silent: no action of the default node                                 //
//      ??:     underspecified case; could complete to one of several actions //
//      ---:    inconsistent clock assignment                                 //
//                                                                            //
//            +----------------+----------------+--------+                    //
//            | initial values |  final values  |        |                    //
//            +----------------+----------------+--------+                    //
//            | cx1  cx2  cy   | cx1' cx2' cy'  | action |                    //
//            +----------------+----------------+--------+                    //
//            |  U    U    U   |  U    U    U   |   ??   |                    //
//            |  U    U    F   |  F    F    F   | silent |                    //
//            |  U    U    T   |  U    U    T   |   ??   |                    //
//            |  U    F    U   |  U    F    U   |   ??   |                    //
//            |  U    F    F   |  F    F    F   | silent |                    //
//            |  U    F    T   |  T    F    T   | x1<-y  |                    //
//            |  U    T    U   |  U    T    T   |   ??   |                    //
//            |  U    T    F   |  -    -    -   |  ---   |                    //
//            |  U    T    T   |  U    T    T   |   ??   |                    //
//            +----------------+----------------+--------+                    //
//            |  F    U    U   |  F    U    U   |   ??   |                    //
//            |  F    U    F   |  F    F    F   | silent |                    //
//            |  F    U    T   |  F    T    T   | x2<-y  |                    //
//            |  F    F    U   |  F    F    F   | silent |                    //
//            |  F    F    F   |  F    F    F   | silent |                    //
//            |  F    F    T   |  -    -    -   |  ---   |                    //
//            |  F    T    U   |  F    T    T   | x2->y  |                    //
//            |  F    T    F   |  -    -    -   |  ---   |                    //
//            |  F    T    T   |  F    T    T   | x2<->y |                    //
//            +----------------+----------------+--------+                    //
//            |  T    U    U   |  T    U    T   | x1->y  |                    //
//            |  T    U    F   |  -    -    -   |  ---   |                    //
//            |  T    U    T   |  T    U    T   | x1<->y |                    //
//            |  T    F    U   |  T    F    T   | x1->y  |                    //
//            |  T    F    F   |  -    -    -   |  ---   |                    //
//            |  T    F    T   |  T    F    T   | x1<->y |                    //
//            |  T    T    U   |  T    T    T   | x1->y  |                    //
//            |  T    T    F   |  -    -    -   |  ---   |                    //
//            |  T    T    T   |  T    T    T   | x1<->y |                    //
//            +----------------+----------------+--------+                    //
//                                                                            //
//                                                                            //
// ************************************************************************** //