Curious nesting of tau actions

[aubertc]

java -jar ~/Telechargements/RCCS-Release-2.0.0.jar "(((a+b) | 'b) | 'a)\{a}"
------| Actionable Labels |------
[0] b
[1] 'b
[2] Tau{'b, b}
[3] Tau{'b, Tau{'b, b}}
[4] Tau{'a, a}
------------
(((a+b)|'b)|'a)\{a}
Please input the index of the label you'd like to act on:

Note sure what this [3] Tau{'b, Tau{'b, b}} is, but it definitely should not be here: it seems to suggest that 'b can synchronize with Tau{'b, b}, which is extremely weird.

[aubertc]

Oh, and if I do Tau{'a, a} I cannot undo it ?

Please input the index of the label you'd like to act on:
4
(((a+b)|'b)|'a)\{a} -Tau{'a, a}-> (((Tau{'a, a}[k2].0+b)|'b)|Tau{'a, a}[k2].0)\{a}
------| Actionable Labels |------
[0] 'b
------------
(((Tau{'a, a}[k2].0+b)|'b)|Tau{'a, a}[k2].0)\{a}

[aubertc]

I don't think it fixed the second part of my bug report:.

java -jar target/RCCS-2.0.0.2-jar-with-dependencies.jar "(((a+b) | 'b) | 'a)\{a}"
------| Actionable Labels |------
[0] b
[1] 'b
[2] Tau{'b, b}
[3] Tau{'a, a}
------------
(((a+b)|'b)|'a)\{a}
Please input the index of the label you'd like to act on:
3
(((a+b)|'b)|'a)\{a} -Tau{'a, a}-> (((Tau{'a, a}[k1].0+b)|'b)|Tau{'a, a}[k1].0)\{a}
------| Actionable Labels |------
[0] 'b
------------
(((Tau{'a, a}[k1].0+b)|'b)|Tau{'a, a}[k1].0)\{a}

I should be able of undoing Tau{'a, a}[k1] @peterbro1 .

[aubertc]

I don't think this was fixed…

java -jar target/RCCS-2.0.0.2-jar-with-dependencies.jar "(((a+b) | 'b) | 'a)\{a}"
------| Actionable Labels |------
[0] b
[1] 'b
[2] Tau{'b, b}
[3] Tau{'a, a}
------------
(((a+b)|'b)|'a)\{a}
Please input the index of the label you'd like to act on:
2
(((a+b)|'b)|'a)\{a} -Tau{'b, b}-> (((a+Tau{'b, b}[k0].0)|Tau{'b, b}[k0].0)|'a)\{a}
------| Actionable Labels |------
[0] [k0]
------------
(((a+Tau{'b, b}[k0].0)|Tau{'b, b}[k0].0)|'a)\{a}

I should be able of undoing Tau{'b, b}[k0]!

The bug is definitely with the restrictions, since that process can backtrack just fine if we get rid of the \{a}.

[peterbro1]

I cannot replicate this issue on my machine. From the example you gave, it looks like you are capable of rewinding-- It shows that you have an actionableLabel [k0], which is the tau{b,'b}