GossipS5 transformer yields wrong results

[m4lvin]

With four agents (called 0 to 3), after calls 01 and 12 we expect agent 2 to know that agent 0 has secret 1 (because 1 knows secret 0, and cannot have learned it via 3 because 1 does not know 3).

However, currently we get:

stack ghci src/SMCDEL/Examples/GossipS5.hs
λ> after 4 [(0,1),(1,2)] |= K "2" (PrpF $ hasSof 4 0 1)
False

The same example in GoMoChe gives:

stack ghci
λ> (totalInit 4, parseSequence "01;12") |= K 2 anyCall (S 0 1)
True

Thanks to @Pathemeous for finding this.

[m4lvin]

In some sense even more worrying is the example with S 1 0 at the end:

λ> after 4 [(0,1),(1,2)] |= K "2" (PrpF $ hasSof 4 1 0)
False

vs GoMoChe:

λ> (totalInit 4, parseSequence "01;12") |= K 2 anyCall (S 1 0)
True