// ************************************************************************** //
//                                                                            //
//    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 computes the strongly connected components (SCCs) of  //
// a directed graph. The graph is given by its adjacency matrix a whose       //
// elements a[i][j] are true iff there is an edge from node i to node j. The  //
// algorithm computes the transitive hull of a so that the SCCs can be easily //
// read from the transitive hull.                                             //
// In addition to a matrix scc where scc[i][j] holds iff nodes i and j are in //
// the same scc, the module also computes a boolean vector rep that maps each //
// node i to a representative of its scc. To this end, the node with the least//
// index of an scc is chosen. Using this mapping rep, we also compute the     //
// quotient graph qa whose nodes are the sccs having edges whenever some nodes//
// in the corresponding sccs are connected.                                   //
// As can be seen, the complexity is essentially due to the transitive hull,  //
// since all other computations are done in O(1) using O(N^3) processors that //
// are also used for the computation of the transitive hull. Hence, the total //
// time is O(log(N)) using O(N^3) processors.                                 //
// ************************************************************************** //

macro N = 9;


module SCCbyTransHull([N][N]bool ?a,scc,qa,[N]nat{N} rep,event !rdy) {
    event transhullrdy;
    event [N][N]bool m;

    // compute the transitive hull in graph scc
    TransHull_OlogN(a,scc,transhullrdy);

    // the scc's are obtained by the transitive hull as follows:
    for(i=0..N-1)
        for(j=0..N-1)
            next(scc[i][j]) = i==j | scc[i][j] & scc[j][i];
    pause;

    // compute mapping of nodes to least node in scc in one step
    // using O(N^2) processors (can be reduced to O(N^{1+eps}) procs.
    for(i=0..N-1) {
        // rep[i] = least j, where scc[i][j] holds
        // set m[i][j] iff some scc[i][k] is greater than scc[i][j]
        for(j=0..N-1)
            for(k=j+1..N-1)
                if(scc[i][j] & scc[i][k])
                    m[i][k] = true;
        // thus, those j where scc[i][j] & !m[i][j] holds are the ones
        for(j=0..N-1)
            if(scc[i][j] & !m[i][j])
                rep[i] = j;
    }
    
    // compute condensed graph (consisting of scc classes)
    for(i=0..N-1)
        for(j=0..N-1)
            if(a[i][j])
                qa[rep[i]][rep[j]] = true;

    emit(rdy);
}
drivenby {
    // 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(forall(i=0..N-1) 
            forall(j=0..N-1)
                (scc[i][j] <->
                    (i==0 &  j==0 |
                     i==1 & (j==1 | j==2) |
                     i==2 & (j==1 | j==2) |
                     i==3 &  j==3 |
                     i==4 & (j==4 | j==5 | j==6) |
                     i==5 & (j==4 | j==5 | j==6) |
                     i==6 & (j==4 | j==5 | j==6) |
                     i==7 &  j==7 |
                     i==8 &  j==8)
                )
          );
    assert(rep[0] == 0);
    assert(rep[1] == 1);
    assert(rep[2] == 1);
    assert(rep[3] == 3);
    assert(rep[4] == 4);
    assert(rep[5] == 4);
    assert(rep[6] == 4);
    assert(rep[7] == 7);
    assert(rep[8] == 8);

    assert(forall(i=0..N-1) 
            forall(j=0..N-1)
                (qa[i][j] <->
                    (i==0 &  j==1 |
                     i==1 & (j==1 | j==4 | j==7) |
                     i==3 & (j==1 | j==4) |
                     i==4 & (j==4 | j==8) |
                     i==7 &  j==7)
                )
          );
}