tamarin-prover-utils- Utility library for the tamarin prover.

MaintainerSimon Meier <iridcode@gmail.com>
Safe HaskellSafe-Inferred




Simple vertice list based representation of DAGs and some common operations on it.


Computing with binary relations

type Relation a = [(a, a)]Source

A relation represented as a list of tuples.

inverse :: Relation a -> Relation aSource

The inverse of a Relation.

image :: Eq a => a -> Relation a -> [a]Source

The image of an element under a Relation.

reachableSet :: Ord a => [a] -> [(a, a)] -> Set aSource

Compute the set of nodes reachable from the given set of nodes.

restrict :: Eq a => (a -> Bool) -> Relation a -> Relation aSource

Restrict a relation to elements satisfying a predicate.


dfsLoopBreakers :: Ord a => [(a, a)] -> [a]Source

Compute a minimal set of loop-breakers using a greedy DFS strategy. A set of loop-breakers is a set of nodes such that removing them ensures the acyclicity of the relation. It is minimal, if no node can be removed from the set.

cyclic :: Ord a => [(a, a)] -> BoolSource

Is the relation cyclic.

toposort :: Ord a => [(a, a)] -> [a]Source

Produce a topological sorting of the given relation. If the relation is cyclic, then the result is at least some permutation of all elements of the given relation.