scyther-proof-0.3.0: Automatic generation of Isabelle/HOL correctness proofs for security protocols.



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



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.

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

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

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

Is the relation cyclic.