The TINA toolbox Home Page - TIme petri Net Analyzer

July 08, 2024: MCC results are out

Tools tedd and SMPT participated to the 2024 edition of the Model Checking Contest, held this year as part of Petri Nets 2024. For the 6th time in a row (even 8th if considering raw values) tedd topped the StateSpace category; SMPT further consolidated its bronze medal in the Reachability category, very near to silver, and recovered full confidence. Full details at MCC 2024. Thanks to the organizers !

May 05, 2024: Version 3.8.0 released

Besides bug fixes and numerous optimizations, Version 3.8.0 of the TINA toolbox enriches several tools and adds a new one: scan.

New exploration modes, referred to as "maxsteps" modes, have been added to tools tina, sift, walk and nd. A summary of maxsteps modes additions can be found in page maxsteps.

The ktz transfer format for Kripke Transition Systems has been enriched with so-called profiles, supported by tools sift and ktzio. In short, a profile specifies the informations to be recorded in the ktz file. A summary of ktz profiles additions can be found in page profiles.

Tool walk now can handle sets of formulas in addition to a single one; the input formula passed by -f may be a set, represented by individual formulas separated by a semicolon. Tool walk evaluates all open formulas at each state and terminates when no more open formula is left or upon some limit violation;
Also, the -loop option now unconditionally restarts the simulation when the exploration path ends; option -repeat behaves like -loop except that it does not restart on limit violations (on path length or time elapsed).

tool muse gains options -m and -script, and its mu-expression language is enriched with "kinded" logical constants, rarely needed to disambiguage expressions. Tool selt gains a similar -script option. Tools selt and muse now check that the input ktz profile is adequate for LTL and mu-calculus model-checking. Please check their manual pages for details.

A new tool is introduced: scan. In short tool scan is a version of tool muse specialized for the verification of reachability properties. Conversely to muse, tool scan is not interactive, however. Please check the scan manual page for details.

tool reduce benefits of more reduction rules, the latest addition detects acyclic nets and build their state equation (the state spaces of acyclic nets are exactly described by their so-called state equation).

Finally, as some use cases were found that need then, "large" integer versions of the tools, providing 64 bit wide markings and time interval bounds instead of the default 32 bit wide are distributed along the regular versions.

May 20, 2023:

Tools tedd and SMPT participated to the 2023 edition of the Model Checking Contest, held this year as part of the Toolympics. Tedd kept its title in the StateSpace category, and SMPT consolidated its standing in the Reachability category, full details at MCC 2023.

March 29, 2023: Version 3.7.5 released

Mostly a maintenance release. Added a preliminary distribution for Apple Silicon.

August 8, 2022:

By the way, tina-3.7.0 and its friend SMPT shined at the last Model Checking Contest. Among the strategies it implements, SMPT makes use of tina tools reduce and walk.

(See MCC 2022 for details.)

January 20, 2022: Version 3.7.0 released

In addition to a number of minor improvements, release 3.7.0 introduces preliminary versions of three new tools: reduce, tedd, and walk.

Tool reduce implements the reduction rules introduced in [20], [21], used successfully in our MCC participations from 2018. Given a reduction rules specification, it produces a reduced net together with reduction traces (equations linking the markings before and after reduction).

Tool tedd plays a role similar to the available sift tool but relies on decision diagram based methods rather than explicit methods. It does not allow to check reachability properties yet, except for absence of deadlocks or dead transitions, but this is a scheduled improvement. An enrichment of tool tedd with reductions and counting methods for integer points in polytopes won the gold medal at the last three Model Checking contests in the State Space category. Tool tedd will be progressively enriched in forthcoming releases of the toolbox to include all capabilities of the MCC version.

Given a reachability property, tool walk attempts to find a marking falsifying it, by a possibly constrained random walk of its state space.

July 17, 2021: Version 3.7.0 forthcoming

In the meantime, and for the third time in a row (see MCC 2021 for details):

June 09, 2020: Version 3.6.0 released

Mostly a maintenance release. The most visible changes concern the nd editor.

The look and feel of nd has been improved on some platforms, following a refresh of some internal components;

nd now provides built-in export of nets and automata to tikz figures, ready to insert in latex documents. Another export is provided to the Graphviz dot format.

In addition to tina for state space analysis and struct for structural analysis, a third tool can be called from the Tools menu, sift, for on the fly reachability analysis.

(Next) The promised new tool, tedd, could not be introduced in the toolbox yet, but its development continues. For the second year in a row, it won a gold award at the Model Checking Contest, in the "StateSpace" category (see MCC 2020 for details).

June 03, 2019: Version 3.5.0 released

Version 3.5.0 is an overhaul of 3.4.4 bringing a number of improvements to the existing tools and a few new features, including:

