Introduction

AMI-Nets are well formed net dressed with a specific syntax. This enables to syntax check the model and to detect basic modelling errors before working on the semantics aspects.

General Definitions

The AMI net model is a high-level net model that includes, besides the graphical features of a Place/Transition Petri net - places, transitions and arcs - textual information like:

• place and transition domains, and transition guards,
• an enriched syntax for arc labels and place markings,

This information is used for the definition of the semantics of an AMI net, which is briefly and informally described in the next section.

Behavior of an AMI-Net

The behavior of an AMI net is controlled by the same set of rules used for general colored nets:

• A domain is associated with each place and transition of the model. Elements of these domains are called colors.
• When firing, a transition is binded by an element of its domain.
• Each token in a place is colored by an element of the place domain (several tokens may have the same color). The marking of a place is thus a multiset of colors - a set in which an element may occur several times.
• For a binded transition to be enabled, each input place of the transition must contain a sufficient (possibly null) number of tokens for every color of the place domain. These tokens will be taken from the place when the transition fires. Similarly, the firing will produce colored tokens in the output places of the transition. Like in Ordinary Petri nets, the label attached to the arcs determines the number of tokens to be taken or produced. However, this label is now a color function that associates a multiset of colors of the place domain with each binding of the transition.
• Independently from the evaluation of the color functions, a transition may not be enabled if its binding does not satisfy some predicate. This predicate is called the guard of the transition.

Declarative part of an AMI-Net

The description of an AMI net is made of two parts. The first part contains the declaration of the Petri net (places, transitions and arcs). This declaration is included in the present model. We describe in the second part, all the high-level features of the model for which we give the syntactic construction rules.

Those high-level features have been listed in the former section. However, their description, i.e., the description of the domains, the markings, the guards, the priorities together with the color.

These descriptions are done in different sections that are all optional :

• The class declaration section defines object classes. The objects are the elementary entities (sites, memories, etc…) that appear in the description of the model;
• The domain declaration section defines the set of color domains associated with the different places and transitions of the net. A color associates one or several elements in a tuple;
• The variable declaration section defines the name and the domain to which variables used for the valuation of the arcs belong.

In the rest of the document, keywords are written with courier bold characters.

Class Declaration

The keyword CLASS determines the beginning of the section in which the object classes that appear in the net are defined. All the classes must have different names : a class cannot be declared several times.

A class is defined by its name (identifier) and the set of objects it contains. This set of objects can be described either by an interval, or by an enumeration of the objects. INTEGER and CHAR, respectively the set of integers and the set of ASCII characters included in [a..z] U [A..Z], are predefined in the analyzer.

CLASS
	C1 IS INTEGER ;
	C2 IS [ a, b, c, d ] ;
	C3 IS CHAR ;
	C4 IS 1..10 ;
	C5 IS a..i ;

Several classes having the same definition can be declared at the same time. This facility will be useful when the further extensions of the language allow classes with the same definition to have different properties.

CLASS
	C1, C2, C3 IS [ a, b, c ] ;

Remarks

1. A class can contain any positive number of elements.
2. The fact that a class is ordered or not is deduced from the color functions that appear in the net. In that case, the order of the elements is given by their enumeration order in the declaration.
3. Objects belonging to different classes can have the same name.
4. An identifier must begin by a letter or an underscore. An lonely underscore is a correct identifier.
5. The bounds of an interval are either integers or characters. The left bound must be less than the right bound.

BNF for the definition of classes :

<ClassSection>          ::= CLASS <ListClassDeclarations>
<ListClassDeclarations> ::= <ClassDeclaration> |
                            <ListClassDeclarations> <ClassDeclaration>
<ClassDeclaration>      ::= <ListClassNames> IS <ClassDescription>;
<ListClassNames>        ::= <ClassIdentifier> |
                            <ListClassNames>, <ClassIdentifier>
<ClassDescription>      ::= INTEGER |
                            CHAR |
                            <Interval> |
                            [ <ListElements> ]
<ListElements>          ::= <Element> | <ListElements>, <Element>
<Element>               ::= <ElementIdentifier>
<Interval>              ::= <PositiveInteger> .. <PositiveInteger> |
                            <Char> .. <Char>

Domain Declaration

The keyword DOMAIN determines the beginning of the section in which the domains of the places and the transitions that appear in the net are defined.

• A domain can be a class defined in section CLASS, or can be a Cartesian product of :
• classes defined in section CLASS
• domains already defined in section DOMAIN.

DOMAIN
	D1 IS C1;
	D2 IS <C1,C2>;
	D3 IS <D2,C3>;	equivalent to D3 IS <C1,C2,C3>

Domain D1 is class C1 and Domain D2 is defined as the cartesian product of C1 and C2. Like for the classes, several domains having the same definition can be declared at the same time.

DOMAIN
	D1,D2,D3 IS <C1,C2>; D1, D2 and D3 have the same definition

Remarks

1. There is only one predefined domain : the one which contains a single element. It is called Null domain and no color is defined in it (a unique color gives no information on the identity).
2. The place domains are defined explicitly, whereas for a transition the domain is derived from the examination of the functions around the transition (see "Arc Labels", page 15).

