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