smcdel-1.3.0: Symbolic Model Checking for Dynamic Epistemic Logic

Safe Haskell	Safe-Inferred
Language	Haskell2010

SMCDEL.Examples.DiningCrypto

Synopsis

dcScnInit :: Int -> (Bool, Bool, Bool) -> KnowScene
dcScn1 :: KnowScene
someonepaid :: Form
notwopaid :: Form
reveal :: Int -> Form
dcScn2 :: KnowScene
everyoneKnowsWhetherNSApaid :: Form
nobodyknowsWhoPaid :: Form
dcCheckForm :: Form
dcValid :: Bool
genDcSomeonepaid :: Int -> Form
genDcNotwopaid :: Int -> Form
genDcKnsInit :: Int -> KnowStruct
genDcEveryoneKnowsWhetherNSApaid :: Int -> Form
genDcReveal :: Int -> Int -> Form
genDcNobodyknowsWhoPaid :: Int -> Form
genDcCheckForm :: Int -> Form
genDcValid :: Int -> Bool

Documentation

dcScnInit :: Int -> (Bool, Bool, Bool) -> KnowScene Source #

dcScn1 :: KnowScene Source #

someonepaid :: Form Source #

notwopaid :: Form Source #

reveal :: Int -> Form Source #

dcScn2 :: KnowScene Source #

everyoneKnowsWhetherNSApaid :: Form Source #

nobodyknowsWhoPaid :: Form Source #

dcCheckForm :: Form Source #

dcValid :: Bool Source #

genDcSomeonepaid :: Int -> Form Source #

genDcNotwopaid :: Int -> Form Source #

genDcKnsInit :: Int -> KnowStruct Source #

Initial structure for Dining Cryptographers (complete graph!)

genDcEveryoneKnowsWhetherNSApaid :: Int -> Form Source #

genDcReveal :: Int -> Int -> Form Source #

genDcNobodyknowsWhoPaid :: Int -> Form Source #

genDcCheckForm :: Int -> Form Source #

genDcValid :: Int -> Bool Source #