Construction of Verified Concurrent Systems
Logo Inria Logo LIG Logo Grenoble INP Logo CNRS Logo UJF

PIC2LNT (Translator from Applied Pi-Calculus to LNT)

  • Download PIC2LNT 3.0 (May 2013)

    PIC2LNT 3.0 takes into account the feedback provided by Saarland University (Germany), where PIC2LNT 2.0 was intensively tested in concurrency courses. In addition to fixing several bugs, PIC2LNT 3.0 brings the following improvements w.r.t. version 2.0:
    • Explicit manipulation of the Chan type representing channel names, and its usage in conjunction with user-defined LNT types (e.g., lists of channels, arrays of channels, etc.).
    • Introduction of the "-nat_bits" option for setting the range of the Nat type, and hence the set of private channel names that can potentially be generated.
    • Introduction of a new example of PIC specification, which illustrates the manipulation of channel lists.
    • Simplification of data variable declarations to maintain the symmetry with the standard pi-calculus and to avoid ambiguous interpretations of mixed declarations involving both data variables and channel names.
    • Simplification of the syntax of single channel emissions to be closer to the mathematical notation used in the pi-calculus literature.
    • Improvement of the manual page with new material.

  • Download PIC2LNT 2.0 (October 2012)

    • PIC2LNT 2.0 [MS13] handles the PIC language, an extension of the polyadic pi-calculus with the data types and functions of LNT.
    • PIC2LNT 1.0 [MS10] was an experimental version, which handled the standard polyadic pi-calculus (without data manipulation).
Last modified: 2015/09/08 16:55:18.