Test matrix for reply rules

Last week, Umit suggested I produce a set of test cases to help clarify 
the rules in section 3.2 (and whatever else they pull in by reference).  
While I didn't think that was necessary to make the immediate point I 
was trying to make, I think it could be very useful in focusing the 
overall discussion.

For our purposes here, there are essentially 5 headers whose presence or 
absence matters: [destination], [action], [reply endpoint], [fault 
endpoint], [message id].  There are other possibilities to consider, for 
example the case of a [relationship] that already contains a reply 
relationship, but I won't consider them here.  It also doesn't matter 
here whether a reply or fault endpoint is anonymous or even valid, and 
I'm not considering transport-level failures and similar faults.  These 
all need to be considered, but they are also an issue outside the 
context of formulating a reply.

To this end, I'll model the rules in terms of what MAPs the receiver 
generates, as opposed to what might get delivered where.  In this view, 
the rules are a function taking an incoming message and producing one of 
the following constraints:

    * The receiver MUST generate a response message (is that the right
      term?) with given MAPs.
    * The receiver MUST generate a fault message with given MAPs and
      given fault.
    * The receiver may generate whatever it likes.

So for each of the 32 possible inputs, we need to specify exactly what 
constraints the rules produce.  I'm deliberately saying "constraints" 
and not "behavior" here.  It's fine if we don't constrain behavior in 
some cases -- in fact, we know we want this in the case where none of 
the properties has a value -- but we need to be able to say 
unequivocally that that's the case.  There's a world of difference 
between "definitely not constrained" and "not definitely constrained".

In a capricious attempt to apply the math part of my math/CS degree, 
I'll try to define a few auxiliary functions.  In a nod to the CS half, 
I'll give them long names instead of single italic letters and use 
not-completely-rigorous notation.  I'll use () to designate an undefined 
or empty value.  I've bolded places where I wasn't sure how to translate 
the spec.

    * EffectiveResponseEndpoint(MAPs) =
          o [reply endpoint] if [reply endpoint] is defined
          o else UnknownDestination
    * EffectiveFaultEndpoint(MAPs) =
          o EffectiveResponseEndpoint(MAPs) if [fault endpoint] == ()
          o else [fault endpoint]
    * EffectiveDestination(MAPs, responseType) =
          o EffectiveResponseEndpoint(MAPs) if the reply is a normal
            response
          o EffectiveFaultEndpoint(MAPs) if the reply is a fault

    * UnknownDestination() =
          o *either (), an EPR with anonymous address and nothing else,
            or something transport-specific*

    * ReplyRelationship(MAPs) =
          o (replyURI, [message id]) if [message id] is defined
          o () otherwise

    * AddReply(relationship, newRel) =
          o relationship, if newRel = ()
          o *else whatever we mean when we say "a new pair of IRIs is
            added to this value", which in turn depends on whether we
            view this list of ordered pairs as a relation, a function,
            or just a list of ordered pairs.*

    * Reply(MAPs, responseType) is defined by
          o [destination] = EffectiveDestination(MAPs, responseType)
          o [action] =
                + http://www.w3.org/2005/03/addressing/fault if
                  responseType is-a FAULT and the fault is a WSA fault
                + else unconstrained
          o [relationship] = AddReply([relationship],
            ReplyRelationship(MAPs))
          o [reply endpoint] unconstrained
          o [fault endpoint] unconstrained
          o [message id] != (), otherwise unconstrained

Unconstrained() means no constraint on MAPs at all.

I believe the current consensus on what the rules /ought to mean/ is 
given by

    * All MAPs = () => Unconstrained()
    * [reply endpoint] = () => Reply(MAPs, NO REPLY ENDPOINT FAULT)
    * [reply endpoint] != ()
          o [destination] = () or [action] = () or [message id] = () =>
            Reply(MAPs, MISSING MAP FAULT)
          o else Reply(MAPs, RESPONSE)

Note that if the reply endpoint is missing, but a fault endpoint is 
present, the fault will go there, by the rules above.  Otherwise, the 
outbound [destination] is undefined.  Note also that section 3.2 is a 
bit looser -- it specifically doesn't say what happens if there is no 
[reply endpoint] but there is a [fault endpoint], because the second 
clause of rule 1 is specifically marked "otherwise".

On the other hand, the current formulation /might well mean:
/

    * All of [destination], [action], [reply endpoint] and [message id]
      defined => Reply(MAPs, RESPONSE)
    * Unconstrained() otherwise

The a la carte rules are given by the single rule

    * ALaCarte(MAPs, responseType)

where ALaCarte(MAPs, responseType) is a simpler version of Reply(MAPs, 
responseType)

    * [destination] = EffectiveDestination(MAPs, responseType)
    * [action] unconstrained
    * [relationship] = AddReply([relationship], ReplyRelationship(MAPs))
      (if [message id] is missing, this ends up being the original
      [relationship])
    * [reply endpoint] unconstrained
    * [fault endpoint] unconstrained
    * [message id] unconstrained

In any of these case, the full 32-case table can be produced 
mechanically, with assertions based on everything that's not 
"unconstrained".  To take a couple of somewhat random examples:

If {[destination], [action], [reply endpoint]} are defined:

    * Under the "ought to mean" rules:
          o [destination] = [fault endpoint]
          o [action] = http://www.w3.org/2005/03/addressing/fault
          o [relationship] = AddReply([relationship], (replyURI,
            [message id]))
          o all other MAPs unconstrained
    * Under the "might well mean" rules, Unconstrained()
    * Under the "a la carte" rules:
          o [destination] = [reply endpoint]
          o [relationship] = [relationship]
          o all other MAPs unconstrained

If {[destination], [action], [fault endpoint], [message id]} are defined:

    * Under the "ought to mean" rules:
          o [destination] = [fault endpoint]
          o [action] = http://www.w3.org/2005/03/addressing/fault
          o [relationship] = AddReply([relationship], (replyURI,
            [message id]))
          o all other MAPs unconstrained
    * Under the "might well mean" rules, Unconstrained()
    * Under the "a la carte" rules:
          o [destination] = UnknownDestination()
          o [relationship] = AddReply([relationship], (replyURI,
            [message id]))
          o all other MAPs unconstrained