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