January 06, 2016: Version 3.4.4 releasedtts 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 releasedRefreshed 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 releasedFunctionally 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 releasedVersion 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 releasedVersion 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 releasedMostly 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 releasedMostly 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 releasedA 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  and : 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 , 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 released2.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;
- 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);
- 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 released2.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 releasedFor 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 availableVersion 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. Also, installation and command line usages are easier since tina and struct are now standalone executables;
- [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;