Question about choice projection

[simonjf]

Hi,

I'm working on encoding some behaviour which, abstracted, takes the following form:

global protocol ChoiceProjectionTest(role A, role B, role C) {

  rec Rec {

    Msg1() from A to B;

    choice at B {

      Msg2() from B to A;

    } or {

      Msg3() from B to A;

      continue Rec;

    }

    Msg4() from A to C;

    Msg5() from C to A;

    continue Rec;

  }

}

Essentially, we have two branches, one of which recurses, and one which doesn't, and a message is sent to a third role after this choice block has completed. Now, the local projections for roles A and B are as expected:

local protocol ChoiceProjectionTest at A(role A,role B,role C) {

  rec Rec {

    Msg1() to B;

    choice at B {

      Msg2() from B;

    } or {

      Msg3() from B;

      continue Rec;

    }

    Msg4() to C;

    Msg5() from C;

    continue Rec;

  }

}

local protocol ChoiceProjectionTest at B(role A,role B,role C) {

  rec Rec {

    Msg1() from A;

    choice at B {

      Msg2() to A;

    } or {

      Msg3() to A;

      continue Rec;

    }

    continue Rec;

  }

}

But the projection for C seems strange:

local protocol ChoiceProjectionTest at C(role A,role B,role C) {

  rec Rec {

    choice at B {

      continue Rec;

    }

    Msg4() from A;

    Msg5() to A;

    continue Rec;

  }

}

For some reason, the choice block is present in the projection for C, even though it's not involved in that choice at all.

I couldn't find any well-formedness restrictions that I'd be violating in the Scribble spec, so any insights would be greatly appreciated. Apologies if I'm missing something totally obvious. I've tried this both on the 0.3 release, and the 0.4 snapshot from Git HEAD.

Thanks!

[objectiser]

This is most likely a bug, so best to create a report in https://issues.jboss.org/browse/SCRIBBLE.

Regards

Gary

[objectiser]

Hi Simon

This is the response from Ray Hu:

"This protocol is not intended to be well-formed because Scribble currently only supports "tail-recursive" protocols.  The segment between A and C is not allowed to follow the choice between A and B containing the first "continue Rec" within the scope of the "Rec" recursion.

Taking a "tail-recursive" interpretation of the protocol:

   "Some number (possibly zero) of (Msg1; Msg3) exchanges, followed by

    a (Msg1; Msg2) exchange, followed by

    a (Msg4; Msg5) exchange, and repeat from start"

can be written (with a small addition)

   rec X {

     Msg1() from A to B;

     choice at B {

       Msg2() from B to A;

       Msg4() from A to C;

       Msg5() from C to A;

       continue X

     } or {

       Msg3() from B to A;

       Msg6() from A to C;  // Added message to make choice well-formed

       continue X;

     }

   }

Msg6 has been added to make the global choice between A, B and C well-formed according to the current (conservative) conditions for choice well-formedness.

Well-formedness validation has not yet been fully completed in this branch of the Scribble tool implementation -- it is currently being implemented in a separate fork, to be merged into the main branch within a few weeks."

We can discuss this more at the Scribble meeting next week. I'll leave the jira open for now.