The sift tool benefits of a new construction for reachability analysis of Time Petri nets. That construction, enabled by flag -hull (selecting either construction -H of -G, see details on the man page), builds an overapproximation of the state classes of the TPN computing only one class per marking. It can be much faster than standard reachability analysis (using -incl , selecting either -M or E). Tool sift also gets a new exploration order flag: -rf. With flag -rf, markings or state classes are explored in random order, as opposed to depth-first order (-df) and breadth-first order (-bf, default). This may help reachability analysis in some cases;

The nd editor now provides built-in export of nets into Romeo and lola formats, and of nets and automata in graphical form into latex/tikz and dot descriptions (check File -> export).

The ndrio net conversion tool has a new flag, -rev, that reverses the edges of a net;

The ktzio transition system conversion tool gets a new textual output format, ktj. Format ktj is a json representation of the kripke transition systems captured in ktz file. Beware that, compared to ktz binary files, ktj files may be very large.

Numerous fixes and internal improvements.

(Preview) The next major release, tentatively scheduled for the end of 2019, will introduce new important features for tool sift and a new tool, tedd. tedd is a symbolic analysis tool developped over the last few years relying both on decision diagrams and on a new symbolic representation of state spaces by equation systems explained in [20]. Tool sift will also benefit of equational representations. The development version of tedd won a gold award at the 2019 edition of the Model Checking Contest in the "StateSpace" category (see MCC 2019 for details).

January 06, 2016: Version 3.4.4 released

tts exceptions are now handled by sift and play rather than by tts libraries, with more helpful error messages.

October 22, 2015: Version 3.4.2 released

Refreshed the development environment for the tools.

June 29, 2015: Version 3.4.0 released

Version 3.4.0 brings many improvements to the tools. Among these:

- The pnml parser is now much faster;

- When requested to compute semiflows on places, the struct tool now prints the ponderated initial marking for each place invariant, following each semiflow. An additional flag has been added to struct, -safe, that checks using semiflows a sufficient condition for safeness of the net;

- The experimental symbolic mode of sift (sift -Z, relying on set decision diagrams) has been moved to a forthcoming tool dedicated to decision diagram based methods (tedd).

