RE: Proposal for CR108

Per this morning's call, CR108 is closed, but Arthur's suggestion will
become a new issue.

 

AIUI, he is proposing something along the lines of these four new
assertions, which while they may be (I'm still not sure) strictly redundant
with the existing assertions, would provide more intelligible error messages
to users:

 

Add to 2.5.3:

-          If the local name is "input" then the message exchange pattern
MUST have at least one placeholder message with direction "In".

-          If the local name is "output" then the message exchange pattern
MUST have at least one placeholder message with direction "Out".

-          If the local name is "infault" then the message exchange pattern
MUST either have at least one placeholder message with direction "In" and
use the Fault Replaces Message propagation rule, or have no placeholder
message with direction "Out" and use the Message Triggers Fault propagation
rule.

-          If the local name is "outfault" then the message exchange pattern
MUST either have at least one placeholder message with direction "In" and
use the Message Triggers Fault propagation rule, or have at least one
placeholder message with direction "Out" and use the Fault Replaces Message
propagation rule.

 

However, I'm not at all sure the last two are 1) correctly stated, 2) don't
overconstrain the development of extended MEPs, or 3) any less confusing
then what we've got already.

 

Jonathan Marsh -  <http://www.wso2.com> http://www.wso2.com -
<http://auburnmarshes.spaces.live.com> http://auburnmarshes.spaces.live.com

 

  _____  

From: www-ws-desc-request@w3.org [mailto:www-ws-desc-request@w3.org] On
Behalf Of Arthur Ryman
Sent: Wednesday, December 20, 2006 6:39 PM
To: Roberto Chinnici
Cc: www-ws-desc@w3.org; www-ws-desc-request@w3.org
Subject: Re: Proposal for CR108

 


Roberto, 

Thx for the analysis. 

Amy rightly pointed our that the same situation occurs with
MessageLabel-0004 and MessageLabel-0012. 

I was assuming that these assertions applied to the case where there was at
least one message placeholder with a given direction and that they were
defining when the messageLabel was required. Here is my analysis 

Let P = The messageLabel AII is Present. 
Let Q = The MEP has a unique placeholder message with direction equal to the
message direction. 

ML06 = If not(Q) then P. 
ML14 = If not(P) then Q. 

Both of these propositions are equivalent to the symmetrical statement (P or
Q), which translates to: 

The messageLabel AII MUST be present OR the MEP MUST have a unique message
placeholder with direction equal to the message direction. 

However, we have not in fact ensured that there is at least one placeholder
message in the given direction, that my translation is wrong since in that
case 

not(Q) = The MEP has either zero OR more than one placeholder message in the
given direction. 

I propose the following resolution: 

In 2.5.3 Mapping Interface Message Reference's XML Representation to
Component Properties add the following assertion: 

If the local name is input then the MEP MUST have at least one placeholder
message with direction = in. 
If the local name is output the the MEP MUST have at least one placeholder
message with direction = out. 

I agree that we can drop MessageLabel-0004 and keep MessageLabel-0012. 

Similarly, fix up 

2.10.3 Mapping Binding Message Reference's XML Representation to Component
Properties 

the same way. 

We probably have to fix up the Interface Fault Reference and Binding Fault
Reference the same way. 

Arthur Ryman,
IBM Software Group, Rational Division

blog: http://ryman.eclipsedevelopersjournal.com/
phone: +1-905-413-3077, TL 969-3077
assistant: +1-905-413-2411, TL 969-2411
fax: +1-905-413-4920, TL 969-4920
mobile: +1-416-939-5063, text: 4169395063@fido.ca 




Roberto Chinnici <Roberto.Chinnici@Sun.COM> 
Sent by: www-ws-desc-request@w3.org 

12/19/2006 06:20 PM 


To

www-ws-desc@w3.org 


cc

 


Subject

Proposal for CR108

 


 

 





With respect to CR108, I set out to prove that MessageLabel-0006 
(henceforth ML06 for brevity) and MessageLabel-0014 (ML14) are 
equivalent and discovered that they are not.

So now I'm in agreement with Amy on this point and I have a proposal to 
close CR108. But before doing that, I'd like to establish that ML06 and 
ML14 are not equivalent.

------ PART 1. ML14 => ML06 ------

I'm going to show that ML14 implies ML06 (I use "=>" for logical 
implication).

Let's consider the two assertions:

ML06: The messageLabel attribute information item  of a
binding message reference element information item MUST be present if
the message exchange pattern has more than one placeholder message with
{direction} equal to the message direction.

ML14:  If the messageLabel attribute information item  of a
binding message reference element information item is absent then there
MUST be a unique placeholder message with {direction} equal to the
message direction.

Assume <<the message exchange pattern has more than one placeholder
message with {direction} equal to the message direction>>, i.e. the
antecedent of ML06. (#1#)

Now let's assume that the consequent of ML06 is false, i.e. that <<the
messageLabel attribute information item  of a binding message reference
element information item is absent>> (#2#) and derive a contradiction 
from it, (#1#) and ML14.

Applying modus ponens to (#2#) and ML14, we obtain <<there MUST be a 
unique  placeholder message with {direction} equal to the message 
direction>>. This is inconsistent with (#1#).

Consequently, ML14 => ML06.

------ PART 2. ML06 =/=> ML14 ------

Initially I thought that the two were equivalent, but they aren't.
Here's a counterexample that proves that ML06 does not imply ML14.

Consider a binding operation

<operation ref="tns:foo"> (#3#)
    <input />
    <output />
</operation>

whose corresponding interface operation is

<operation name="foo" pattern="myNs:pattern1">
    <output />
</operation>

such that the nyNs:pattern1 MEP (#4#) has no input messages.

You would expect this to be an error, but if you only assume ML06 but 
not ML14, you can't prove it. Why? Because the antecedent of ML06 says 
"if the message exchange pattern has more than one placeholder message 
with {direction} equal to the message direction" and the MEP (#4#) 
doesn't satisfy it (zero is not "more than one").

ML14 catches this case because the MEP (#4#) does not satisfy its 
consequent: <<there MUST be a unique placeholder message with 
{direction} equal to the message direction>> (there isn't one), thus 
making the component model is invalid. So ML06 =/=> ML14.

------ PART 3. PROPOSAL ------

Given that ML14 => ML06, we propose to remove ML06 from the spec as 
redundant.

We should then close CR108 with no further action, indicating that the 
question it raised ("are ML06 and ML14 equivalent?") can be answered 
negatively by the counterexample in part 2 of this message.

Thanks,
Roberto