Maxsteps options in TINA 3.8.0

Summary

In addition, for experiments and further investigations, Version 3.8.0 offers three more "steps" constructions:

- Construction -Zv, or -sleptsov, implements a slight variation of the firing rule discussed in [3] in the list of references given at the bottom of this page, in which transitions always fire at their maximum multiplicity, individually. The differences with [3] are discussed in the references section too.
- Construction -Zi, or -salwicki [6], builds marking graphs using a firing rule referred to as the "Salwicki" rule: firing maximal sets of simultaneously firable transitions;
- Construction -Zvi [2], combines the two previous: it fires maximal bags of transitions, that is maximal sets of simultaneously firable transitions, each possibly firing at some multiplicity.

All three constructions are supported by tools tina, sift and walk. Each tentatively 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 two 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 so-called spleptsov firing rule for simulation.

Example usage of tina, sift, walk with these firing rules

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 (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

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 tool instead, as follows:

Counting the number of deadlocks in a ktz file with scan:

scan pol15.ktz -dead -c

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):

scan pol15.ktz -dead -s
scan pol15.ktz -dead -m > deadlocks

Some references

On the "Sleptsov" rule and applications:

1. Bernard Berthomieu, Dmitry A. Zaitsev, Sleptsov Nets are Turing-complete, Theoretical Computer Science, Volume 986, 2024, 114346, ISSN 0304-3975.
[editor] [author]
2. Dmitry A. Zaitsev, Strong Sleptsov nets are Turing complete, Information Sciences, Vol. 621, 2023, 172-182. [editor] [author]
3. Dmitry A. Zaitsev, Sleptsov Nets Run Fast, IEEE Transactions on Systems, Man, and Cybernetics: Systems, 2016, Vol. 46, No. 5, 682 - 693. [editor]
4. Dmitry Zaitsev and Jan Jürjens. Programming in the sleptsov net language for systems control. Advances in Mechanical Engineering, 8(4):1687814016640159, 2016. [pdf]
5. A. I. Sleptsov. State equations and equivalent transformations of loaded petri nets (algebraic approach). In Formal models of parallel computations: Proceedings of all-USSR conference, Novosibirsk (Russia), pages 151–158, 1988. (in Russian)

On the "Salwicki" rule:

6. Hans-Dieter Burkhard. On priorities of parallelism: Petri nets under the maximum firing strategy. In Workshop on Logic of Programs, pages 86–97. Springer LNCS 148, 1980. [editor] [author]
7. Andrzej Salwicki and Tomasz Müldner. On the algorithmic properties of concurrent programs. In Logic of Programs: Workshop, ETH Zürich, May–July 1979, pages 169–197. Springer, 1981. [editor] [author]

On steps semantics:

8. Ugo Montanari and Francesca Rossi. Contextual nets. Acta Informatica, 32:545–596, 1995. [editor] [author]
9. Nadia Busi and G. Michele Pinna. Non sequential semantics for contextual p/t nets. In International Conference on Application and Theory of Petri Nets, pages 113–132. Springer, 1996. [editor] [author]
10. Walter Vogler, Alex Semenov, and Alex Yakovlev. Unfolding and finite prefix for nets with read arcs. In CONCUR’98 Concurrency Theory: 9th International Con- ference Nice, France, September 8–11, 1998 Proceedings 9, pages 501–516. Springer, 1998. [editor] [author]
11. François Vernadat, Pierre Azéma, and François Michel. Covering step graph. In Application and Theory of Petri Nets 1996: 17th International Conference Osaka, Japan, June 24–28, 1996 Proceedings 17, pages 516–535. Springer, 1996. [editor] [author]

Note: -Zv vs sleptsov rule in [3]:

First, TINA, even in modes -Z*, support generalized Read and Inhibitor arcs, while [3] only considers ordinary inhibitor arcs;

Next, for the definition of steps, we follow [8,9]: a step is a set (or bag) of simultaneously firable transitions, where "simultaneously firable" implies "in any order", while [3] interprets "simultaneously firable" as "does not make negative the marking of some place". As a consequence, and conversely to that of [3], our treatment guarantees that the transitions in any step are successively firable, which in turn implies that all markings reachable in modes -Zv, -Zi, -Zvi are reachable in the interleaving semantics (-R) of the net, and that we can get rid of inhibitor and read arcs when the net is bounded.