Open
Description
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.