Bisimulation relation wrong way round
When checking for bisimulation, the reported relation has its pairs inverted.
So if I have:
P=(a->(b->c ->P|
b -> c -> P)).
Q = (a -> b -> R |
a -> b -> R),
R = (c -> Q).
And I check bisimulation between P and Q (the order of selection is important) I get
Models P and Q are (STRONG) bisimilar.
Bisimulation relation:[(0,0), (1,1), (2,2), (2,3), (3,1)]
But I should get the pairs inverted:
Models P and Q are (STRONG) bisimilar.
Bisimulation relation:[(0,0), (1,1), (2,2), (3, 2), (1, 3)]