/APTE

Algorithm for Proving Trace Equivalence

Primary LanguageOCamlGNU General Public License v3.0GPL-3.0

#APTE : Algorithm for Proving Trace Equivalence Version : 0.4beta-RED

This repository contains an ongoing work: implementing the optimized semantics defined in this paper in APTE.

There is one branch per optimized semantics:

  1. optim-compression: compressed semantics
  2. optim-c+r: reduced semantics

The branch bench_ref corresponds to the reference version (without optimization) used in benchmarks. The branch benchmark contains routines and results of benchmarks.

For more information about the original tool, visit the dedicated website.

  1. Installation
  2. Usage
  3. Uninstall

###1. Installation

To install APTE, first reach the extracted directory APTE-v0.4beta, then enter the following commands:

  1. cd Source
  2. make

Once the installation is done, an executable 'apte' is created in the directory main directory APTE-v0.4beta

###2. Usage

#####Synopsis :

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

#####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 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.

###3. Uninstall

To uninstall APTE, first reach the extracted directory APTE_v0.4beta, then enter the following commands:

  1. cd Source
  2. make clean