// ************************************************************************** // // // // 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 the recursive definitions of Warshall's // // algorithm to compute the transitive hull of a binary relation or a graph. // // As can be seen, it requires only one macro step containing N^3 micro // // steps. Since these N^3 micro steps form N^2 chains of length N, we have to // // admit in terms of PRAM algorithms that the algorithm has depth O(N), and // // thus, can only make use of N^2 processors in parallel. // // ************************************************************************** // macro N = 9; module TransHull_ON0([N][N]bool ?a, [N][N][N]bool t) { for(k=0..N-1) for(i=0..N-1) for(j=0..N-1) t[k][i][j] = (k==0 ? a[i][j] | a[i][k] & a[k][j] : t[k-1][i][j] | t[k-1][i][k] & t[k-1][k][j]); } 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; for(i=0..N-1) for(j=0..N-1) assert((t[N-1][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) ) ); }