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