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

Conda package

Pint can be installed on GNU/Linux using Conda with the colomoto channel:

conda install -c colomoto pint

Docker

Docker is the easiest way to use Pint with the Jupyter notebook interface on GNU/Linux, macOS, and Microsoft Windows. Pint is integrated in the CoLoMoTo Interactive Notebook available as Docker image colomoto/colomoto-docker.

A Python helper script can be installed and upgraded by executing the following command (you may have to use pip3 instead of pip depending on your configuration):

pip install -U colomoto-docker

The CoLoMoTo notebook can then be started by executing in a terminal (if using Docker Toolbox, in a Docker Terminal):

colomoto-docker

The container can be stopped by pressing Ctrl+C keys.

Warning: by default, the files within the Docker container are isolated from the running host computer, therefore files are deleted after stopping the container. To have access to the files of your current directory you should use the --bind option:

colomoto-docker --bind .

See

colomoto-docker --help

for other 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.