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(s) when undoing tau synchronization #76

Closed aubertc closed 1 year ago

aubertc commented 1 year ago

I'm using the dev version IRDC-4.3.5.1.jar, and have a very strange bug:

java -jar IRDC*.jar --interactive "Tau{a}[k1] | Tau{a}[k1].Tau{b}[k2] | Tau{b}[k2]"
------| Actionable Labels |------
[0] [k2]
[1] [k0]
[q] Quit program
------------
((Tau{a}[k0].0|Tau{a}[k0].Tau{b}[k2].0)|Tau{b}[k2].0)
Please input the index of the label you'd like to act on:
1
((Tau{a}[k0].0|Tau{a}[k0].Tau{b}[k2].0)|Tau{b}[k2].0) ~[k0]~> ((a|Tau{a}[k0].Tau{b}[k2].0)|Tau{b}[k2].0)
------| Actionable Labels |------
[0] [k2]
[1] a
[q] Quit program
------------
((a|Tau{a}[k0].Tau{b}[k2].0)|Tau{b}[k2].0)
Please input the index of the label you'd like to act on:
  1. The program renamed the keys, but that's ok.
  2. In ((Tau{a}[k0].0|Tau{a}[k0].Tau{b}[k2].0)|Tau{b}[k2].0), I should not be allowed to undo k0 (since I need to undo k2 first).
  3. If I still decide to undo k0, then only the "left part" of the synchronization is undone

I don't know how those three observations relate, but there's definitely something off!

aubertc commented 1 year ago

Very nice, thanks.