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

[m4lvin]

Some notes which things might be relevant.

To show the action model equivalent to the call transformer event:

stack ghci src/SMCDEL/Examples/GossipS5.hs src/SMCDEL/Translations/S5.hs
import SMCDEL.Examples.GossipS5
import SMCDEL.Internal.TexDisplay
disp $ eventToAction $ call 3 (0,1)

Why does this contain 8 actions for the 3 agents case? There are only 3 possible calls!

To explain the vocabulary:

explain :: Int -> Prp -> String
explain n (P k) = "S_" ++ show a ++ "_" ++ show b where
  a = k `div` n
  b = k - (n * a)

mapM (print .  (\p -> show p ++ ": " ++ explain 4 p)) $ vocabOf $ after 4 []

After looking at the factual change BDDs in callTrf 4 they seem alright 🤔