6.2.1 Elementary net properties

ORD: ordinary

A net is said to be ordinary, if the multiplicity of every arc equals one [Sta90, Definition 2.3 (24)]. A coloured net is ordinary, if its unfolded net is ordinary.

HOM: homogenous

A net is said to be homogenous, if for any place p, all arcs starting at p have the same multiplicity [Sta90, Definition 14.4 (157)].

NBM: non-blocking multiplicity

A net has non-blocking multiplicity, if for each place p, the minimum of multiplicities of the arcs ending at p is not less than the maximum of multiplicities of the arcs starting at p [Sta90, Definition 15.3 (164)].

PUR: pure

INA checks, whether there is a transition in the current net, for which a pre-place is also a post-place. In this case, the net is not pure, i.e. not loop-free [Sta90]. Such nets are not live under the safe firing rule.

CSV: conservative

A net is said to be conservative, if all transitions add exactly as many tokens to their post-places as they subtract from their pre-places. In a conservative net, the total number of tokens is thus not altered by firing any transition. Therefore, the amount of tokens is an invariant. A net is sub-conservative, if all transitions add at most as many tokens to their post-places as they subtract from their pre-places. The total number of tokens can therefore not increase.

SCF: static conflict free

If two transitions have a common pre-place, they are in a static conflict about the tokens on this pre-place. Then, the net is not static conflict free [Sta90, Definition 3.4 (35)].

CON: connected

A net is said to be connected, if for each node in the net, there exists an undirected path to every other node [Sta90, Definition 14.1 (148)]. The direction of the arcs is thus ignored in the corresponding investigation.

SC: strongly connected

If a net is connected, it is checked whether each node also has a directed path to every other node, i.e. the direction of the arcs is also considered [Sta90, Definition 14.1 (148)].

One-sided nodes

Ft0: transition without pre-place

A net has Ft0-transitions, if there are transitions without a pre-place; $Ft=\emptyset$.

tF0: transition without post-place

A net has tF0-transitions, if there are transitions without a post-place; $tF=\emptyset$.

Fp0: place without pre-transition

A net has Fp0-places, if there are places without pre-transitions; $Fp=\emptyset$.

pF0: place without post-transition

A net has pF0-places, if there are places without post-transitions; $pF=\emptyset$.

Structures

MG: marked graph

A net is a synchronisation (or marked) graph, if every place has exactly one pre-transition and one post-transition. Here, arc multiplicities are ignored [Sta90, Definition 14.3.1 (152)].

SM: state machine

A net is a state machine, if every transition has exactly one pre-place and one post-place. Here, arc multiplicities are ignored [Sta90, Definition 14.3.2 (152)].

FC: free choice

A net has free choice, if every shared place is the only pre-place of its post-transitions [Sta90, Definition 14.3.3 (152)].

EFC: extended free choice

A net has extended free choice, if the post-transitions of shared places have the same pre-places [Sta90, Definition 14.3.4 (152)].

ES: extended simple

A net is extended simple, if the following holds: If two places have a common post-transition, then for one of them, its post-transitions are also post-transitions of the other place; i.e., one of the two places can also have other post-transitions [Sta90, Definition 14.3.5 (153)].