no bundeling of tina anymore, improved cmdl interfacing

build.gradle

@@ -80,7 +80,7 @@ dependencies {
 
     jastadd2 "org.jastadd:jastadd:2.3.4"
     relast group: 'org.jastadd', name: 'relast', version: "${relast_version}"
-    ecore files("libs/ecore2relast-0.1.jar")
+    ecore files("src/libs/ecore2relast-0.1.jar")
 
     testImplementation('org.junit.jupiter:junit-jupiter:5.8.2')
 
@@ -110,23 +110,31 @@ jar {
 
 task fatJar(type: Jar) {
     group = "build"
-
     archiveAppendix = "fatjar"
+
+    // Include the compiled output and runtime dependencies
     from sourceSets.main.output
     from sourceSets.main.allSource
     from {
         configurations.runtimeClasspath.collect { it.isDirectory() ? it : zipTree(it) }
     }
 
-    manifest.attributes "Main-Class": "de.tudresden.inf.st.pnml.flatter.Main"
+    // Ensure the correct Main-Class is specified
+    manifest {
+        attributes(
+                "Main-Class": "de.tudresden.inf.st.pnml.flatter.Main"
+        )
+    }
 
+    // Exclude unnecessary files
     exclude 'META-INF/*.RSA', 'META-INF/*.SF', 'META-INF/*.DSA'
-
     duplicatesStrategy = DuplicatesStrategy.EXCLUDE
 
     archiveBaseName = 'pnml-relast-flattener'
 }
 
+
+
 // Generated files
 def ecoreFile = './src/main/resources/placeTransition.ecore'
 def ecoreRelastAspect = './src/gen/jastadd/pnml/placeTransition.ecore.jadd'

libs/tina-3.7.0/CHANGES

-Changes from 3.0.0 to current:
------------------------------
-
-Now summarized on http://www.laas.fr/tina/news.php
-
-
-Changes from 2.10.0 to 3.0.0:
------------------------------
-
-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 (http://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.
-
-
-Changes from 2.9.0 to 2.10.0:
------------------------------
-
-The standard tina distribution  now supports the "Stopwatch Time Petri
-nets", formerly  in a specific distribution, introduced in paper:
-
-  B. Berthomieu, D. Lime, O. H. Roux, F. Vernadat,
-  Reachability Problems and Abstract State Spaces for Time Petri Nets
-  with Stopwatches,
-  Journal of Discrete Event Dynamic Systems 17:133-158, 2007.
-
-
-Changes following the support of stopwatches:
-
-- The graphic  editor and  all net formats  support two more  types of
-arc: stopwatch arcs and stopwatch-inhibitor arcs.  These arcs serve to
-stop/resume the clock of their target transition.
-
-- In the  textual .net format, stopwatch  and stopwatch-inhibitor arcs
-are  specified  like  read  and  inhibitor  arcs,  respectively,  just
-replacing symbol "?" by "!", as in e.g.:
-
-            tr t0 [4,5] p1 p2!1 -> p3*3
-            tr t1 [3,w[ p6 p5!-3 -> p8 
-
-The tool tina has two extra flags:
-
-- flag  -grid  n/d specifies  a  grid  size  for overapproximation  of
-temporal domains (default none) in presence of stopwatches.
-
-- flag  -pk   (1|2|3)  specifies  the  format   of  inequality  system
-coefficients   and  constants   in  state   classes  in   presence  of
-stopwatches: 1 means 32 bit (fast but high risks of overflow), 2 means
-64  bits (default),  3  means arbitrary  precision  integers (may  not
-overflow, but computationally expensive).
-
-Support  of  stopwatches   currently  suffers  some  restrictions.  In
-particular:
-
-- Some constructions are not implemented  for SwTPN's yet; tina modes
-  -D/-F/-U/-A are not supported;
-
-- Unbounded static intervals are not supported for SwTPNs in mode -S;
-
-- The  plan tool does not support stopwatch arcs yet,  so the  counter
-  examples computed by the model checker cannot be timed (nor reloaded
-  into the nd stepper if using selt from nd);
-
-Finally, it  should be stressed  than computation of state  classes of
-SwTPN's is not  guaranteed to terminate in general,  unless the net is
-intrinsically bounded  AND some grid  size is specified by  flag -grid
-(check the above papers for details). Also, computing state classes in
-presence of stopwatches can be very slow and space consuming.
-
-
-The other changes include:
-
-- nd:  The nd  editor  now  provides a  toolbar.   The former  graphic
-bindings are still supported (when toolbar is in selection mode).  The
-graphic bindings  have been cleaned  up, specially on MacOS;  they are
-recalled  in the  nd  window on  startup.   Check nd->preferences  for
-options;
-
-- tools:   besides  bug   fixes  and   many  optimizations,   flag  -s
-(boundedness test) of tina now has  two options only: -s 0 removes any
-boundedness  check, -s 1  (default) checks  a necessary  condition for
-unboundedness of the underlying petri net (omitting time constraints).
--s 1  is cheap but with  a small risk  of non termination; for  a true
-boundedness  check on  untimed  nets,  one should  use  the costly  -C
-option (on untimed nets).
-
-- the pnml parser now handles pages (one page actually);
-
-
-Changes from 2.8.4 to 2.9.0:
------------------------------
-
-Besides  many   improvements,  it  introduces   static  priorities:  A
-transition is  firable at  some instant if  no transition  with higher
-priority is  firable at the  same instant.  In absence  of priorities,
-2.9.0  behaves  exactly  like  2.8.4  (in  spite  of  minor  ergonomic
-differences) and is fully upward-compatible.
-
-- Priorities  may be  specified graphically,  by drawing  arcs between
-transitions, from  that with higher  priority, 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.  All tools  support priorities, but priorities are not
-meaningfull in  all state space abstractions  (notably in coverability
-graphs (-C)  and state classes (-W)).  The  adequate constructions for
-handling priorities are the reachability graph (mode -R) in absence of
-time constraints and the strong state class graph (or zone graph, mode
--S) with time constraints.  More constructions will support priorities
-in  the  future  (including  covering  state graphs  (mode  -V)).   By
-default, the state space  abstraction tool selects a construction that
-handles all features present in the net.
-
-- The nd  editor and other  tools have been  improved in an  number of
-ways  favoring robustness, ease  of use  and performances.
-
-
-Changes from 2.8.0 to 2.8.4:
------------------------------
-
-Besides bug fixes and many  small improvements, the changes from 2.8.0
-to 2.8.4 essentially concern the tina tool:
-
-- New tina  modes (tina -D/-F/-F1) provides three  variants of Louchka
-Popova's "essential states" construction;
-
-- Constructions  -S,  -A and  -U  have  been  improved for  nets  with
-unbounded firing  intervals: instead of the  "clock domain relaxation"
-defined in our TACAS'03 paper, these constructions now use the simpler
-"normalization" operation proposed by Hadjidj/Boucheneb;
-
-- 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);
-
-Though this is  not documented yet, Tina 2.8.4  also supports (for all
-targets) a  form of "predicate/action" Time Petri  net: predicates and
-actions over  some data  may be associated  with the transitions  of a
-net, written in C. Some tutorial examples are available.
-
-Finally, an experimental version  of Tina is available, called SwTina.
-SwTina supports  an extension of  Time Petri nets with  suspension and
-resumption of transitions, called "Stopwatch Time Petri nets".  Please
-check  the  page   http://www.laas.fr/tina/next.php  for  details  and
-pointers.
-
-
-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 inhibitor arcs and test (read) arcs:
-================================================
-
-All tools now support generalized inhibitor 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> on an arc allows to select its
-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 or  .tpn formats as  well (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 extended
-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.
-To give an idea, the following  are examples of legal selt commands:
-
-    [] (3*p1 + 4*p2 - p3 >= 7);	         (checks a marking invariant)
-    infix x follows y = [] (y => <> x);  (declares follows)
-    t5 follows (p5 >= 4);		 (a mixed state/trans formula)
-
-Check the  selt man page (doc/man/mann/selt.n)  or in doc/txt/selt.txt
-for a full 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, produces a characterisation
-of all firing  schedules having this sequence as  support, or a single
-such  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 for replay.
-
----------------------------------------------------------------------------
-
-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)
-
-
----------------------------------------------------------------------------
-

libs/tina-3.7.0/INSTALL

-Installation instructions for Linux or Solaris.
-
-
-1. prerequisites:
------------------
-
-None.
-
-
-2. installing the toolbox:
---------------------------
-
-Download and  unpack the tina  distribution. This creates  a hierarchy
-rooted  at tina-3.X.Y.   The binaries  are in  subdirectory  bin.  The
-editor  is "nd".
-
-The man pages are in  doc/man/mann, a quick installation in tcsh is e.g.
-	setenv MANPATH <tinadir>/doc/man:$MANPATH
-Directory doc/txt holds text only copies of these.
-
-To  use  the tools  standalone,  you  may wish  to  add  the tina  bin
-directory to the PATH environment variable, and the tina lib directory
-(if any) to  variable LD_LIBRARY_PATH. This is not  required for using
-the tools from  the editor, however.  Alternatively, nd  and the tools
-can  be  moved or  copied  at  some  standard place  (e.g.   /usr/bin)
-provided all the contents of the tina bin directory is moved or copied
-there. Similarly, the libraries could be moved to /usr/lib and the man
-pages to /usr/man/mann.
-
-The nd  graphic editor assumes  a 3-button mouse is  present. Bindings
-for  emulating a  3-button  mouse with  a  2-button mouse  or pad  are
-built-in: the  Middle button is simulated  by Shift-RightButton. Click
-Help->nd help for information on the graphic bindings.
-
-
-3. drawing filters:
--------------------
-
-Nd can draw nets or  automata from textual descriptions, provided some
-placement filters  are installed.  Nd has builtin  interfaces for four
-filters :  graphplace, dot, neato  and circo. Graphplace and  dot play
-somewhat the  same role  and are suitable  for drawing dags;  neato is
-best suited for drawing graphs  with cycles; circo attempts a circular
-layout.
-
-Graphplace is bundled  with nd. It is a program  by Jos van Eijndhoven
-at Eindhoven University of Technology, available in source form at:
-	ftp://ftp.es.ele.tue.nl/pub/users/jos/graphplace.tar.gz
-
-Filters  dot, neato  and  circo are  part  of the  AT&T graph  drawing
-package  Graphviz.  Graphviz  is  available  precompiled  for  various
-platforms at:
-	http://www.graphviz.org
-
-For convenience,  stripped down versions  of dot, neato and  circo are
-bundled with the tina distributions.  If Graphviz is already installed
-on your system,  then you may wish to delete the  versions in the tina
-bin directory, and make the installed filters reachable from your PATH
-instead.
-
-
-4. bcg support:
----------------
-
-Format  bcg  is one  of  the formats  supported  by  the CADP  toolbox
-(available at http://www.inrialpes.fr/vasy/cadp).  Bcg support is only
-available on linux and windows versions (please contact us if you need
-bcg support for other targets).  It first requires to properly install
-the CADP  toolset on your machine,  then you must  compile and install
-libbcg.so  (on linux),  or  libbcg.dll (on  windows)  as explained  in
-extras/bcgsupport/README.
-
-
-5. pnml support:
-----------------
-
-As  of 2.8.0,  the  tina tools  support  the PNML  (Petri Nets  Markup
-Language) format as  an alternative to .net or  .ndr. The PNML support
-is still evolving,  check the formats man page  for details about PNML
-support by tina.
-
-
-6. help, feedback:
-------------------
-
-Please report bugs or other problems to the author at bernard@laas.fr.
-All comments/questions are also welcome on the tina-users forum:
-
-	register at url: http://sympa.laas.fr/wws/info/tina-users
-	post at address: tina-users@laas.fr	
-
-Enjoy,

libs/tina-3.7.0/README

-ABOUT TINA :
-------------
-
-Tina (TIme petri Net Analyzer) is  a toolbox for the analysis of Petri
-Nets and Time Petri Nets. The latest version of Tina may be downloaded
-from the web page www.laas.fr/tina, tab Download.
-
-At that time, the toolbox includes:
-
-nd (NetDraw) : Time Petri net and Automata editor.
-~~~~~~~~~~~~~~
-Allows one to create a {Time} Petri nets, in textual or graphical form.
-Interfaced with some of the following tools.
-
-tina : construction of reachability graphs.
-~~~~~~
-Depending upon the  option retained, builds (references at  the end of
-file):
-
-The coverability graph of a Petri net, by the Karp and Miller technique.
-
-The  markings reachability  graph of  a  Petri net  (untimed, or  with
-timing information discarded).
-
-The covering  step graph  of a Petri  net, according to  the technique
-introduced in (6,7), preserving various properties.
-
-The partial marking  graph of a Petri net  according to the persistent
-sets method,  as well as  three experimental variants of  it combining
-persistent sets and covering steps, described in (8).
-
-Various  state space  abstractions for  Time Petri  nets  (state class
-graphs),  following the  techniques introduced  in (1,2),  and further
-refined  in (3,5).   Depending  on option  selected, the  construction
-perserves markings, states, LTL  properties, or CTL* properties of the
-concrete state space of the Time Petri net.
-
-sift: Construction and checking of reachability graphs.
-~~~~~
-Sift is  a specialized version of  tina supporting in  addition on the
-fly verification  of reachability  properties. If offers  less options
-than  tina but  is  typically faster  and  requires considerably  less
-space.
-
-struct :  structural analysis of Petri nets.
-~~~~~~~
-Computes  generator sets  for  semi-flows or  flows  on places  and/or
-transitions  of  a Petri  net.   Also  determines  the invariance  and
-consistency properties.
-
-path : path analysis of Time Petri nets.
-~~~~~~
-Given a  firable sequence of  transitions, this tool computes  all, or
-one of, depending  on options, firing schedule that  has this sequence
-as support.
-
-selt : A State/Event LTL model checker.
-~~~~~~
-This tool checks a Kripke  transition system against S/E-LTL formulas,
-interactively or in batch mode.   Produce counter examples reusable by
-the nd  stepper. For converting  S/E-LTL formula into  Buchi automata,
-selt  relies on  the spin  converter (bundled)  or on  Oddoux/Gastin's
-ltl2ba (www.lsv.fr/~gastin/ltl2ba).
-
-muse: A modal mu-calculus model checker.
-~~~~~
-Model  checks a  Kripke transition  systems against  modal mu-calculus
-formula.  Muse computes the set of states obeying some formula. A path
-to some  state can then be  computed using the pathto  and plan tools,
-and that path replayed on the model using tool play or the nd stepper.
-
-play: Stepper simulator.
-~~~~~
-Allows to simulate interactively and  step by step net descriptions in
-all formats accepted  by tina.  Its capabilities are  similar to those
-of the  nd stepper except that  play may also  simulate nets augmented
-with data processing (in tina tts format).
-
-pathto: Path finder.
-~~~~~~~
-A utility tool computing the path to some state in a  kripke transition system.
-
-ndrio : conversion tool for nets.
-~~~~~~~
-A tool for  converting Petri nets and Time  Petri nets between various
-formats, including tina formats .net, .ndr and .tpn, and .pnml.
-
-ktzio : conversion tool for transition systems.
-~~~~~~~
-A  tool   for  converting  labelled  transition   systems  (or  Kripke
-transition  systems) between various  formats, including  formats .ktz,
-.aut, .bcg, .mec, and textual formats.
-
-frac: Fiacre to tina tts compiler.
-~~~~~
-A companion  tool, not distributed  with the toolbox but  available at
-the companion site "http://projects.laas.fr/fiacre".  Fiacre is a high
-level description language for real time systems; frac compiles Fiacre
-descriptions into Time Petri nets enriched with data processing (in tina
-tts format) that can then be checked with the TINA tools.
-
-
-INSTALLATION:
-------------
-
-Read file INSTALL  for installation notes, 
-man pages in various formats are found in directory doc.
-
-The Tina toolbox is property of LAAS-CNRS, 7, avenue du Colonel Roche,
-31077, Toulouse.   For any comments, bug reports  or specific demands,
-please contact the author at bernard.berthomieu@laas.fr.
-
-The binary distributions  of the Tina toolbox may  be freely installed
-and used.  The software is  distributed "as is", without warranties or
-conditions of any kind.
-
-
-REFERENCES : (please check www.laas.fr/tina, tab papers, for updates)
-------------
-
-(1) B.  Berthomieu, M. Menasche, An Enumerative Approach for Analyzing
-    Time Petri Nets, IFIP Congress 1983, Paris, 1983.
-
-(2) B.   Berthomieu,  M.   Diaz,  Modeling and  verification  of  time
-    dependent  systems using  time Petri  nets.  IEEE  Transactions on
-    Software Engineering, 17(3), 1991.
-
-(3) B. Berthomieu, La méthode des Classes d'états pour l'Analyse des Réseaux
-    Temporels - Mise en Oeuvre, Extension à la multi-sensibilisation.
-    Modélisation des Systèmes Réactifs, MSR'2001, Hermes, 2001.
-
-(4) B.  Berthomieu,  P.-O.  Ribet,  F.  Vernadat,  The  tool  TINA  --
-    Construction  of Abstract  State Spaces  for Petri  Nets  and Time
-    Petri Nets, International Journal of Production Research, Vol. 42,
-    No 4, July 2004.
-
-(5) B. Berthomieu, F. Vernadat, State class constructions for branching
-    analysis of Time Petri nets, TACAS 2003. Springer Verlag LNCS 2619,
-    2003.
-
-(6) F. Vernadat, P. Azéma, F. Michel, Covering Step Graph, Application
-    and Theory of Petri Nets 96, Springer Verlag LNCS 1091, 1996.
-
-(7) F. Vernadat, F. Michel, Covering Step Graph Preserving Failure Semantics,
-    Application and Theory of Petri Nets 97, Springer-Verlag LNCS 1248, 1997.
-
-(8) P-O. Ribet, F. Vernadat, B. Berthomieu, On Combining the Persistent Set
-    Method with the Covering Step Graph Method, FORTE 2002, Springer Verlag
-    LNCS 2529, 2002.
-
-(9) B.  Berthomieu,   P.-O.  Ribet,  F.  Vernadat,   L'outil  TINA  --
-    Construction d'espaces d'états abstraits pour les réseaux de Petri
-    et réseaux Temporels, Modélisation des Systèmes Réactifs, MSR'2003,
-    Hermes, 2003.

libs/tina-3.7.0/bin/plughelp

-#!/bin/sh
-#
-echo " 
-As of  Version 2.7.4, nd offers  the users the  capability of invoking
-their own  tools from  nd; this file  explains how to  proceed.  These
-tools may be  for instance transformation tools for  nets or automata,
-or  tools for computing  specific information  from nets  or automata.
-This  text is itself  produced by  a tool  interfaced that  way, named
-plughelp.
-
-Plugging a new tool is done in 2 steps:
----------------------------------------
-
-1. Declare the  tool by adding  a mount command  for the tool  in file
-bin/plugins/ndmount. For  instance, for having access  to the plughelp
-tool in this particular edition mode of nd, we added the line:
-
- mount PlugHelp {how to add your own tools here} $2 .txt plughelp.tcl
-
-The synopsis of  the mount command is:
-
-    mount name label intype outtype [script]
-
-Where the arguments are:
-
-name: Identifies the tool, must be a legal tcl namespace identifier.
-
-label: The  entry added  into the  nd tool menu  for the  tool. Unless
-entirely alphanumeric, should be enclosed in braces.
-
-intype: The  type of  data expected  by the tool,  one of  .ndr, .net,
-.adr, .aut.  The tool will  be mounted whenever the nd buffer contains
-data of that type.  If your tool can operate on several input types, a
-mount command must be provided for each type.
-
-outtype:  The type  of results  produced by  the tool,  all  types are
-accepted but the  data should be textual.  The  results will appear in
-an nd window that can be  saved or closed.  In addition, if outtype is
-one of the types accepted as  input by nd, the window contents will be
-loadable into nd.  Click in the window for the available choices.
-
-script: If the tool has no  options, the name of the executable is the
-first parameter  (name), and  the tool operates  as a  filter (reading
-data on standard input and returning results on standard output), then
-this parameter may  be omitted.  Otherwise you must  specify a control
-panel  and a  commandline for  the tool,  as explained  in  (2) below.
-Argument  script   is  the   name  of  the   tcl  file   holding  this
-specification.
-
-When started, nd searches  for file bin/plugins/ndmount.  If that file
-exists,  then the  mount commands  it contains  are  evaluated.  Thus,
-modifications of ndmount will be effective at the next call of nd.
-
-If your tina distribution is  shared among several users, and you want
-to plug a private application,  then you should first create a private
-setup file for nd (help->setup,  then save), and append the above line
-to the setup  file created in your home  directory (.ndrc or ndrc.txt,
-depending on platform) instead of the ndmount file.
-
-
-2. Optionally, specify  a control  panel for the  tool, and  a command
-line.  This is done by creating a tcl file defining a namespace fo the
-tool holding  two procedures: controls  and command. At run  time, the
-file    must    reside    in    bin/plugins.   For    instance,    the
-bin/plugins/plughelp.tcl file holds:
-
-  namespace eval PlugHelp {
-
-    proc controls {} {
-        radiobox PlugHelp::flg1 \"first flag\" \"quiet verbose\" \"-q -v\" -v
-        fieldsbox PlugHelp::values \"parameters\" \"first second\" \"0 {}\"
-        radiobox PlugHelp::flg2 \"second flag\" \"slow fast\" \"-O1 -O6\" -O1
-    }
-
-    proc command {} {
-        return \"plughelp $::bin $::intype \\
-	        \$PlugHelp::values(first) \$PlugHelp::flg1 \\
-	        \$PlugHelp::flg2 \$PlugHelp::values(second)\"
-    }
-  }
-
-The name of the namespace MUST  be identical to the first parameter of
-the mount command for the tool.
-
-Procedure controls  offer the  user to set  the options for  the tool.
-Additional Confirmation and Cancel buttons  are provided by nd. If you
-are  fluent in  tcl, you  can  put what  you want  in this  procedure,
-suffice  to know that  all widgets  defined in  the procedure  must be
-packed into a  frame named .z.controls. In most  cases, however, these
-controls  can be easily  specified using  the two  predefined commands
-provided by nd explained below. These are:
-
-radiobox:
-  Defines a group of radiobuttons, typically for choosing the
-  value of an option among several choices.
-  Its synopsis is:	
-    radiobox var label choices values initial
-  where:
-    var is a variable of shape Name::flagname (Name is the namespace);
-    label is a title for the group of radiobuttons;
-    choices is a list of labels identifying the different options;
-    values is the list of corresponding option values;
-    initial is the default value.
-
-fieldsbox:
-  Defines a group of parameter entries.
-  Its synopsis is:    
-    fieldsbox var label tags initials
-  where:
-    var is an array variable of shape Name::aname (Name is the
-	namespace identifier, aname is a tcl array);
-    label is a title for the group of entries;
-    tags is a list of labels identifying nthe individual entries;
-    initials is the list of default values for the entried.
-
-Procedure command returns a suitable  command line for the tool, built
-from the  name of the executable,  possibly prefixed by  its path, and
-from the values  of the options and parameters, as  shown in the above
-example. It is the responsability  of the tool to check consistency of
-parameters and options.
-
-nd will first search for the  executable in the bin directory of tina.
-Unless the  home directory of your  tool is the Path  variable of your
-environment,  you should  put a  copy of  the executavble  in  the bib
-directory of tina.
-
-Finally, nd assumes  by default that tools operate  as filters, taking
-their  input  on standard  input  and  returning  results on  standard
-output. If your tool operates  on file(s) instead, then you must place
-the keywords infile and/or outfile in the command line description, at
-the places where the input  file and/or output file are expected.  For
-invoking the  tool, nd  will create temporary  files if  necessary and
-replace these keywords with their names, with intype and/or outtype as
-extensions.
-
-What information is available to the tools:
--------------------------------------------
-
-The tool receives  on its standard input, or  through a temporary file
-if made precise  in the command procedure, the  description of the net
-or automaton in the current nd buffer.
-
-The parameters  specified in the  control procedure are passed  to the
-tool  as  specified in  the  command  procedure.  For this  call,  for
-instance, we have:
-
-    first flag = $4
-    second flag = $5
-    first parameter = $3
-    second parameter = $6
-
-In  addition, a  few predefined  variables  may be  useful for  tools.
-These include:
-
-::home contains the path of tina bin directory (where nd resides).
-::intype : contains  the input type of the  tool invoked.
-
-For this call, we have:
-
-    $::home = $1
-    $::intype = $2
-"

libs/tina-3.7.0/bin/plugins/ndmount

-
-# One line per tool, and per input format for which the tool is available.
-# Each line constituted of:
-#
-# mount
-# name	
-#	plugin identifier
-#	if desc.tcl is provided
-#	then must be the name of the namespace declared in desc.tcl
-#	else must be the name of the executable
-# label 
-#	entry label in tool menu
-# input_format
-#	input format, one of .ndr, .net, .adr, .aut
-# output_format
-#	arbitrary, but textual
-# desc.tcl
-#	optional
-#	tcl file specifying the control panel and the command line
-#	if no controls are necessary and the tool operates as a filter
-#	then the file may be omitted. The executable name is then
-#	taken then as the above name.
-
-
-# .ndr tools
-mount PlugHelp {how to add your own tools here} .ndr .txt plughelp.tcl
-
-# .net tools
-mount PlugHelp {how to add your own tools here} .net .txt plughelp.tcl
-
-# .adr tools
-mount PlugHelp {how to add your own tools here} .adr .txt plughelp.tcl
-
-# .aut tools
-mount PlugHelp {how to add your own tools here} .aut .txt plughelp.tcl
-

libs/tina-3.7.0/bin/plugins/plughelp.tcl

-
-namespace eval PlugHelp {
-
-    proc controls {} {
-	wm title .z "example flags"
-        radiobox PlugHelp::flg1 "first flag" "quiet verbose" "-q -v" -v
-        fieldsbox PlugHelp::values "parameters" "first second" "0 none"
-        radiobox PlugHelp::flg2 "second flag" "slow fast" "-O1 -O6" -O1
-    }
-
-    proc command {} {
-        return "plughelp [list $::home] $::intype \
-	        [list $PlugHelp::values(first)] $PlugHelp::flg1 \
-	        $PlugHelp::flg2 [list $PlugHelp::values(second)]"
-    }
-}