// ************************************************************************** //
//                                                                            //
//    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 implements Warshall's algorithm to compute the lengths//
// of all shortest paths between all pairs of nodes (i,j) of a graph.         //
// As can be seen, it requires O(N) time using O(N^2) processors.             //
// ************************************************************************** //

macro N = 9;
macro addp(x,y) = (x>0 & y>0 ? x+y : 0);
macro min(x,y) = (x==0 ? y : (y==0 ? x : (x<=y ? x : y)));

module AllPairsShortestPaths_ON1([N][N]nat ?a, t,event !rdy) {
    for(k=0..N-1) {
        for(i=0..N-1) {
            for(j=0..N-1)
                next(t[i][j]) = (k==0 ? min(a[i][j],addp(a[i][k],a[k][j]))
                                      : min(t[i][j],addp(t[i][k],t[k][j])));
        }
        pause;
    }
    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] = 1;
    a[1][2] = 1;
    a[2][1] = 1;
    a[2][4] = 1;
    a[2][7] = 1;
    a[3][2] = 1;
    a[3][4] = 1;
    a[4][5] = 1;
    a[5][4] = 1;
    a[5][6] = 1;
    a[5][8] = 1;
    a[6][5] = 1;
    a[7][7] = 1;
    await(rdy);
//    for(i=0..N-1) 
//        for(j=0..N-1)
//            assert((t[i][j] <->
//                    (i==0 & (j==1 | j==2 | j==4 | j==5 | j==6 | j==7 | j==8) |
//                     i==1 & (j==1 | j==2 | j==4 | j==5 | j==6 | j==7 | j==8) |
//                     i==2 & (j==1 | j==2 | j==4 | j==5 | j==6 | j==7 | j==8) |
//                     i==3 & (j==1 | j==2 | j==4 | j==5 | j==6 | j==7 | j==8) |
//                     i==4 & (              j==4 | j==5 | j==6 |        j==8) |
//                     i==5 & (              j==4 | j==5 | j==6 |        j==8) |
//                     i==6 & (              j==4 | j==5 | j==6 |        j==8) |
//                     i==7 &  j==7)
//                )
//          );
}