Next: Abstraction and reduction techniques
Up: Finite-state Analysis and Model-checking
Previous: The Model Checking Kit
IF.OPEN is a set of modules for the exhaustive
simulation and validation of IF specifications:
- libifmodel.a : is a library providing an access to
the abstract tree of IF specifications.
- libifsimulator.a : is a library of components
needed for the simulation of IF specifications. It
provides implementation for structures such as
strings, events, labels, etc but also for various kind
of hash-tables.
- if2c : is a program which generates the C
primitives needed for the exhaustive simulation of
IF specifications. Basically, it generates a C type
encoding the state of the system and an iterator
function over states. This C code is intended
to be compiled and linked together with some
specialized application (e.g. generator) to obtain an
executable for the IF specification.
- generator : is a reachability analysis tool of IF
specifications.