TIme petri
Net Analyzer

MCC, a High-Level Petri nets unfolder

MCC is a tool developped by Silvano Dal Zilio aimed at unfolding high-Level Petri nets models given in PNML format into equivalent Place/Transition nets. Output formats include the net, tpn and pnml formats supported by the Tina tools.

Such nets are found, notably, among the models used at the Model Checking Contest, found in the current collection.

The mcc sources are available under license CeCILL-B at mcc github site.
mcc binaries are bundled with tina distributions. They are found at:

64 bit mcc for Linux
64 bit mcc for Windows
64 bit mcc for macOS
64 bit mcc for Solaris x86

Installation: Copy the mcc binary into a directory found in your PATH environment variable.

LTL to Buchi Automata converter options

(see also selt man page)


For building Buchi automata from LTL formula, selt relies on spin, but other options are supported, including ltl2ba, a tool developped by Denis Oddoux and Paul Gastin and ltl2tgba, part of the spot toolset, developped by Alexandre Duret-Lutz.

By default, selt will use the converter the name of which (one of ltl2nc, spin, ltl2ba, spot) is found in the environment variable LTL2BA, if set, or ltl2nc otherwise.

ltl2nc, spin

ltl2nc (ltl to never claim) is a stripped down version of spin-6.2.3 only implementing option -f.
This is the default converter. If needed, it can be enforced by -ltl2nc (e.g. if environment variable LTL2BA is defined and its contents is not ltl2nc).
ltl2nc binaries are bundled with tina distributions. These are:

32 bit ltl2nc for Linux (Ubuntu 14, glibc 2.19)
32 bit ltl2nc for Windows (mingw-w64)
32 bit ltl2nc for macOS (10.12, Sierra)
32 bit ltl2nc for Solaris x86 (Solaris 11.4)

64 bit ltl2nc for Linux (Ubuntu 14, glibc 2.19)
64 bit ltl2nc for Windows (mingw-w64)
64 bit ltl2nc for macOS (10.12, Sierra)
64 bit ltl2nc for Solaris x86 (Solaris 11.4)

The stripped spin-6.2.3 sources used to create ltl2nc can be found in archive ltl2nc.tgz.

According to the spin 6.2.3 license, no license is required for educational or research purposes, but one is needed for commercial usage.

If spin is installed at your site (whatever version), it can be used for ltl formula conversion instead of ltl2nc by passing flag -spin to selt or setting variable LTL2BA to spin. In any case, the directory in which the spin binary resides must be found in your Path variable.

ltl2ba

Convert ltl formula to buchi automata using Oddoux/Gastin ltl2ba. Typically yields smaller automata than the above, fits most purposes and easy to compile. ltl2ba must be installed at your site, from the GPL licensed sources available at (http://www.lsv.fr/~gastin/ltl2ba). Pre-compiled binaries of ltl2ba v1.0 (unchanged) for some targets are made available below.
ltl2ba is enabled by selt flag -ltl2ba or by the environment variable LTL2BA containing the word ltl2ba.

ltl2ba v1.0 binaries:

32 bit ltl2ba for Linux (glibc 2.11)
32 bit ltl2ba for Windows (mingw-w64)
32 bit ltl2ba for Intel macOS (10.6, Snow Leopard)
32 bit ltl2ba for Solaris x86 (Solaris 11)
32 bit ltl2ba for PowerPC macOS
32 bit ltl2ba for Sparc Solaris (Solaris 10)

64 bit ltl2ba for Linux (glibc 2.11)
64 bit ltl2ba for Windows (mingw-w64)
64 bit ltl2ba for macOS (10.12, Sierra)
64 bit ltl2ba for Solaris x86 (Solaris 11)

Installation: The simplest is to copy the ltl2ba binary into the bin directory of your tina distribution. Alternatively, copy the ltl2ba binary into a directory found in your PATH environment variable.

ltl2tgba, spot

Convert ltl formula to buchi automata using ltl2tgba from the SPOT model checking library. ltl2tgba must be installed at your site, from the GPL licensed sources available at (http://spot.lrde.epita.fr). This is certainly the fastest converter available, and that yielding the smallest automata, but compilation may be challenging on some targets.
ltl2tgba is enabled by selt flag -spot or by the environment variable LTL2BA containing spot or ltl2tgba

For compiling and installing spot from the sources, check https://spot.lrde.epita.fr/install.html. Some pre-compiled binaries of ltl2tgba (not a full binary distribution of spot) may be available below.

ltl2tgba version 2.9.3 binaries:

64 bit ltl2tgba for macOS (10.12, Sierra)

Installation: The simplest is to copy the ltl2tgba binary into the bin directory of your tina distribution. Alternatively, copy the ltl2tgba binary into a directory found in your PATH environment variable.

Linear algebra tools

4ti2

For improved performances of the struct and reduce tools, and of some variable order computations by tedd, one may wish to install the 4ti2 tool suite from the GPL licensed sources at https://github.com/4ti2/4ti2.
It should compile without issues on unixes, please follow the instructions in the 4ti2 source distribution. There may be some minor issues for compiling it for Windows, depending on the compiler used. For convenience here are pre-compiled binaries of the 4ti2 1.6.7 suite for the most common targets:

64 bit 4ti2 for macOS (10.12, Sierra)
64 bit 4ti2 for Linux (Ubuntu 14, glibc 2.19)
64 bit 4ti2 for Windows (Windows 10)

Installation: These archives pack a folder named 4ti2 containing a binary distribution of 4ti2 version 1.6.7, including its dependencies for windows. For using it with tina, unpack the distribution in (say) folder location, then add location/4ti2/bin (location\4ti2\bin on windows) to your PATH environment variable, or, alternatively, copy the contents of 4ti2/bin into the bin directory of your tina distribution.