tina logo

TIme petri
Net Analyzer

laas logo

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:
Three new tools: Also:

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:

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:

October 1, 2004: Version 2.7.0 is now available

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