```// ************************************************************************** //
//                                                                            //
//    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 an algorithm to compute the transitive hull//
// of a binary relation or a graph. It is based on an algorithm for boolean   //
// matrix multiplication that requires O(1) time using O(N^3) processors.     //
// This algorithm is used for iterative squaring of the given matrix so that  //
// in total O(log(N)) time with O(N^3) processors is required.                //
// Note that t is a memorized variable, so that it is sufficient to only set  //
// potentially new elements t[i][j] while those that are already true remain  //
// so automatically. Finally note that it is an CRCW algorithm since several  //
// writes to the same t[i][j] with the same value true are possible.          //
// ************************************************************************** //

macro N = 9;

module TransHull_OlogN([N][N]bool ?a, t,event !rdy) {
// copy matrix a to t
for(i=0..N-1)
for(j=0..N-1)
t[i][j] = a[i][j];
// iterative squaring
for(h=0..log(N)-1) {
// multiply matrix t with itself
for(i=0..N-1) {
for(j=0..N-1)
for(k=0..N-1)
if(t[i][k] and t[k][j])
next(t[i][j]) = true;
}
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] = 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);
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)
)
);
}
drivenby t2 {
// the assignments below construct the following graph that
// is a worst case example
//
//    0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 6 -> 7 -> 8
//
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;
a[7][8] = true;
await(rdy);
}
```