search

nuscr / oven

A tool for handling Synthetic MPST specifications
1 stars 0 forks source link

Weak bisimulation is not really working #6

Closed fferreira closed 2 years ago

fferreira commented 2 years ago

global Borked(role A, role B, role C, role D) { par {A() from A to B;} and { B() from C to D;} }

This should not be a violation because the states are weakly bisimilar

sungshik commented 2 years ago

The following protocol is equivalent (explicit choice instead of par) and gives the same error:

global Borked1(role A, role B, role C, role D) {
  choice {
    A() from A to B;
    B() from C to D;
  } or {
    B() from C to D;
    A() from A to B;
  }
}

The following protocol gives an error, but a different one:

global Borked2(role A, role B, role C, role D) {
  choice {
    A() from A to B;
  } or {
    B() from C to D;
    A() from A to B;
  }
}

The projection on A differs only in a trailing tau in the first alternative (present in Borked1, absent in Borked2).

Hypothesis based on these two examples: there's an issue with trailing taus in the computation of ==>.

fferreira commented 2 years ago

Borked and Borked1 are accepted now.

For the last one: My understanding is that Borked2 is not C2-well behaved because for D, it can weakly step to the end, and the start and end states are not weakly bisimilar (the start can receive or end). Question 1: is this understanding correct? Question 2: this is also a C1 violation, no?

sungshik commented 2 years ago
  1. Yes (same is true for C)
  2. Nope. C1 demands that if a state has a (strong) transition, then it is not final. Every state in every projection satisfies this.
fferreira commented 2 years ago

Solved a while ago. This issue is stale