BNF for the definition of domains :

<DomainSection>          ::= DOMAIN <ListDomainDeclarations>
<ListDomainDeclarations> ::= <DomainDeclaration> |
                             <ListDomainDeclarations> <DomainDeclaration>
<DomainDeclaration>      ::= <ListDomainNames> IS <DomainDescription>;
<ListDomainNames>        ::= <DomainIdentifier> |
                             <ListDomainNames>, <DomainIdentifier>
<DomainDescription>      ::= <DomainProduct> |
                             <ClassOrDomainIdentifier>
<DomainProduct>          ::= < <ListComponents> >
<ListComponents>         ::= <Component> |
                             <ListComponents> , <Component>
<Component>              ::= <ClassOrDomainIdentifier>

Declaration of variables

The keyword VAR determines the beginning of the section in which variables are defined. It is not necessary to declare all the variables that appear in the expressions labelling the arcs of the net. The domain of an undeclared variable will be derived from the information on the place connected to the arc.

A domain is associated with each variable. This domain is either a domain defined in section DOMAIN, or a class defined in CLASS section.

VAR
	X12 IN D2;
	XPC1, YPC1 IN PC1;   XPC1 and YPC1 have the same domain PC1

Like for classes and domains, several variables belonging to the same domain can be declared at the same time.

Remarks

1. A variable can be declared only once.

BNF for the definition of variables :

<VariableSection>          ::= VAR <ListVariableDeclarations>
<ListVariableDeclarations> ::= <VariableDeclaration> |
                               <ListVariableDeclarations> <VariableDeclaration>
<VariableDeclaration>      ::= <ListVariableNames> IN <ClassOrDomainIdentifier>;
<ListVariableNames>        ::= <VariableIdentifier> |
                               <ListVariableNames>, <VariableIdentifier>

Arc Valuation, Transition Guards and Place Marking

Arc Labels

If the domain of the place connected to the arc is null, the only possible labels are positive integers. Otherwise, the label is a linear combination of products (possibly reduced to one component) whose components are either class elements or predefined operations on class elements and variables.

Thus, the expression of arc labels uses the following components :

• class elements :
  • c. : element c
  • C.c : element c in class C
  • C.ALL : all elements of the class C
• predefined operations on class elements and variables :
  • c++n, c--n : the nth successor and the nth predecessor of element c.
  • X , X++n, X--n : variable X, the nth successor of X, the nth predecessor of X. ++ and -- operations can be applied only if the domain of X is a class.

2                            two non coloured token
<2>                          one constant coloured token "2"
<X>                          one coloured token of the colour domain of X
<X++2> + 2*<Y--1>            three tokens
<X, Y>                       one composed token
<X, C4.10>                   two non coloured token
<X++1,<Y, C.ALL>> + <X, <Y, Z>>   N+1 token if there are N colors in class C
2*<X++1, Y, C.ALL> + <X, Y, Z>   2*N+1 token if there are N colors in class C

The first two labels have different meanings. The first one refers to two tokens, whereas the second one refers to an object whose identity is 2. It is necessary to be careful when writing labels that are a difference of two or more expressions, like in our 7th example, because the analyzer will not control that the result is non-negative.

BNF for the definition of arc labels :

<ArcLabel>             ::= <ListElementaryExpr> |
                           <PositiveInteger>
<VarClassElement>      ::= <VariableOrObjectIdentifierOrPredefinedClassElement> |
                           <ClassIdentifier>.<ObjectIdentifier> |
                           <ObjectOrVariableIdentifier>++<PositiveInteger> |
                           <ObjectOrVariableIdentifier>--<PositiveInteger> |
                           <ClassOrDomainIdentifier>.ALL
<ListElementaryExpr>   ::= <ElementaryExpression> |
                           <ListElementaryExpr>+<ListElementaryExpr> |
                           <ListElementaryExpr>-<ListElementaryExpr>
<ElementaryExpression> ::= <ElementaryProduct> |
                           <PositiveInteger>*<ElementaryProduct>
<ElementaryProduct>    ::= < <ListProdElements> >
<ListProdElements>     ::= <ProdElement> |
                           <ListProdElements> , <ProdElement>
<ProdElement>          ::= <ElementaryExpression> |
                           <VarClassElement>

Transition Guards

The aim of a guard is to restrict the possible bindings of a transition by adding constraints on the variables. The guards are not defined in a particular section. They only appear in the information associated with a transition.

The guards included in the definition of AMI nets can compare (<, ², >, ³, ­) two variables class, or a variable and a constant. Both terms must belong to the same class or domain. For inequalities, the order of the elements is the enumeration order in the class declaration.

Guards can be combined using usual logical connectors AND, OR and NOT. It is also possible to add brackets in their expression.

[x > the_constant]
[X <> Y]
[(X < Y) AND (Y < Z)]
[(X < Y OR X < Z) AND X <> Q]

Remark

1. Predicate variables have to appear on the valuation of an input arc. They may also appear in the valuation of an output arc.

BNF for the definition of transition guards :

