Updating history by deleting events in it

[aubertc]

As of now, a process doing

a|b ---a[k0]---> a[k0]|b ---b[k1]---> a[k0] | b[k1] ~~a[k0]~> a | b[k1]

will have a different history than a process that does

a|b ---b[k1]-> a | b[k1]

Ideally, we should not be able to distinguish them: this implies, when the k0 key is undone, to "remove the a[k0]" event instead of adding to the history "undo a[k0]".

I hope this is clear enough, it is more of a reminder of our discussion than an actual issue :-)

[aubertc]

In more detail, we have the following:

java -jar target/IRDC-*-with* --interactive "a|b"
------| Actionable Labels |------
[0] a
[1] b
[q] Quit program
------------
(a|b)
Please input the index of the label you'd like to act on:
0
(a|b) -a-> (a[k0].0|b)
------| Actionable Labels |------
[0] [k0]
[1] b
[q] Quit program
------------
(a[k0].0|b)
Please input the index of the label you'd like to act on:
1
(a[k0].0|b) -b-> (a[k0].0|b[k1].0)
------| Actionable Labels |------
[0] [k1]
[1] [k0]
[q] Quit program
------------
(a[k0].0|b[k1].0)
Please input the index of the label you'd like to act on:
1
(a[k0].0|b[k1].0) ~[k0]~> (a|b[k1].0)

java -jar target/IRDC-*-with* --interactive "a|b"
------| Actionable Labels |------
[0] a
[1] b
[q] Quit program
------------
(a|b)
Please input the index of the label you'd like to act on:
1
(a|b) -b-> (a|b[k0].0)

So, we have (a|b[k1].0) vs (a|b[k0].0).

I believe this is more of an issue of the theory, that simply specify "pick a fresh key", and that we cannot really address this issue until we decide which way is "right" (re-using the same key, or simply picking new ones all the time).