// ************************************************************************** // // // // 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) // ) // ); }