tamarin-prover-theory- Term manipulation library for the tamarin prover.

PortabilityGHC only
MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellNone



Conversion of the graph part of a sequent to a Graphviz Dot file.



nonEmptyGraph :: System -> BoolSource

True iff the dotted system will be a non-empty graph.

dotSystemLoose :: System -> Dot ()Source

Convert the sequent to a Dot action representing this sequent as a graph in the GraphViz format. The style is loose in the sense that each premise and conclusion gets its own node.

dotSystemCompact :: BoringNodeStyle -> System -> Dot ()Source

Dot a sequent in compact form (one record per rule), if there is anything to draw.

compressSystem :: System -> SystemSource

Unsound compression of the sequent that drops fully connected learns and knows nodes.

data BoringNodeStyle Source

The style for nodes of the intruder.