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