search

CinRC / IRDC-CCSK

Java implementation of distributed reversible computation verification
https://spots.augusta.edu/caubert/cinrc/
GNU General Public License v3.0
4 stars 2 forks source link

Bug in implementation of simulation #67

Closed aubertc closed 1 year ago

aubertc commented 1 year ago

There is a problem with the implementation of simulation:

https://github.com/CinRC/IRDC-CCSK/blob/4e59d6488557626f3b3c857eaa911014f44acbcd/src/main/java/org/cinrc/parser/LTTNode.java#L59-L93

(I believe that) The issue is that, in case of a "wrong choice", the algorithm does not backtrack to explore other options. We can see it for instance with processes such as a.b + b.a and b.a + a.b (that are obviously equivalent, I mean, bisimilar):

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

Simulations and Bisimulations: 
 ------------

This was spotted by @lanese.

The best fix would probably be to look for an already existing implementation of simulation and to mimick it, as backtracking can be very expensive at times.

aubertc commented 1 year ago

My example was incorrect (it should have been b.a + a.b, not b.a + a.a), but there is a minimal example that I need to dig in the history of my computer.

In the meantime, we can observe that the following fails:

java -jar target/IRDC-4.0.1.0-jar-with-dependencies.jar --equivalence "(b|(a+(d.((b|(a+c))+((b+c)|a)+((a+0)|(b+0)))))), (b|(a+(d.((b|(a+c))+((b+c)|a)+((a+0)|(b+0))))))"

even if it is the same process that is given twice.

aubertc commented 1 year ago

This has been solved.

Bonus:

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

Simulations and Bisimulations: 
 ------------
(((b|(a+d.(((b|(a+c))+((b+c)|a))+((a+0)|(b+0)))))+((b+d.(((b|(a+c))+((b+c)|a))+((a+0)|(b+0))))|a))+((a+d.((b|(a+c))+((b+c)|a)))|(b+d.((b|(a+c))+((b+c)|a))))) ≈ (((b|(a+d.(((b|(a+c))+((b+c)|a))+((a+0)|(b+0)))))+((b+d.(((b|(a+c))+((b+c)|a))+((a+0)|(b+0))))|a))+((a+d.(((b|(a+c))+((b+c)|a))+((a+0)|(b+0))))|(b+d.(((b|(a+c))+((b+c)|a))+((a+0)|(b+0))))))