Documentation

Installation

Pint is distributed as binaries for Ubuntu/Debian and Mac OS X. A docker image which contains all dependencies and the Jupyter notebook is also available.

Binaries

Docker

Docker is the easiest way to use Pint with the Jupyter notebook interface on any operating system. The image is named pauleve/pint.

Installation/upgrade using the command line:

docker pull pauleve/pint

The image can be mounted as follows, binding your current directory to the default image working directory:

docker run -it --rm -p 8888:8888 -v "$PWD":/notebook pauleve/pint

You can then go to http://localhost:8888 to access to the Jupyter notebook.

Please refer to Docker documentation for other usage. You can also use the python script docker-pint.py to ease docker invocation (see python docker-pint.py --help for the different options).

Python/notebook interface

The pypint module requires Python 3. It can be installed and upgraded with the pip command line as follows:

pip3 install -U pypint

If you are interested in the IPython notebook web interface, see Jupyter documentation for installation and usage. Essentially you need to install the jupyter python module (pip3 install jupyter) and then run jupyter-notebook.

Command line usage

Instead of using the python API, one can invoke directly the Pint command line tools:

  • Model input / output
    • pint-export – Automata network transformations and exportation
    • pint-import – Conversion to Pint .an format (requires the pypint python package)
  • Analysis tools
    • pint-reach – Static analysis of reachability
    • pint-stable – Stable states listing
    • pint-sg – State graph analysis
    • pint-lcg – Local Causality Graph computation
  • Interface with model-checkers
    • pint-its – Model-checking with ITS
    • pint-mole – Model-checking with mole
    • pint-nusmv – Model-checking with NuSMV
  • Miscellaneous commands
    • pint-confg – Pint installation informations
    • pint_install_deps – Script to install third-party dependencies
    • pint – Pint+OCaml interactive toplevel
    • pintc – Pint+OCaml native-code compiler

Note that all these command take as input a model in the Pint native format (.an). You may need to use python API to convert model from other formats.

All these commands come with a --help option which display the full usage of it. Another source of documentation is the debug mode of pint python module (enable_dbg()) which displays the executed command lines.

OCaml API

All functions implemented in Pint are available through an OCaml library that can be embedded in other OCaml programs. The library is compiled by executing make libpint in the source directory and is named pint.cmxa.

pintc file.ml can be used as a shortcut to compile OCaml code against the pint library.

pint is an OCaml interactive toplevel embedding the Pint modules.

See Pint OCaml module API.