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] |
non-deterministic automata with epsilon transitions
|
| SNFA [Automata] |
symbolic non-deterministic 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 |