- The nd editor provides a support for annotations in graphic descriptions, for both nets and automata, and in textual net descriptions, see files nets/annotations_examples/* in the distribution for some examples.

August 25, 2014: Version 3.3.0 released

Functionally identical to 3.2.2 but slightly faster thanks to some optimizations of memory management. Some minor fixes to the nd editor.

June 16, 2014: Version 3.2.2 released

Version 3.2.2 is a maintenance release. The graphic editor nd benefits of some improvements, notably: graphic descriptions can now be printed in pdf format; graphic transformations have been added to menu Edit (h/v flips, rotations, zooming).

October 15, 2013: Version 3.2.0 released

Version 3.2.0 is a major release.

The toolbox underwent a major refactoring work following the recent introduction of several tools. The new source organization favors modularity and ease of maintenance; performances should be similar or slightly better than those of version 3.1.0;

Other changes include:

Some algorithmic improvements of the timed modes of tool sift. Also added ktz output for modes -M/-E (state classes under time domains inclusion). In such modes, the ktz file only captures states (but no paths), each with a loop for each transition firable from the state. This allows one to check reachability and quasi-liveness properties on such constructions using the muse model checker;

Discrete time constructions in tina and sift (modes -D and -F) now allow strict interval bounds;

Updated pnml parser/printer; the tools reading pnml should now be able to read all single-page P/T pnml files;

All uncovered bugs have been fixed;

January 7, 2013: Version 3.1.0 released

Mostly a maintenance release.

Improved computation of fixpoints in muse model checker. Fixed mode -A of tina (could disagree with mode -U). Added conversion from ktz to concurrency workbench format to ktzio. Minor fixes in nd.

November 2, 2012: Version 3.0.6 released

3.0.6 fixes the generation of ktz files by the sift tool; these files are now readable on all targets, independently of the version of the zlib provided. If needed, the ktz files generated by older sift versions can be fixed by: gzcat old.ktz | gzip -c > new.ktz (don't worry about the crc error message).

Also fixes output mode "bool" of muse; now returns the truth value of the formula at the initial state, as it should be.

October 9, 2012: Version 3.0.4 released

Mostly a maintenance release.

Adds an "assert" command to the model checkers. Command assert allows one to customize the message printed when an expression is proved or disproved (please check the selt and muse man pages for details);

July 4, 2012: Version 3.0.2 released

A maintenance release.

Fixes a bug in ktz generation by sift on Windows targets (ktz file could be unreadable in some cases);

Added to selt the capability of using ltl2tgba from the SPOT library instead of the default ltl2ba (please check the selt man page for details);

February 29, 2012: Version 3.0.0 beta released

In addition to bug fixes and many improvements of 2.10.0 tools, Tina version 3.0.0 introduces five new tools:

frac -- support for high-level descriptions in Fiacre: As of version 2.9.0, tina supports an extension of Time Petri Nets with data actions and preconditions specified in C (see the description of the tts format in manual pages). A higher level notation is now available, in a language called Fiacre. Fiacre descriptions can be compiled to tts descriptions accepted by tina by a dedicated compiler, Frac. The Fiacre language and the Frac compiler are described and made available in a companion site www.laas.fr/fiacre.

sift: it is a specialization of the tina tool, it offers less options than tina but implements them more efficiently; sift is faster than tina and makes use of considerably less space. sift also allows to check reachability properties on the fly.

pathto: a utility program; given a kripke transition system in a ktz file and a target state, pathto computes and prints a path to that state. pathto is mostly useful for for building transition sequences leading to counter-example states computed by sift.

play: allows to simulate net descriptions in all formats accepted by tina. Its capabilities are similar to those provided by the nd stepper except that play may also simulate .tts descriptions.

muse: (in progress) a modal mu-calculus model checker operating on kripke transition systems represented in .ktz format. Check the Fiacre pages and the manual pages in directories doc/* of the distributions for usage details.

March 8, 2011: Version 2.10.0 released

Most tools now handle Stopwatch Time Petri Nets formerly supported only by the experimental swtina distributions. Support of stopwatches is still partial though, check file CHANGES in the distribution for the constructions supported and limitations;

The editor (nd) has been improved. A toolbar makes it easier to use on laptops. The former graphic bindings, slightly cleaned up, are still supported as shortcuts when selection mode is set in toolbar. The bindings in use are recalled in the nd window on startup;

Concerning tools, all known bugs have been fixed, many optimizations applied, and a few simplifications of control flags implemented.

tina 2.10.0 is available for three more 64 bit targets (MacOS, Windows, Solaris) in addition to Linux.

November 24, 2009: Version 2.9.8 released

A maintenance release, except for MacOS:

Fixes all uncovered issues with 2.9.6, including font issues on Fedora 11;

A new limit flag (-en k) has been added to the tina tool: "tina -en k" stops as soon as the number of enabled transitions in the net drops below k. Hence "tina -en 1" checks absence of deadlocks on the fly;

The MacOS version of the nd editor underwent a major revision, improving its "look and feel" and fixing all known issues on that target.

June 10, 2009: Version 2.9.6 released

2.9.6 is a maintenance release. All known issues with 2.9.4 have been fixed; some algorithmics improvements have been introduced.

November 17, 2008: Version 2.9.4 released

Version 2.9.4 is mostly a maintenance release. The most visible change is the addition of a 5 lines digest printed by tina on standard output (or in a file) upon completion of the analysis. The digest summarizes its results (whatever the actual output format), it notably prints the status of the boundedness, liveness and reversibility properties. In nd, the digest is shown in the tina result window, for all output formats.

Read arcs and inhibitor arc are now supported by all constructions (where meaningfull). Liveness analysis is faster for large graphs, and takes less memory. Many small improvements have been implemented, with a notable speedup for modes -P, -M, -E. Minor changes to tina commandline: added flags -stats, -d, removed flag -x, added digestfile argument.

May 2, 2008: Version 2.9.2 released

Version 2.9.2 is functionally equivalent to 2.9.0, but brings an improved memory management. The new memory management significantly improves the speed of all tina constructions, specially those not handling time constraints.

February 29, 2008: Version 2.9.0 released

Version 2.9.0 is a major release. Among many improvements it introduces static priorities, as explained in [15] and [16]: A transition is firable at some instant if no transition with higher priority is firable at the same instant. In absence of priorities, and besides minor ergonomic differences, 2.9.0 behaves exactly like 2.8.4 and is fully upward-compatible.

Priorities may be specified graphically by drawing arcs between transitions (the source has higher priority than the destination), or textually with "pr" declarations (check doc/formats/net.txt for details). The priority relation is the transitive closure of the specified relation, it must be irreflexive. The priority relation is checked when saving/loading/simulating/analyzing nets or explicitly by tools->check net. All tools support priorities. The tina constructions taking advantage of priorities are the reachability graph (mode -R) in absence of time constraints, and the strong state class graph (or zone graph, mode -S) if time constraints are present. The other constructions forget priorities (a proper warning is printed). The construction selected by default is assured to handle all features present in the net.

Besides priorities, the nd editor and other tools have been improved in an number of ways favoring robustness, ease of use and performances. All tools have been intensively tested over the last months.

January 9, 2008: Version 2.8.6 beta released

Besides the new targets, 2.8.6 is mostly a maintenance release. The visible changes from 2.8.4 include:

New targets: i86pc (for PCs under Solaris x86), intel-pc (a native version for macintels), and x86_64-linux (for 64 bit linuxes);

nd: The control menubar has been moved to a more standard place, making edition easier in fullscreen mode or on targets not supporting "focus-follows-mouse" (MacOS). The old behavior can be selected on the setup panel, if desired;

nd: The naming discipline for pasted nodes has been changed: suffixed names are replaced by generated names of form tn or pn. Again, the old behavior can be selected on the setup panel, if desired;

November 17, 2006: Version 2.8.4 released

Besides bug fixes and many small improvements, the changes from 2.8.0 to 2.8.4 essentially concern the tina tool:

tina now provides Popova's "essential states" method (tina -D/-F/-F1);

A variant of the coverability tree construction (-Cm n) allows one to set a marking threshold for unbounded places (see the man pages for details);

Constructions -S, -A and -U have been improved for nets with unbounded firing intervals: instead of the "clock domain relaxation" of [5], these constructions now use the simpler "normalization" operation proposed by Hadjidj/Boucheneb;

The ktz binary format for transition systems has been improved;

March 31, 2006: Version 2.8.0 released

2.8.0 is a major overhaul of the toolbox.

The internals have been restructured to accomodate new forthcoming features, and three new tools are available. Externally, the main visible changes are:
More and enriched input formats:

PNML support: all tools accept nets described in PNML (BasicPNML and a timed extension). The nd editor may import from, and export to, PNML, the tools (tina, struct, plan, ndrio) accept PNML files;
TPN scripts: a new net description format (.tpn) extending both .net and .ndr allows one to build complex nets by composition, using place and/or transition labels;
All net description formats now support generalized inhibitor and read (test) arcs;

Three new tools:

selt: a State/Event LTL model checker operating on kripke transition systems represented in .ktz format;
plan (preliminary): a path analysis tool. Plan computes all, or a single, firing schedules over some transition sequence; more capabilities to come;
ndrio: converts nets between several formats (.net, .ndr, .tpn and .pnml, at the time);

Also:

New tina flags -ls and -lt allow to print transition systems labelled using place or transition labels rather than names;
The MacOSX distribution has been improved and is now self-contained;
Performances and robustness have been improved throughout;
Check the man pages in doc/man, and the documents in doc/txt and doc/formats for all new features.

May 2, 2005: Version 2.7.4 released

2.7.4 mainly improves the nd editor and stepper simulator. Also, installation on Windows is simpler. The changes are:

[nd] Now provides selection, with standard bindings and Cut/Copy/Paste/Move facilities for node groups.
[nd] Several nets can be merged into the graphic buffer (File->include->...).
[nd] Nodes in the graphic buffer can be fused (superpose them, then use Button 3);
[nd] Generic facilities allows one to invoke his/her own applications from the tools menu, provided they operate on files in the formats recognized by nd, check (Tools->how to ...) for details.
Available plugins for nd using these features will be advertized in the new Friends page, if desired.
[nd] The stepper simulator has been much improved, in look, behavior, and functions for replaying scenarios
[tools] On windows, the cygwin library is no more needed, just download and run.
[tools]: A new flag (-wp) controls generation of temporal divergence information in lts outputs (check the man pages for details). The ktz format captures that information.

December 20, 2004: Version 2.7.2 released

For Linux/Windows/Solaris, 2.7.2 is essentially a bug fixes and clean up release. The real novelty is availability of a version for MacOS X. The changes are:

[nd+tools] Now available for MacIntoshes under MacOS X. The MacOS X release comes with two versions of the editor, one runs under X11, and the other runs under the native Aqua graphic system. Check file INSTALL in the distribution for details.
[nd] Now runs with the latest, and much faster, Tcl/Tk version. To ease installation, the editor is now deployed as a standalone application only. Problems with management of temporary files have been solved.

October 1, 2004: Version 2.7.0 is now available

Version 2.7.0 brings major improvements over previous releases. The major changes are:

[nd] Includes a stepper simulator. One may animate a Petri net or Time Petri net without leaving the editor;
[tina and struct] Overall performances improvements due to a change of compiler.
[tina] Improved algorithmics for constructions -S (SSCG) and -A (ASCG);
[tina] New modes -M (preserves markings), -E (preserves states), and -Vq (checks quasi-liveness);
[struct] Now offers a choice of algorithms for computing flows or semiflows;

TIme petriNet Analyzer