Theory.Model.Atom

Formulas that represent security properties.

Atoms

data Atom t

Atom's are the atoms of trace formulas parametrized over arbitrary terms.

Constructors

Action t (Fact t)

EqE t t

Less t t

Last t

Instances

Functor Atom

Typeable1 Atom

Foldable Atom

Traversable Atom

Apply BLAtom

Apply LNAtom

Eq t => Eq (Atom t)

Data t => Data (Atom t)

Ord t => Ord (Atom t)

Show t => Show (Atom t)

Binary t_1627458332 => Binary (Atom t_1627458332)

NFData t_1627458332 => NFData (Atom t_1627458332)

HasFrees t => HasFrees (Atom t)

type NAtom v = Atom (VTerm Name v)

LAtom are the atoms we actually use in graph formulas input by the user.

type LNAtom = Atom LNTerm

LAtom are the atoms we actually use in graph formulas input by the user.

isActionAtom :: Atom t -> Bool

True iff the atom is an action atom.

isLastAtom :: Atom t -> Bool

True iff the atom is a last atom.

isLessAtom :: Atom t -> Bool

True iff the atom is a temporal ordering atom.

isEqAtom :: Atom t -> Bool

True iff the atom is an equality atom.

LFormula

type BLAtom = Atom BLTerm

Atoms built over BLTerms.

Pretty-Printing

prettyNAtom :: (Show v, HighlightDocument d) => NAtom v -> d