A  
AVL [Sets] 
sets as binary balanced trees (i.e., OCaml stdlib)

Automata 
Types for the various kind of manipulated automata

B  
BFS [Queues]  
Bdd 
Binary Decision Diagrams (BDDs)

C  
Common 
Common definitions and utilities

Congruence 
congruence closure algorithm, for the `up to congruence' variant
of the algorithms

D  
DFS [Queues]  
Determinisation 
Symbolic determinisation

Dup [Sets] 
duplicator, to check the consistency of one implementation w.r.t.

E  
Epsilon 
Symbolic epsilon removal

I  
IntSet [Common] 
efficient implementation of sets of integers

M  
Make [Safa] 
Symbolic equivalence check, using queues
Q

Make [Congruence]  
Map [Sets.T]  
N  
NarithInlined [Sets] 
sets as large integers, without Z

O  
OList [Sets] 
sets as ordered lists

Q  
Queues 
Various implementations of queues

R  
RFS [Queues]  
S  
SDFA [Automata] 
symbolic deterministic automata

SENFA [Automata] 
nondeterministic automata with epsilon transitions

SNFA [Automata] 
symbolic nondeterministic automata

Safa 
Symbolic algorithms for language equivalence

Set [Common] 
(not so efficient) implementation of polymorphic sets

Sets 
Sets of integers

Small [Sets] 
sets as integers (so that elements have to be really small)

Span [Common] 
spans: sparse polymorphic maps indexed by
'v
these maps are used to represent explicit part of the
transitions of guarded string automata

Stats 
Simple module to record statistics, by profiling

T  
Trace 