Maximum Steps TINA options
Contents
The traditional Tina distributions in tina pages
offer several partial order constructions, including
the covering steps construction (option -V), persistent sets (option -P), and a combination of these (option -Q).
In addition, for experiments and further investigations, the distributions in this page offer three more "steps" constructions:
Construction -Zv, or -sleptsov, builds marking graphs using a firing rule referred to as the "Sleptsov" rule:
in which transitions always fire at their maximum multiplicity, individually;
Construction -Zi, or -salwicki, builds marking graphs using a firing rule referred to as the "Salwicki" rule:
firing maximal sets of simultaneously firable transitions;
Construction -Zvi, or -sleptsalw, combines the two previous: it fires maximal bags of transitions, that is maximal
sets of simultaneously firable transitions, each possibly firing at some multiplicity.
These constructions are explained in details in paper
[editor] [arxiv]
(see also [this recent result]).
All three are supported by tools tina, sift and walk.
Each accept inhibitor arcs and read arcs, but only the first accepts priorities;
while there is a sensible interpretation of priorities for -sleptsov, this is far less obvious for the other options.
Tool nd supports these firing rules in the following sense:
- when calling tina or sift on a net, you may choose any of the above construction in the
"partial graphs" group. This will call tina or sift with the corresponding option;
- the stepper has an additional "sleptsov" option in its mode menu, in addition to the untimed
(Petri rule) and timed (TPN rule) options. When selected, the stepper will use the spleptsov
firing rule for simulation.
Downloads
Tina distributions supporting these features are available on the tina preview page.
Example usage of tina, sift, walk:
Counting markings; with sift (generally faster) or tina:
sift -sleptsov pol15.net
tina -sleptsov -g -q pol15.net log
Building state spaces stored in ktz representation; with sift (typically faster) or tina:
sift -sleptsov pol15.net pol15.ktz
tina -sleptsov -g pol15.net pol15.ktz
Counting the number of deadlocks in a ktz file:
muse pol15.ktz -f "- <T>T" -c -q
Printing the list of deadlocks in a ktz file (each printed as its state index in the ktz file):
muse pol15.ktz -f "- <T>T" -s -q
[As of Sep 13 2023:] Printing the list of deadlocks in a ktz file in clear:
muse pol15.ktz -f "- <T>T" -m -q
For large nets (e.g. pol50.net), muse may need a huge amount of space, you may wish to use the new scan utility instead, as follows:
Counting the number of deadlocks in a ktz file with scan:
Printing the deadlocks found in a ktz file with scan (as their indices in the ktz file with -s, or in clear in file deadlocks with -m):
[As of Sep 13 2023:] -v option of scan has been renamed -m
scan pol15.ktz -dead -s
scan pol15.ktz -dead -m > deadlocks
Printing in clear the first deadlock computed by sift, with the -dead option:
sift -sleptsov -dead pol15.net
Same by walk; walk will stop if a deadlock is found, and print it, or it will loop forever if none is found:
[As of Sep 16 2023:] Printing the number of deadlocks of a net without priorities with tedd. Note: only the default firing rule is supported.
tedd -dead-states mynet.net -q
Printing in clear the deadlocks of a net without priorities with tedd. Note: only the default firing rule is supported.
tedd -dead-states mynet.net -v
Last updated: Fri Sep 17 15:51:41 CEST 2023