#APTE : Algorithm for Proving Trace Equivalence Version : 0.5beta
For more information about the original tool, visit the dedicated website.
To install APTE, first reach the extracted directory APTE-v0.4beta, then enter the following commands:
- cd Source
Once the installation is done, an executable 'apte' is created in the directory main directory APTE-v0.4beta
apte [-debug high|low|none] [-unfold] [-no_comm] [-no_erase] [-verbose [<int>]] [-display traces|size|step] [-log <int>] [-with_por [compr|red] [improper] [nouse]] file
APTE is programmed with three level of debugging.
- The High debugging option checks several invariants of the algorithms. While this mode provides more guarantee about the result, it makes the algorithm slower.
- The Low debugging option only checks basic invariants.
- The None debugging option does not check any invariant. (default) Chose this option for optimal running time.
-display traces : Display symbolic traces that are explored.
-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 .
-with_por [compr|red] [improper] [nouse]: Uses Partial Order Reductions techniques to significantly improve performance. It is possible to choose a specific POR technique (compressed or reduced semantics), improper and nouse are optional. Without extra argument, -with_por option will enable the best POR tehnique (i.e., reduced semantics with improper and nouse).
Note : This option automatically activates the option '-no_comm'.
WARNING : This option should only be used for action-determinate processes.
-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.
To uninstall APTE, first reach the extracted directory APTE_v0.4beta, then enter the following commands:
- cd Source
- make clean