// ************************************************************************** //
//                                                                            //
//    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.          //
// ************************************************************************** //



[7][7]bool t;

function log2Ceil(nat n) : nat {
	nat h,l;
	h = 1;
	l = 0;
  	while(h<n) {
        	h = h*2;
        	l = l+1;
   	 }

	return l;
}

function TransHull_OlogN(nat n, [][]bool a):nat{
nat i,j,k,h;
	//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..log2Ceil(n)-1){
		for(i=0..n-1){
			for(j=0..n-1){
				for(k=0..n-1){
					if(t[i][k] & t[k][j]){
						t[i][j]=true;
					}
				}
			}
		}
	}

	return 1;
}

thread test{
    nat x,n,i,j;
    [7][7]bool a;
    bool test_passed;
    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;
    n = 9;
    x = TransHull_OlogN(n,a);

    for(i=0..n-1){
        for(j=0..n-1){
			if(!((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)
                )))
                {
                test_passed = false;
                }

        }

    }
}