Documentation

Manual

The complete manual is still not available yet. A first draft is currently available in the v0.3beta (and above) and it will be improved in future releases.

Installation

APTE was implemented in Ocaml hence you need to install it first before trying to install APTE. For MacOS X users, you need Xcode, which is available on the MacAppStore of Apple (it is free).

To install APTE, first reach the extracted directory then enter the following commands:

$ cd Source

$ make

Once the installation is done, an executable ‘apte’ is created in the extracted directory

Usage

Synopsis :


apte [-debug high|low|none] [-unfold] [-no_comm] [-no_erase] [-verbose [<int>]] [-display size|step] [-log <int>] file

Options :

  • -debug [high|low|none] : APTE is programmed with three level of debugging.
    • The High debugging option checks several invariants of the algorithms. While this option provides more guarantees about the result, it makes the algorithm slower.
    • The Low debugging option only checks basic invariants. (default)
    • The None debugging option does not check any invariant. Select this option for optimal running time.
  • -display step : Show statistics on the matrices generated by APTE for each main step of the algorithm.
  • -display size : Group the statistics on the matrices generated by the size traces.
  • -log <int> : Log all the symbolic processes and the matrices obtained on the leaves for all traces of size smaller than or equal to <int>.
  • -no_comm : Does not consider the internal communication in the trace equivalence.

    WARNING : This option should not be used in presence of private channel.
  • -no_erase : Does not consider a slight optimisation that consists of removing symbolic processes with the same process during the execution of the algorithm.

    Note : This option is automatically activated when -unfold is used.
  • -unfold : Use the glutton strategy that consists of unfolding all symbolic traces and apply the symbolic equivalence decision procedure for each of them.
  • -verbose [<int>] : Display some statistics on the matrices generated at the end of the execution. When an integer <int> is given, the statistics are displayed every <int> matrices generated.

Uninstall

To uninstall APTE, first reach the extracted directory, then enter the following commands:

$ cd Source
$ make clean