// ************************************************************************** //
//                                                                            //
//    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 modules of this file show the step-by-step derivation of the
// systolic array described in KuLL87a.
// ----------------------------------------------------------------

import ComputerArchitecture.SystolicArrays.TransitiveClosure.KuLL87a.*;
import ComputerArchitecture.SystolicArrays.TransitiveClosure.Warshall.WarshallB;

package ComputerArchitecture.SystolicArrays.TransitiveClosure.KuLL87a;

macro N = 3;

module KuLL87a([N][N]bool ?a, t2,[N][N][N]bool t1, event !rdy, !OnlyReflexive) {
    {Opt3RotLocDepWarshall(a,t1,OnlyReflexive); || WarshallB(a,t2);}
    //Other alternatives are, e.g.:
    //Opt1RotLocDepWarshall(a,t1,OnlyReflexive); || WarshallB(a,t2);}
    //Opt2RotLocDepWarshall(a,t1,OnlyReflexive); || WarshallB(a,t2);}
    //RotLocDepWarshall(a,t1,OnlyReflexive); || WarshallB(a,t2);}
    //RotWarshall(a,t1,OnlyReflexive); || WarshallB(a,t2);}
    //LocDepWarshall(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][N-1] <-> t2[i][j])
        );
}

// ----------------------------------------------------------------
// The reference is the O(N) time version of Warshall's
// algorithm (see WarshallAB.qrz for equivalent variants).
// ----------------------------------------------------------------