Issue with reachability

[aubertc]

The process Tau{a}[k1].Tau{b}[k2] | Tau{b}[k2].Tau{a}[k1] is not reachable (on the left hand, I would have needed to do a then b, but on the right hand I would have needed to do b first).

The implementation somehow feels that something is off, but does not throw an exception:

java -jar IRDC*.jar --interactive "Tau{a}[k1].Tau{b}[k2] | Tau{b}[k2].Tau{a}[k1]"
------| Actionable Labels |------
[0] [k0]
[q] Quit program
------------
(Tau{a}[k0].0|Tau{a}[k0].0)

I guess it's a way of "correcting" the process, but silently changing it is dangerous!