<TransitionGuard> ::= trUE | FALSE | [<Guard>]
<RelOp>           ::= = | < | > | <= | >= | <>
<Guard>           ::= trUE | FALSE |
                      NOT <Guard> |
                      (<Guard>) |
                      <Guard> AND <Guard> |
                      <Guard> OR <Guard> |
                      <VarClassElement><RelOp><VarClassElement> |

Description of a Marking

The initial marking of the net is not defined in a particular section. For every place, the initial marking is part of the information associated with the place. A marking is described as a list of tokens that may have a multiplicity greater than 1. A token is a product (possibly reduced to one component) of class elements or operations on class elements.

2                        two tokens
<2>, <3>, 2*<4>          and two  with identity 4.
<C.ALL, a>, 2*<x, y>     tokens with identity <x, y> (a, x, y are
                         objects, not variables).
<a++1>                   one token with identity a++1 (a is an object).

BNF for the definition of markings :

<InitialMarking>    ::= <ListMarkings>
<ListMarkings>      ::= <Marking> |
                        <ListMarkings> , <Marking>
<Marking>           ::= <MarkingExpression> |
                        <PositiveInteger>*<MarkingExpression>
<MarkingExpression> ::= <ElementaryProduct>

Macao and AMI-Nets

We describe here how AMI nets can be designed using MACAO editor. We describe all different available nodes and the associated information. For each information, we indicate the default value if any. Otherwise, "" is assumed by MACAO editor.

The declaration node

The declaration node has the shape given in Figure 1.

Figure 1 : Declaration node

This node contains the following information :

• declaration of classes, domains and variables using the syntax previously described,
• author, version, project, title are information that the designer uses at his convenience.

Places

There are two different kinds of places : classic places and queues (FIFO places). Their shape is given in Figure 2.

Figure 2 : Shape of places and queues.

These nodes contain the following information :

• name : a string value is expected,
• domain (default null) : null represents the neutral color domain. Otherwise, it must have been defined in the Declaration node,
• marking (no default) : the initial marking of the place,
• symbolic : not yet implemented,
• component : used as an extra data by prototyping tools in order to define interfaces between submodels.

Transitions

There are two different kinds of transitions : transitions with an exponentially distributed firing delay, and immediate transitions that fire in zero time. The information on timing and priorities is ignored when studying qualitative properties.

Figure 3 :transitions and immediate transitions.

These nodes contain the following information :

• name : a string value is expected,
• guard (default true) : the guard associated with the transition that must respect the syntax defined in Section 2.7.,
• priority : the default value for timed transitions is zero. The default value for immediate transitions is one,
• delay : for a timed transition, gives the mean of the exponential distribution.
• weight : For an immediate transition, the firing probability is given by the ratio of of the transition weight to the sum of the weights of all enabled immediate transitions,
• component : used by the prototyping tool.

Remark

delay, weight and component are not checked by SANDRINE, the Syntax checker in CPN-AMI (version 1.3 and 2.0)

Arcs

Figure 4 : Arcs and inibitor arc.

These arcs contain the following information :

• value (default 1) : contains the valuation of the arc that must respect the syntax defined in sections 2.3.2 and 2.3.4. The default value assumes that the place connected to the arc has a null domain.

A Petri net example

The philosophers are siting around a table. Each of them has got a plate in front of him and two forks : one on his left and one on his right. The fork situated to the left side of a philosopher is the one situated to the right side of the next philosopher around the table.

Each philosopher can be in two states, either he thinks or either he eats. Initially, all the philosophers are thinking. To go in the eating state, a philosopher has to take the two forks : one situated to his right side and one situated to his left side. So, no two adjacent philosophers, therefore, may eat simultaneously.

An eating philosopher conserves the two fork as long as he eats. When he has finished to eat the philosopher have to put the two forks back.

The model

The model of Figure 5 is a representation of the above problem. The philosophers are enumerated in the class C and there is one fork for each philosopher. An eating philosopher holds the fork labelled by his name and the one by the name of his neighbour.

Figure 5 : Petri Net of the famous philosophers

The two possible states of the philosophers are modelised by the two places : Thinking Philosophers and Eating Philosophers. The available forks are in the place named Forks.

The two transitions EAT and THINK model the two possible changes of state.

The transition EAT is firable for a given philosopher X when this one is in the place Thinking Philosophers and the two forks labelled X and X++1 are in the place Forks. Its firing takes the token X out of the place Thinking Philosophers and the tokens X and X++1 of the place Forks and produces a token X in the place Thinking Philosophers.

The transition THINK is fireable for an eating philosopher X. The firing of this transition produces the token X in the place Thinking Philosopher and take back the two forks labelled by X and X++1 in the place Fork.

Each time a philosopher X goes from the thinking state to the eating state (when the transition EAT is fired), the token X is produced in a counting place called Witness Place. When a philosopher X has eaten 100 times, the transition EatTooMuch may be fired and the token X is produced in the place FatPhilosopher.

Remark

Seeing the firing of the transition EAT takes out the two forks simultaneously, the deadlock problem of the classic modelisation of the philosophers is avoided.