LIP6 UPMC CNRS Move-team Macao FrameKit CPN-AMI
2008-11-01
LIP6 > Software > MoVe Sofware > CPN-AMI > Manual > Structural bounds

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.

Bas