
Changes from 2.7.4 to 2.8.0:
-----------------------------

tina-2.8.0 brings a number of new features and three new tools, all
brielfly described below.

PNML support:
=============

(check doc/formats/pnml.txt for futher information)

Tina 2.8.0 provides a preliminary  support for PNML. PNML support will
follow evolutions of the PNML  standard. The version of PNML currently
supported  are  BasicPNML   and  its  extension  (TPNPNML)  informally
described below. The TPNPNML extends Basic PNML as follows:

- In the "graphics" element of a node, one may add an offset specification
  interpreted as the position of the node id, relative to the node.
  e.g.	<offset x=... y=... />

- arcs may have an optional "type" element, one of normal, inhibitor, test;
  e.g.	<type value="test"/>

- Any transition may have a "delay" element, specifying a time interval in
  the style of MathML intervals, and optionally some position relative to
  the transition.

  e.g. (check doc/formats/pnml.txt for other examples) interval [4,9],
  positionned (-10,0) relative to the transition is specified as follows
  (note the "closure" attribute in the interval line):

  <delay>
   <interval xmlns="http://www.w3.org/1998/Math/MathML" closure="closed">
    <cn>4</cn>
    <cn>9</cn>
   </interval>
   <graphics>
    <offset x="-10" y="0" />
   </graphics>
  </delay>

The tools tina, struct, and the new plan tool, natively read BasicPNML
and its above extension. The nd editor may import from, and export to,
the above  format. The new ndrio  tool can convert  between .pnml .ndr
and .net formats. PNML support will follow evolutions of the PNML standard.

Generalized inhibor arcs and test (read) arcs:
==============================================

All tools now  support generalized inhibor arcs and  test (read) arcs.
The .aut and .ndr formats have been extended to support these features
(check   formats/net.txt   and   formats/ndr.txt   for  up   to   date
descriptions).  The .pnml TPN format also supports these.

To specify  a test (resp.   inhibitor) arc in  .net or .ndr,  one must
specify  its weight  and  uses  "?"  (resp.   "-?")   instead of  "*".
e.g. in  the following line,  p1*3 defines a  normal arc of  weight 3,
p2?4 a test arc of weight 4, and p3?-2 an inhibitor arc of weight 2.

   tr t1 p1*3 p2?4 p3?-2 -> p4*5
   tr t2 p2?4 p5 -> p6

In the  nd graphic editor, clicking  <3> allows to select  an arc type
together with its weight.

NOTE: The boundedness proprety  is undecidable for nets with inhibitor
arcs. However,  tina still  uses the usual  stopping test  by default,
that provides  here a sufficient  only condition for  boundedness.  If
desired, one  one may cancel it  (option -s 0) and  optionnaly use the
limit flags to enforce termination.

The net scripting language tpn:
===============================

In  addition to  format .net,  .ndr and  .pnmml, the  tina-2.8.0 tools
support a  simple scripting language  for building Time Petri  nets by
composition of  smaller nets.

The  .tpn  format   extends  both  .net  and  .ndr,   its  syntax  and
interpretation are defined in  file formats/tpn.txt. In short, the tpn
format allows one to build nets by composing net elements specified in
.net and/or  .ndr, composition operations  rely upon the .net  or .ndr
labels. When  nd, tina,  or another  tool,  reads a  .tpn files,  the file  is
interpreted on the fly. The composition operations are:

   - merge n : juxtaposition of nets (without fusion)
   - sync n  : composition by transitions (synchronous)
   - chain n : composition by places
   - ren ... : renaming and hiding of labels

The .tpn  format will  probably be extended  in future  versions. Some
example nets can be found in directory nets/tpn_examples.

New syntax for defining labels in .net:
=======================================

A mode convenient syntax is provided for declaring place or transition
labels in .net  files.  That notation will replace  in future releases
the obsolete "lb" declarations. e.g.

to assign label {TRANS 34} to transition t1, one had to write in 2.7.4:

		tr t1 [3,4[ p1 -> p2
                lb t1 {TRANS 34}
	
In 2.8.0, these two lines are equivalent to:

		tr t1 : {TRANS 34} [3,4[ p1 -> p2
	
Changes to the tina tool:
=========================

In addition to  the support of PNML, and  inhibitor/read arcs, two new
flags, -lt  and -ls  allows one to  output transition systems  (in any
output format) labelled by node labels rather than node names. This is
particularly useful in conjunction with CADP.

Also, performances have been improved for all constructions, specially
for nets with a large number of transitions.

Changes to the struct tool:
===========================

Now accepts net descriptions  in .pnml format (see above).  Structural
analysis  is performed  on nets  with  their inhibitor  and read  arcs
removed.

New tool, selt:
===============

This new tool is a model checker for a variant of State/Event-LTL with
integer  state/transition  properties.  The  tool operates  on  Kripke
transition systems in  .ktz format (as built by  tina with option -k),
and model checks the ktz read against Extended S/E-LTL formula.

Check the  selt man page (doc/man/mann/selt.n)  or in doc/txt/selt.txt
for a description.

For  translation of  LTL formula  to  Buchi automata,  selt relies  on
ltl2ba,   a    tool   developped    by   Didier   Oddoux    at   Liafa
(http://www.liafa.jussieu.fr/~oddoux).

New tool, ndrio:
================

This new tool converts between net descriptions in formats .net, .ndr, .tpn
and .pnml. When converting from a textual format to a graphic one, a
drawing tool may be specified (one of graphplace, dot, neato, circo).

Check the ndrio man page (doc/man/mann/ndriot.n) or file doc/txt/ndrio.txt
for a full description.

New tool, plan:
==============

This  tool  accepts  as  arguments  a net  and  a  firable  transition
sequence, and, according to other options, procudes a characterisation
of all firing  schedules having this sequence as  support, or a single
firing schedule. This tool is particularly helpful when model-checking
time Petri nets,  it allows to transform the  untimed counter examples
produced  by   selt  into  firable  firing   schedules  (times  firing
sequences) loadable into the nd simulator.

---------------------------------------------------------------------------

CHANGES from V2.7.2 to 2.7.4:
-----------------------------

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.


---------------------------------------------------------------------------

CHANGES from V2.7.0 to 2.7.2:
-----------------------------

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
8.4. To ease installation, the editor  is now deployed as a standalone
application  only. Problems  with management  of temporary  files have
been solved.



---------------------------------------------------------------------------

CHANGES FROM V2.6,. to V2.7.0 :
-------------------------------

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.   

* [tools] 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;


---------------------------------------------------------------------------

CHANGES FROM V2.0 to V2.6.6:
---------------------------

(dropped)


---------------------------------------------------------------------------

