Obtaning proof of non-simulation

[aubertc]

This is a follow-up of the discussion started at https://github.com/CinRC/IRDC-CCSK/issues/33.

Is there an easy way to output the strategy the program found to assert that two processes were not in capacity of simulating each other?

For instance, consider

p = a.((b.c) + (b.d))
q = a.b.(c+d)

Then, p cannot simulate q, because q can "trick" p by doing a, then b (and at this moment p needs to make a choice), and then q can pick c or d, while p is forced to follow the choice it made previously.

Is there an easy way to compute, and then picture / present this?

[peterbro1]

Closed as complete in latest release, using --equivalence flag

[peterbro1]

[0] a0.(b1.c2+b3.d4) => Parsed Successfully. [1] a0.b1.(c2+d3) => Parsed Successfully.

Simulations and Bisimulations:

a0.(b1.c2+b3.d4) ≲ a0.b1.(c2+d3)

Process finished with exit code 0

[aubertc]

It's something slightly more subtle than that: can we output any information when there is no simulation?

For instance, as of now we have:

java -jar target/IRDC-4.1.1.1-jar-with-dependencies.jar --equivalence "a.((b.c)+(b.d)), a.b.(c+d)"
[0] a.(b.c+b.d) => Parsed Successfully.
[1] a.b.(c+d) => Parsed Successfully.

Simulations and Bisimulations: 
 ------------
a.(b.c+b.d) ≲ a.b.(c+d)

This improvement is asking the program to output something explaning why a simulation the other way around does not work (a strategy to trick one process). Something along the lines of:

Both processes can do a then b, but then the first must do either c or d, while the other one can do both.

This is a complicated issue :-)