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

Automata networks

Pint takes as input automata networks. Automata networks are transition-centered models, close to 1-bounded Petri nets. They gather a finite number of finite-state machines, where their internal transitions can be conditioned by the state of other automata in the network.

Pint uses a simple plain text format to specify automata networks and their initial state. The text files have the extension .an.

Models expressed as Boolean and multi-valued networks can be automatically converted using the python interface. See pint.model.load() and Model input tutorial.

The structure of a .an file is the following. You can refer to the model repository for some examples.

Automata declaration

An automaton is defined by a name and a list of local states. If the name of the automaton contain special characters, it should be enclosed with ". The local states can either be integers, or strings (enclosed in ").

Examples:

a [0, 1]
b [0, 1, 2]
"Fyn-1" ["inactive", "active"]

Transitions

A transition specifies a local state change within one automaton, and can be conditionned by the conjunction of states of other automata.

Examples:

a 0 -> 1 when "Fyn-1"="active" and b=2
a 1 -> 0  (* no external condition *)
"Fyn-1" "inactive" -> "active" when a=0
"Fyn-1" 0 -> 1 when a=0 (* equivalent to previous declaration *)

Transitions can also be coupled, i.e., their application is done simultaneously:

{ b 0 -> 1 ; "Fyn-1" "active" -> "inactive" } when a = 1

The above synchronized transition can be perfomed only when a=1, b=0, and Fyn-1=active.

Initial state

By default, each automaton starts in the local state 0. The initial state of the automata network can be overrided with the following directive:

initial_state a=1,b=2

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.