Hi,

Firstly, thanks for the creating a great tool

I'm currently in the process of reimplementing the Scribble monitoring runtime (in a different language) for a project I'm working on. This got me thinking about the implementation of parallel scopes.

Essentially, I'm wondering about a protocol such as the following:

  module com.simonjf.scribbletest.Parallel;

  global protocol Parallel(role Role1, role Role2, role Role3, role Role4) {

    A() from Role1 to Role2;

    B() from Role1 to Role2;

    par {

      E() from Role3 to Role4;

      F() from Role4 to Role3;

      C() from Role1 to Role2;

    } and {

      C() from Role1 to Role2;

      D() from Role2 to Role1;

    }

    G() from Role1 to Role2;

  }

This validates and projects fine. (Attached as Parallel.scr)

Suppose we have a trace (attached as paralleltrace.trace) of:

1 -> 2 (A)

1 -> 2 (B)

3 -> 4 (E)

4 -> 3 (F)

1 -> 2 (C)

2 -> 1 (D)

1 -> 2 (C)

1 -> 2 (G)

This fails, as there is nondeterminism after the F message has been received, and the monitor runtime seems to resolve this by using the first scope.

  Simulate: paralleltrace.trace

    SUCCESSFUL: A from Role1 to Role2;

    SUCCESSFUL: B from Role1 to Role2;

    SUCCESSFUL: E from Role3 to Role4;

    SUCCESSFUL: F from Role4 to Role3;

    SUCCESSFUL: C from Role1 to Role2;

    FAILED: D from Role2 to Role1;

    SUCCESSFUL: C from Role1 to Role2;

    FAILED: G from Role1 to Role2;

  ERROR: Simulation failed

Here's the local protocol for Role1:

  local protocol Parallel at Role1(role Role1,role Role2,role Role3,role Role4) {

    A() to Role2;

    B() to Role2;

    par {

      C() to Role2;

    } and {

      C() to Role2;

      D() from Role2;

    }

    G() to Role2;

  }

Similar situations can't arise in, for example, choice blocks due to message label distinction, I think? I'm just wondering whether this is an error at the validation phase (ie, are certain parallel protocols such as the one above disallowed?) or whether it's an error at the monitoring phase. Or have I got the wrong end of the stick completely?

I've tried this with both the released Scribble-0-3 and the 0-4 snapshot from GitHub, current as of 15:45 on 19/01/15. If I haven't got the wrong end of the stick completely, I'll pop an issue on the issue tracker.

Thanks for reading, and I'd really appreciate any insights you have.

Simon