m4lvin/gomoche

🗣️📞 Gossip Model Checking

GoMoChe - Gossip Model Checking

A Haskell tool to analyse (dynamic) gossip protocols, including an epistemic model checker.

Getting Started

Option A: For a quick try-out, click here to use GoMoChe in your browser via GitPod, wait and use the terminal there.

Option B: To use GoMoChe locally, you need the Haskell Tool Stack. Then do stack build and stack ghci inside this folder.

Usage Examples

List all call sequences permitted by the protocol lns on the graph threeExample defined in the module Gossip.Examples:

GoMoChe> mapM_ print $ sequences lns (threeExample,[])
[(0,1),(0,2),(1,2)]
[(0,1),(1,2),(0,2)]
[(0,1),(2,1),(0,2)]
[(1,2),(0,1)]
[(2,1),(0,1)]

Count how many of these call sequences are successful and unsuccessful:

GoMoChe> statistics lns (threeExample,[])
(3,2)

The same, for another gossip graph given in short notation:

GoMoChe> statistics lns (parseGraph "01-12-231-3 I4",[])
(57,20)

Evaluate a formula at a gossip state:

GoMoChe> eval (threeExample,[(0,1)]) (S 1 0)
True
GoMoChe> eval (threeExample,[(0,1)]) (S 1 2)
False
GoMoChe> eval (threeExample,[(0,1)]) (K 2 anyCall (S 1 0))
True
GoMoChe> eval (threeExample,[(0,1)]) (K 2 lns (S 1 0))
True
GoMoChe> eval (threeExample,[(0,1),(1,2)]) (S 0 2)
False
GoMoChe> eval (threeExample,[(0,1),(1,2)]) (S 2 0)
True

If you have graphviz installed, you can visualize gossip graphs like this:

GoMoChe> dispDot $ diamondExample

Also execution trees can be visualized, for example:

GoMoChe> dispTreeWith [2] 2 1 lns (tree lns (nExample,[]))

Note: In GitPod, use pdf and pdfTreeWith instead of dispDot and dispTreeWidth.

Tests

The file test/results.hs contains a test suite that also covers most examples. You can run it with stack clean; stack test --coverage.

References

• Hans van Ditmarsch, Malvin Gattinger, Louwe B. Kuijer, Pere Pardo: Strengthening Gossip Protocols using Protocol-Dependent Knowledge In: Journal of Applied Logics - IfCoLog Journal of Logics and their Applications, Volume 6, Number 1, 2019.

• Chapter 6 "Dynamic Gossip" in Malvin Gattinger: New Directions in Model Checking Dynamic Epistemic Logic PhD thesis at ILLC, University of Amsterdam, 2018.

• Hans van Ditmarsch, Jan van Eijck, Pere Pardo, Rahim Ramezanian, François Schwarzentruber: Dynamic Gossip. In: Bulletin of the Iranian Mathematical Society (BIMS), 2018. https://doi.org/10.1007/s41980-018-0160-4

• Hans van Ditmarsch, Jan van Eijck, Pere Pardo, Rahim Ramezanian, François Schwarzentruber: Epistemic protocols for dynamic gossip. In: Journal of Applied Logic, Volume 20, 2017, Pages 1-31, https://doi.org/10.1016/j.jal.2016.12.001

Other Tools

• ElmGossip: Explore dynamic gossip in your browser by Ramon Meffert https://github.com/RamonMeffert/elm-gossip

gomoche's Issues

Find out if Data.Sequence can improve performance

Using [Call] for histories might be a bottleneck.

See for example https://stackoverflow.com/questions/9611904/haskell-lists-arrays-vectors-sequences

wrong epistAlt results in ASync version

The definition of epistAlt for the asyncrhonous setting contains sequences which should not be considered.

λ> totalBound 
5
λ> mapM_ (\(_,_,s) -> putStrLn (charSequence  s)) $ epistAlt 0 (wlog anyCall) (ASync, totalInit 4, parseSequence "ab;bc;cd;ad;ab")
ab;cd;ad;ab
cd;ab;ad;ab
ab;bc;bd;ad;ab
ab;bc;cd;ad;ab
ab;bd;cd;ad;ab
ab;cd;ad;ab;bc
ab;cd;ad;ab;bd
ab;cd;ad;ab;cd
ab;cd;ad;bc;ab
ab;cd;ad;bd;ab
ab;cd;ad;cd;ab
ab;cd;bc;ad;ab
ab;cd;bd;ad;ab
ab;cd;cd;ad;ab
cd;ab;ad;ab;bc
cd;ab;ad;ab;bd
cd;ab;ad;ab;cd
cd;ab;ad;bc;ab
cd;ab;ad;bd;ab
cd;ab;ad;cd;ab
cd;ab;bc;ad;ab
cd;ab;bd;ad;ab
cd;ab;cd;ad;ab
cd;cd;ab;ad;ab
λ> knowledgeOverview (ASync, totalInit 4, parseSequence "ab;bc;cd;ad;ab") (wlog anyCall)
    a           b           c           d     
ab  ab         ab           c           d     
bc  ab         abc        abc           d     
cd  ab         abc        abcd   CD  abcd   CD
ad  abcd A  D  abc        abcd   CD  abcd A CD
ab  abcd AB D  abcd AB    abcd   CD  abcd A CD
λ> knowledgeOverview (ASync, totalInit 4, parseSequence "cd;ab;ad;ab") (wlog anyCall)
    a           b           c           d     
cd  a           b           cd         cd     
ab  ab         ab           cd         cd     
ad  abcd A  D  ab           cd       abcd A  D
ab  abcd AB D  abcd AB      cd       abcd A  D

Improve documentation and use haddock

Ideally also generate haddock with CI and make it available.