[logo]www.petriweb.org

Not logged in

On the repository: On external files: About Petriweb

Select nets by specifying required properties

Help me


Choose the required properties below:

The name of the net. The value of this property is set by hand name
A description of the net. The value of this property is set by hand description
The filename from which this net was uploaded. The value of this property is set by hand uploaded from
Meta-properties
Title of the publication from which the net was taken. The value of this property is set by hand publication title
Author of the publication from which the net was taken. The value of this property is set by hand author
Number of the figure in which the net appears, as indicated in the original publication. The value of this property is set by hand figure number
Structural properties
The number of places in the net. The value of this property is calculated automatically nr of places
The number of subnets in the present net. The value of this property is calculated automatically nr of subnets
The number of transitions in the net. The value of this property is calculated automatically nr of transitions
The number of inhibitor arcs in the net. An inhibitor arc tests for the absence of tokens in a place. Many other properties become undefined (or at least, ought to be) in the presence of inhibitor arcs. The value of this property is calculated automatically nr of inhibitors
The number of reset arcs in the net. A reset arc clears a place of tokens.Many other properties become undefined (or at least, ought to be) in the presence of reset arcs. The value of this property is calculated automatically nr of reset arcs
There is a undirected path between every two nodes (places or transitions). The value of this property is calculated automatically connected yes no (ignored)
There is a directed path between every two nodes (places or transitions). The value of this property is calculated automatically strongly connected yes no (ignored)
The multiplicity of every arc is one. The value of this property is calculated automatically ordinary yes no (ignored)
Every transition has exactly one input place and exactly one output place. The value of this property is calculated automatically state machine yes no (ignored)
Every place has exactly one input transition and exactly one output transition. The value of this property is calculated automatically marked graph yes no (ignored)
Loop-free: no transition has an input place that is also an output place. The value of this property is calculated automatically pure yes no (ignored)
For any place, all outgoing arcs have the same multiplicity. The value of this property is calculated automatically homogeneous yes no (ignored)
If two places have a common input transition, the output transitions of one are a subset of the output transitions of the other. The value of this property is calculated automatically extended simple yes no (ignored)
For each input arc to a place, some output arc has at least the same multiplicity. The value of this property is calculated automatically with a nonblocking multiplicity yes no (ignored)
No two transitions have the same input places. The value of this property is calculated automatically statically conflict-free yes no (ignored)
All (different) transitions with a shared input place have no other input place. The value of this property is calculated automatically simple free-choice yes no (ignored)
Any two transitions with the same input place have the same set of input places. The value of this property is calculated automatically extended free-choice yes no (ignored)
For each transition, the sum of input arc multiplicities equals the sum of output arc multiplicities. The value of this property is calculated automatically conservative yes no (ignored)
For each transition, the sum of input arc multiplicities equals or exceeds the sum of output arc multiplicities. The value of this property is calculated automatically subconservative yes no (ignored)
If a set of components is given such that the corresponding sub-nets define strongly connected state machines, and their union equals the set of all places in the net. The value of this property is calculated automatically state machine decomposable yes no (ignored)
In a state machine decomposable net, every transition has a pre-place; a pre-place allocation is a mapping which assigns to each transition one of its pre-places. A component is said to be selected in a pre-place allocation, if to all transitions that have a pre-place in the component, a pre-place in the component is assigned. The net is said to be state machine allocatable, if every pre-place allocation selects a strongly connected state machine component . The value of this property is calculated automatically state machine allocatable yes no (ignored)
The value of this property is calculated automatically with a nonempty clean trap yes no (ignored)
Every place takes a positive value in some P-invariant. The value of this property is calculated automatically covered by semipositive p-invariants yes no (ignored)
Every transition takes a positive value in some T-invariant. The value of this property is calculated automatically covered by semipositive t-invariants yes no (ignored)
The net contains one or more places without input transitions. The value of this property is calculated automatically with source place(s) yes no (ignored)
One or more places have no output transitions. The value of this property is calculated automatically with sink place(s) yes no (ignored)
Distinct places i without inputs and f without outputs exist such that all nodes (places and transitions) are on a directed path from i to f. The value of this property is set by hand p-workflow yes no (ignored)
One or more transitions have no input places. The value of this property is calculated automatically with source transition(s) yes no (ignored)
One or more transitions have no output places. The value of this property is calculated automatically with sink transition(s) yes no (ignored)
A component of a net is a set of places which is both a deadlock and a trap. It defines a sub-net comprising these places and the adjoining transitions. If a set of components is given such that the corresponding sub-nets define state machines, and their union equals the set of all places in the net, then this net is said to be state machine coverable. The value of this property is calculated automatically state machine coverable yes no (ignored)
Two distinct transitions i, without inputs, and f, without outputs, exist such that all nodes (places and transitions) are on a directed path from i to f. The value of this property is set by hand t-workflow yes no (ignored)
Behavioural properties
One or more tokens are present. The value of this property is calculated automatically marked yes no (ignored)
Exactly one token is present. The value of this property is calculated automatically marked with exactly one token yes no (ignored)
No reachable marking has more than k tokens on any place. The value of this property is calculated automatically bounded yes no (ignored)
Bounded in every initial marking. The value of this property is calculated automatically structurally bounded yes no (ignored)
All transitions can always be enabled. I.e. for every transition, from every reachable marking, some marking can be reached in which the transition can fire. The value of this property is calculated automatically live yes no (ignored)
(See the definitions of 'live' and 'safe'.) The value of this property is calculated automatically live and safe yes no (ignored)
In every reachable marking, there is no more than one token on a place. The value of this property is calculated automatically safe yes no (ignored)
A P-workflow that, when provided with a marking of a single token in its initial place, will inevitably reach a making of a single token in its final place. The value of this property is set by hand 1-sound yes no (ignored)
A P-workflow that, when provided with a marking consisting of only tokens in its initial place, will inevitably reach a marking consisting of the same number of tokens in its final place. The value of this property is calculated automatically generalized sound yes no (ignored)
The lowest integer k for which the net is not k-sound, or 0 if no such k exists. The value of this property is calculated automatically k-unsoundness
In all reachable markings, no transition can be disabled by firing another. The value of this property is calculated automatically dynamically conflict-free yes no (ignored)