// ************************************************************************** //
//                                                                            //
//    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:                       //
//                                                                            //
//                +-----------------------+                                   //
//                |  +-----+              |                                   //
//                +->| Buf |--+           |                                   // 
//                   +-----+  |           | x1                                //
//                            |  +-----+  |                                   //
//                +-----------o->|     |  |                                   //
//            x2  |  +-----+     | Add |  |                                   //
//                +->| Buf |---->|     |--o-->  y                             // 
//                   +-----+  x3 +-----+                                      //
//                                                                            //
//                                                                            //
// This SIGNAL program generates the sequence of Fibonacci numbers. It is a   //
// nice example for compositional verification.                               //
// ************************************************************************** //

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

module Fibonacci(event ?clk_y,event int !val_y) {
    event(int * bool) x1,x2,x3;
       Buf(x1,x2,1);
    || Buf(x2,x3,1);
    || Add(x2,x3,x1);
    || CpyOut(clk(x1),clk_y,val(x1),val_y);
}
// ************************************************************************** //
// This input trace is not clock consistent and will lead to val(x2)=⊤ in the //
// second macro step of the Quartz program.                                   //
// ************************************************************************** //
drivenby t1 {
    int i;
    while(i<100) {
        clk_y  = true;
        next(i) = i+1;
        pause;
    }
}