What's new in TINA 3.8.0
May 5, 2024
- Arm64-darwin versions are slightly outdated, a refresh is forthcoming
New in TINA 3.7.5 (Apr 6, 2023)
- Added preliminary tina-3.7.5-arm64-darwin distribution;
New in TINA 3.4.4 (Jan 9, 2016)
- tts exceptions are now handled by sift and play rather than by tts libraries, with more helpful error messages.
New in TINA 3.4.2 (Oct 23, 2015)
- Refreshed the development environment for the tools.
New in TINA 3.4.0 (Oct 23, 2015)
- 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.
New in TINA 3.3.0 (Aug 27, 2014)
- Functionally identical to 3.2.2 but slightly faster thanks to some optimizations of memory management. Some minor fixes to the nd editor.
New in TINA 3.2.2 (Aug 27, 2014)
- 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).
New in TINA 3.2.0 (Aug 27, 2014)
- 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;
New in TINA 3.1.0 (Aug 27, 2014)
- 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.
New in TINA 3.0.6 (Aug 27, 2014)
- 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.
New in TINA 3.0.4 (Aug 27, 2014)
- 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);
New in TINA 3.0.2 (Aug 27, 2014)
- 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);