| Location |
Locations of the elements in a source file
|
| Error |
Module for printing errors
|
| Trace |
Debug module,
functions for trace and internal errors
|
| Abstract |
Abstract syntax for protocol specifications
|
| Symbols |
Manage the abstract data type of symbols of the protocol specifications
|
| Termutil |
Utilities for term replacement in abstract protocol specifications
|
| Alias |
Control and replacement of alias symbols in terms and
protocol specifications.
|
| Types |
Module for type checking and type convertion
|
| Translator |
Module for checking a specification in abstract syntax, and translating a specification a la BAN (several processes in a single message list)
into a multi processes specification.
|
| Pp |
Iterator functions used in pretty printers
|
| Debugpp |
Dump specifications in abstract syntax for
debugging puposes.
|
| Evapp |
Pretty print a specification in abstract syntax into
a LAEVA concrete syntax,
with additional constructions for definition
of separate processes.
|
| Evaparse | |
| Evalex |
Lexical analyser for protocol specifications in LAEVA concrete syntax
|