Introduction
Some of the bound services have been implemented by our team. Some other
come from LoLA,
a tool developed at the Humboldt-university zu Berlin.
The service menu
When the Place/Transition net you have designed is syntactically correct,
you can reach the service (in red). To operate
the service "Is a place bounded", you must select a place in
the model window.
Bounds
|
|
Compute structural bounds
|
|
Is the net structuraly safe?
|
|
Is the net structurally bounded?
|
|
Compute bounds structural by unfolding
|
|
Is the colored structurally net safe (by
unfolding)?
|
|
Is the colored net structurally bounded?
|
|
Options
|
|
|
Suppress structuraly useless places and transitions
|
An option can be set to optimize the net when unfolding it by deleting
structurally useless places and transitions (basically, 0-bounded ones).
Display of Results (P/T nets)
Let us consider this small P/T net.
P/T net example
The computation of bounds provide this result.
Computation of bounds for a P/T net.
Display of Results (Colored
nets)
Let us consider this small colored net.
Colored Petri net example.
The computation of bounds by unfolding provides the followin result.
Result display in the historic window.
This result show that anly a token <1,2> can take place in place
Ext_Mem_Acc. Place names are computed after the name of the colored place
they are issued from concatenated with the corresponding color value.
|