Since you asked for my opinion specifically, here is what I am thinking (following your convention, I'm also attaching a .txt file, in case the e-mail itself has any wrapping problems):

I think that each of these iterations has made the trace based approach more promising.  On the other hand, I'm still not sure we've turned the corner to where we have a presentation that I believe would be simple and comprehensible, especially for novice readers.  The choices are exactly the ones you've outlined at the end: go back to the status quo, or keep working on this.  I am willing to put a little more effort into exploring this option, if you are, but I still think we have to assume the status quo until this approach reaches a level of polish where everybody feels good about it.

It feels to me like the right balance might be to use some of the formalism, but not to carry it all the way down to the properties.  Would it makes sense to do something like the following:

* Outline the traces on the wire using the algebraic notation, more or less as you have been proposing right along.  Do not include the local state properties at this level.

* Describe each state with a triple.  This would be a simple English state name such as "Sending Request" as we have today (I like this better than S1, S2), a list of the trace fragments that characterize the inbound edges, and an informal English description.  See below for an illustration.

* Keep the named typed properties and operational descriptions that we have in our existing working draft.  Put these in a table immediately below the triple.  The result would be something along the lines of:

      *************************Description of State "Sending Request"********************
	State name: Sending Request
	Traces leading to this state: 
		   eoReq.S2 +                      //Finished sending Request
     		  !soResp.receiving.S3 +           //Start of overlapping response
                  !channelfail.Fail +              //Channel/media failure
                  !localException.Fail             //Local Timeout or reason to abort
 	Description:  Requesting node begins transmission of request

     =========================================================================================
    | Next State   |       Action                                                            |
    |   Fail       |   Set "transport:FailureReason" to "transmissionFailure"                |
    |   Waiting    |                                                                         |
     =========================================================================================
      *************************End Description of State "Sending Request"*****************

I don't think the actual traces line up with the action illustrated, but the idea is that the traces would illustrate the different means by which one can enter the state.

I still feel like I'm missing something, but I'm trying to put in enough plain English and formatting, and put the traces in a context where even novices will have a sense of their purpose.  I think I would find something like this easier than:  

!soHTTPResp(status==200,responder=x).setProperty(transport:ImmediateSender=x
).
         receiving.SentAndReceiving
      +
!soHTTPResp(status==202,responder=x).setProperty(transport:ImmediateSender=x
)....
      +
!soHTTPResp(status==500,responder=x).setProperty(transport:FaultHint,true).
        setProperty(transport:ImmediateSender=x).SentAndReceiving
	+ !soHTTPResp(
	+ ...

Are we making progress?  Thanks very much.