PhaseChangeA  &  NILA  &
 next ( NILA until ( SendA(a) &
  next ( NILA until ( SendA(b) &
   next ( NILA until ( PhaseChangeA &
    next ( always NILA ) )) )) ))      &

PhaseChangeA &
 next ( ~ PhaseChangeA until ( PhaseChangeA &
  next ( always ~ PhaseChangeA )  ))           &

always (  ( NILA | SendA(a) | SendA(b) ) &
          ~ ( NILA & SendA(a) ) &
          ~ ( NILA & SendA(b) ) &
          ~ ( SendA(a) & SendA(b) ) 
       )                                       &

~ sometime ( PhaseChangeA  &
             next (  ( ~ ( SendA(b) & next ( NILA until PhaseChangeA ) ) )
                     until
                     PhaseChangeA
                  )
           )