```// ************************************************************************** //
//                                                                            //
//    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 module below computes the set of states of a labelled transition system//
// where the CTL formula E[phi SU psi] holds, i.e. states that have a path    //
// that ends in a state where psi holds where all states on the path with the //
// possible exception of the last one satisfy phi. As can be seen, we reduce  //
// this problem to the computation of a transitive hull, so that O(log(N))    //
// time with O(N^3) processors is sufficient.                                 //
// ************************************************************************** //

macro N = 9;

module ExistsStrongUntil([N][N]bool ?R,[N]bool ?phi,?psi,Phi,event !rdy) {
event trdy;
[N][N]bool Rphi;

// compute the transitions Rphi starting in phi
for(i=0..N-1)
for(j=0..N-1)
Rphi[i][j] = R[i][j] & phi[i];

// compute the transitive hull RphiCl of Rphi; i.e. we have
// RphiCl[i][j] :<=> phi[i] -> phi[i_0] -> ... -> phi[i_n] -> [j]
TransHull_OlogN(Rphi,Rphi,trdy);

// compute predecessors of psi[i] under Rphi
for(i=0..N-1)
for(j=0..N-1)
if(Rphi[i][j] & psi[j] | psi[i])
Phi[i] = true;
emit(rdy);
}
drivenby g1 {
// the assignments below construct the following graph:
//
//                 3
//                / \
//               v   v
//    0 -> 1 <-> 2-> 4 <-> 5 <-> 6
//               |         |
//               v         v
//               7<|       8
//               |_|
//
R[0][1] = true;
R[1][2] = true;
R[2][1] = true;
R[2][4] = true;
R[2][7] = true;
R[3][2] = true;
R[3][4] = true;
R[4][5] = true;
R[5][4] = true;
R[5][6] = true;
R[5][8] = true;
R[6][5] = true;
R[7][7] = true;
phi[2] = true;
phi[4] = true;
phi[5] = true;
phi[7] = true;
psi[4] = true;
psi[5] = true;
await(rdy);
for(i=0..N-1)
assert(Phi[i] <-> (i==2 | i==4 | i==5) );
}
drivenby g2 {
// the assignments below construct the following graph:
//
//        >1 -> 2 -> 3 -> 4 -|
//      /                 |__|
//    0           />7 -|
//      \> 5 -> 6   |__|
//                \> 8
//
R[0][1] = true;
R[1][2] = true;
R[2][3] = true;
R[3][4] = true;
R[4][4] = true;
R[0][5] = true;
R[5][6] = true;
R[6][7] = true;
R[6][8] = true;
R[7][7] = true;
phi[0] = true;
phi[1] = true;
phi[2] = true;
phi[4] = true;
phi[6] = true;
phi[7] = true;
phi[8] = true;
psi[3] = true;
psi[5] = true;
await(rdy);
for(i=0..N-1)
assert(Phi[i] <-> (i<=3 | i==5) );
}
```