- data Atom
- data Formula
- substAtom :: Equalities -> Atom -> Atom
- relabelTIDs :: [TID] -> Formula -> Formula
- hasQuantifiers :: Formula -> Bool
- conjuncts :: Formula -> [Formula]
- conjunctionToAtoms :: MonadPlus m => Formula -> m [Atom]
- isTypingFormula :: Formula -> Bool
- destTypingFormula :: Formula -> Maybe Typing
- atomTIDs :: Atom -> [TID]
- findRole :: TID -> Formula -> Maybe Role
- isaCompr :: IsarConf -> Message -> Doc
- isaUncompr :: IsarConf -> Message -> Doc
- sptAtom :: Mapping -> Atom -> Doc
- isaAtom :: IsarConf -> Mapping -> Atom -> Doc
- isaFormula :: IsarConf -> Mapping -> Formula -> Doc
- sptFormula :: Mapping -> Formula -> Doc
A representable logical atom.
An event must have happened.
|AEvOrd (Event, Event)|
An event order.
A compromised agent variable.
An uncompromised agent variable.
|AHasType MVar (Maybe Type)|
A claim that a variable is of the given type; Nothing stands for weakly-atomic.
A claim that the current state of a protocol is approximated by the given typing.
A claim that the current state is reachable.
A representable logical formula. Currently these are monotonic formula.
Substitute all variables in an atom.
HasType atom will only have its thread identifier substituted, but
not the whole message variable.
Relabel quantified TIDs according to the given list of labels.
Convert a formula consisting of conjunctions only to a list of atoms. Uses
fail for error reporting.
Extract the typing from a singleton well-typedness formula.
Find the first conjoined thread to role equality for this thread, if there is any.