search

Pathemeous / Symbolic-Gossip

Symbolic Model Checker for the Gossip Problem
GNU General Public License v2.0
2 stars 0 forks source link

Possible Bug: Classic Transformer Test case is evaluated wrongly #13

Open Pathemeous opened 3 months ago

Pathemeous commented 3 months ago

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` True

Tested on both SMCDEL and our own project, both return false.

Pathemeous commented 3 months ago

Code part of SMCDEL, and issue tracked at https://github.com/jrclogic/SMCDEL/issues/48.