smcdel-1.3.0: Symbolic Model Checking for Dynamic Epistemic Logic
Safe HaskellSafe-Inferred
LanguageHaskell2010

SMCDEL.Examples.Prisoners

Documentation

n :: Int Source #

light :: Form Source #

prisonExpStart :: KripkeModelS5 Source #

prisonGoal :: Form Source #

prisonAction :: ActionModelS5 Source #

prisonInterview :: Int -> MultipointedActionModelS5 Source #

data Story a b Source #

Constructors

Story a [b] 

Instances

Instances details
(Update a b, Optimizable a, TexAble a, TexAble b) => TexAble (Story a b) Source # 
Instance details

Defined in SMCDEL.Examples.Prisoners

Methods

tex :: Story a b -> String Source #

texTo :: Story a b -> String -> IO () Source #

texDocumentTo :: Story a b -> String -> IO () Source #

pdfTo :: Story a b -> String -> IO () Source #

disp :: Story a b -> IO () Source #

svgViaTex :: Story a b -> String Source #

endOf :: (Update a b, Optimizable a) => Story a b -> a Source #

prisonExpStory :: Story PointedModelS5 MultipointedActionModelS5 Source #

prisonSymStart :: MultipointedKnowScene Source #

wasInterviewed :: Int -> Form Source #

isNowInterviewed :: Int -> Form Source #

lightSeenByOne :: Form Source #

prisonSymEvent :: KnowTransformer Source #

prisonSymInterview :: Int -> MultipointedEvent Source #

prisonSymStory :: Story MultipointedKnowScene MultipointedEvent Source #