// ************************************************************************** //
//                                                                            //
//    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                                             //
//                                                                            //
// ************************************************************************** //
// The following module checks whether a given graph has cycles. This is done //
// essentially by computing the transitive hull of the graph, thus O(log(N))  //
// time using O(N^3) processors is sufficient.                                //
// ************************************************************************** //

macro N = 9;


module CyclicByTransHull([N][N]bool ?a,event hasCycle,!rdy) {
    [N][N]bool t;
    // compute the transitive hull in graph scc
    TransHull_OlogN(a,t,rdy);

    // check whether there is cycle in the graph
    for(i=0..N-1)
        for(j=i..N-1)
            if(t[i][j] & t[j][i]) 
                hasCycle = true;
}
drivenby g1 {
    // the assignments below construct the following graph:
    //
    //                 3
    //                / \
    //               v   v
    //    0 -> 1 <-> 2-> 4 <-> 5 <-> 6
    //               |         |
    //               v         v
    //               7<|       8
    //               |_|
    //
    a[0][1] = true;
    a[1][2] = true;
    a[2][1] = true;
    a[2][4] = true;
    a[2][7] = true;
    a[3][2] = true;
    a[3][4] = true;
    a[4][5] = true;
    a[5][4] = true;
    a[5][6] = true;
    a[5][8] = true;
    a[6][5] = true;
    a[7][7] = true;
    await(rdy);
    assert(hasCycle);
}
drivenby g2 {
    // worst case example: a chain of length N
    a[0][1] = true;
    a[1][2] = true;
    a[2][3] = true;
    a[3][4] = true;
    a[4][5] = true;
    a[5][6] = true;
    a[6][7] = true;
    await(rdy);
    assert(!hasCycle);
}