It seems there might be a bug in the classical transformer as implemented in SMCDEL.
In the setting of 4 (or more) agents we should have:
$$01;12 \models K_2 S_10$$
because $1$ shared the secret of $0$ with $2$ in the second call, allowing $2$ to infer that the previous call was $01$ hence the call effects lead to $S_10$.
it "ClsTrf 1: agents can reason about other agents' knowledge 1" $ do
eval (after 4 [(0,1),(1,2)]) (K "2" (has 4 1 0)) `shouldBe` TrueTested on both SMCDEL and our own project, both return false.
It seems there might be a bug in the classical transformer as implemented in SMCDEL.
In the setting of 4 (or more) agents we should have:
$$01;12 \models K_2 S_10$$ $1$ shared the secret of $0$ with $2$ in the second call, allowing $2$ to infer that the previous call was $01$ hence the call effects lead to $S_10$ .
because
Tested on both SMCDEL and our own project, both return false.