Checking precedence of operators

[aubertc]

Please, make sure that the precedence of operators is actually the one you have implemented, and that my examples make sense.

[peterbro1]

This will be an ongoing investigation. As of right now they are all correct, but it will be important to check (and possibly add a test)

[aubertc]

We assume that the operators have decreasing binding power, in the following order: \a, a., |, +.

The test should be as simple as

"P_0 + P_1 | P_2" should be parsed as "(P_0 + P_1) | P_2", "a.P_0 | P_1" should be parsed as "(a.P_0) | P_1", etc.

[aubertc]

Ideally, it would cover all the combinations:

• a . b | c
• a | b . c
• a \b | c
• a | b \c
• a + b | c
• a | b + c
• a + b \ c
• a \ b + b
• a + b + c (even if in this case there is "nothing" to check: either strategy is fine, we just have to be explicit about it)
• a | b | c (ditto)
• a \ b \c (ditto)
• a.b.c (ditto)

I believe that's it?

[aubertc]

If I am not mistaken, we have a isEquivalent method for labels:

https://github.com/CinRC/IRDC-CCSK/blob/4ec8f4ff0683c217eb49079d21a5cf64bff1d78e/src/main/java/me/gmx/process/nodes/Label.java#L111

I was thinking that a way of testing that would be to create two processes, a + b | c and (a + b) | c, and then to call an isEquivalent method for processes, but actually they are probably internally parsed the same way, so we could "just" check for syntactical equality. But I don't think there is an easy way to do that as of now.

Any thoughts?

[peterbro1]

The isEquivalent method only works for labels (a, 'b, Tau{c,'c}). I think in our case, processes can be of 4 relations with eachother:

• Process p and q can be of no relation, e.g they have nothing to do with eachother
• Process p simulates process q
• Process p and q are bisimulations
• Process p and q are equivalent

In this program's case, equivalency essential means 'equals'. So in this case, p and q can be in bisimulation, but not be equivalent.

[aubertc]

Absolutely. Proving that a + b \a and a+(b\a) are bisimilar would already be a step in the right direction, and we may want to stick to that if we like it / if defining this equivalence is too much work (especially since the benefits are rather slim).

[aubertc]

We can actually state that some process are equivalent to give a good indication that they are correctly parsed:

java -jar target/IRDC-2.4.7.15-jar-with-dependencies.jar --equivalence "a + b\{a}, a+(b\{a})"
[0] (a+b\{a}) => Parsed Successfully.
[1] (a+b\{a}) => Parsed Successfully.

Simulations and Bisimulations: 
 ------------
(a+b\{a}) ≲ (a+b\{a})
(a+b\{a}) ≈ (a+b\{a})
(a+b\{a}) ≲ (a+b\{a})
(a+b\{a}) ≈ (a+b\{a})

[peterbro1]

I'm going to close this issue as completed. The precedence is set in code and is not likely to change

[aubertc]

Yes, I agree we can close it.