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

// ----------------------------------------------------------------
// In this file, we take the algorithms of KuLL87a.qrz and map one
// of the three iterations to time. Thus, the three-dimensional
// arrays become two-dimensional.
// ----------------------------------------------------------------

import ComputerArchitecture.SystolicArrays.TransitiveClosure.Warshall.*;

macro N = 3;

module TimedKuLL87a([N][N]bool ?a, t1, t2, event !rdy, !OnlyReflexive) {
//Compares TimedOpt3RotLocDepWarshall with WarshallB
{TimedRotLocDepWarshall(a,t1,OnlyReflexive); || WarshallB(a,t2);}
//Other alternatives for example:
// {TimedOpt3RotLocDepWarshall(a,t1,OnlyReflexive); || WarshallB(a,t2);}
// {TimedOpt1RotLocDepWarshall(a,t1,OnlyReflexive); || WarshallB(a,t2);}
// {TimedOpt2RotLocDepWarshall(a,t1,OnlyReflexive); || WarshallB(a,t2);}
emit (rdy);
}
satisfies {
s : assert (OnlyReflexive->
forall(i=0..(N-1))
forall(j=0..(N-1))
a[i][i]
)
-> A G (rdy ->
forall(i=0..(N-1))
forall(j=0..(N-1))
(t1[i][j] <-> t2[i][j])
);
}
```