OBJSA NET SYSTEMS

OBJSA Net Systems are high-level Petri Nets in which
1) the net can be decomposed in State-Machine Components and
2) the domains to which individual tokens belong are defined as abstract data types using the OBJ2 language.

Definition

(according to [chi94])

An OBJSA Net System is a couple C=(N, A) where
N is an extended SA Net and
A is an OBJ algebraic specification.
There are the following relations between N and A:

every elementary subnet of N is associated with an object OBJ of A, which specifies the token domain of the subnet
every transition is associated with an OBJ module which introduces:
- variables associated with the input arcs
- a predicate which specifies an additional condition for the transition enabling
- operators associated with the output arcs which specify the changes of the token data
the initial marking consists in a formal sum of algebraic terms (ground term) which sort is defined in 1.

Transition Rule

A transition is enabled when
(i) the input places contain at least as many tokens as specified by the labelling of the transition input arcs; and
(ii) there exists a binding of these tokens to the free variables occuring in the transition input arcs such that the predicate inscribed in the transition is satisfied.
Its occurrence removes the involved tokens from the input places and add to each output place the tokens obtained according to the labelling of the transition output arcs, under the same binding.

Sample Net

(from [bat94])

OBJSA Model of a Sender | Port | Receiver system:

Tools

The incremental tool environment ONE.

References

E. Battiston, F. De Cindio, G. Mauri: OBJSA Nets: A class of high-level nets having objects as domains [bdm88]
A. Chizzoni: CLOWN: CLass Orientation With Nets [chi94]

BACK