The LLAMAS language, syntax and semantics. - Software Modeling ...

Alexis Marechal Centre Universitaire d’Informatique Université de Genève 7 route de Drize, 1227 Carouge, Suisse

Didier Buchs Centre Universitaire d’Informatique Université de Genève 7 route de Drize, 1227 Carouge, Suisse

Technical report #221 (2013)

The LLAMAS language, syntax and semantics.

Software Modeling and Verification Department of Computer Science University of Geneva Battelle Bat. A Route de Drize 7 CH-1227 Carouge Switzerland

Abstract The Llamas Language for Advanced Modular Algebraic Systems (LLAMAS) is a modular Petri nets formalism that was defined to serve as a semantic platform to define modular extensions of Petri nets. Its objective is to be expressive enough to gather even the most complex modular features from the modular formalisms in the literature. This document gives the formal definition of the LLAMAS language. While this document is self contained, some prior knowledge of the basic features of the language is useful to understand the complex definitions we give here. Keywords: LLAMAS, Petri Nets, Modularity, Formal definition, Syntax, Semantics

Contents 1

Introduction

2

Running example 2.1 Internal behavior of a module - Petri net . . . . . . . . 2.2 Compositions . . . . . . . . . . . . . . . . . . . . . . 2.3 Interface - basic LLAMAS module . . . . . . . . . . . 2.4 Hierarchy and static instantiation . . . . . . . . . . . . 2.5 Dynamic instantiation - the nets within nets mechanism

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

. . . . .

1 2 2 2 4 5

Data types 3.1 Syntax . . . . . . . . . . . . . 3.1.1 Basic notations . . . . 3.1.2 Typing : S -sorted sets 3.1.3 Signature . . . . . . . 3.1.4 Terms . . . . . . . . . 3.1.5 Substitutions . . . . . 3.2 Semantics . . . . . . . . . . . 3.3 Nets Within Nets signature . .

3

4

5

1

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

6 6 6 7 9 10 11 12 14

The LLAMAS language - syntax 4.1 Petri nets . . . . . . . . . . . . . . . . . . . . . . 4.1.1 Multisets . . . . . . . . . . . . . . . . . . 4.1.2 Guards . . . . . . . . . . . . . . . . . . . 4.1.3 Place markings . . . . . . . . . . . . . . . 4.1.4 Transitions . . . . . . . . . . . . . . . . . 4.1.5 Parametric Activatable Algebraic Petri Nets 4.2 Encapsulation : interface . . . . . . . . . . . . . . 4.3 Hierarchy and static instantiation . . . . . . . . . . 4.4 LLAMAS class . . . . . . . . . . . . . . . . . . . 4.5 The LLAMAS Composition Mechanism . . . . . . 4.5.1 Composition participants . . . . . . . . . . 4.5.2 Compositions . . . . . . . . . . . . . . . . 4.5.3 Interface delegation . . . . . . . . . . . . . 4.6 LLAMAS specification . . . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

. . . . . . . . . . . . . .

17 17 17 18 19 19 20 21 22 24 26 26 29 30 32

The LLAMAS language - semantics 5.1 A note on the inference rules . . . . . . 5.2 LLAMAS model . . . . . . . . . . . . 5.3 Evaluation of guards . . . . . . . . . . 5.4 Operations on place markings . . . . . 5.5 States of a LLAMAS : global markings 5.6 Events in a LLAMAS model . . . . . . 5.7 Pre and Post conditions : event effects . 5.8 Computing event effects . . . . . . . . 5.9 Computing the effects of compositions . 5.10 Instantiation . . . . . . . . . . . . . . . 5.11 Events firing and garbage collection . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

33 34 34 35 36 37 39 40 40 45 48 54

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . .

. . . . . . . . . . .

. . . . . . . . . . .

6

5.12 The transition relation of a LLAMAS model . . . . . . . . . . . . . . . . . . . . . . . .

55

Conclusion

56

A Meaning of mathematical symbols

57

1. INTRODUCTION

1

1/58

Introduction

Through the years the original version of Petri nets has been extended to integrate a wide range of notions such as colors (tokens identity), time, probabilities, and modularity. Modularity is the ability to define complex systems by assembling smaller entities. We presented in [MB12] a survey about the mechanisms that were defined in the literature to integrate this notion to the Petri nets formalism. This survey reflected that these mechanisms were extremely variable, and their definitions are very different. Two main approaches have been followed by their authors to define the semantics (i.e., the possible executions) of these mechanisms. Many authors define a translation from their modular formalisms to "flat" (non-modular) Petri nets. In some cases (e.g., [DKR03]) this translation is very complex and difficult to understand. In some other cases (e.g., [BBG01, Lak01]), such translation is simply not attempted as it would be too complex or yield Petri nets with infinite places or transitions. In this case, the semantics of the formalisms is usually defined as compositions of the transition relations of individual modules. This is a low-level and usually very complex operation. To overcome this difficulty and give a unified approach for defining modular extensions of Petri nets, we propose a new modular formalism called the Llamas Language for Advanced Modular Algebraic Systems (LLAMAS). The objective of LLAMAS is to be expressive enough to be able to define translations from most if not all the modular extensions of Petri nets to LLAMAS in order to define their semantics. For this, the expressivity of LLAMAS must be enough to handle the huge array of modular mechanisms defined in the Petri nets literature. Our proposition is strictly limited to the definitions of modularity in the Petri nets formalisms. In particular, we do not consider the problem of the kind of data types used in the formalism. Indeed, there are many variants of the so-called High Level Petri Net (HLPN), that is, Petri nets variants that use complex data types. In LLAMAS, we are not interested in the definitions of this data types, and thus we chose one particular data types definition: Algebraic Data Types (ADTs). ADTs are a general specification formalism that is already used in the ISO-IEC 15909 standard. In this document, we consider a simplified definition of ADTs. This document gives the formal definition of the LLAMAS language, both syntax and semantics. It explores thoroughly all the formal details of LLAMAS, and thus reading it without a prior knowledge of the language may be a daunting task. As mentioned previously, we intend LLAMAS to be expressive enough to handle the semantics of the most complex modular formalisms in the literature. This means that LLAMAS is very complex itself. This document is organized as follows. In Sec. 2 we give an running example of the LLAMAS formalism, in order to provide an informal introduction to the formalism. The next section, Sec. 3, gives a formal definition of our simplified version of ADTs. An informed reader will remark that the definition of the semantics of the data types has been reduced to a strict minimum. The next two sections dive into the definitions of LLAMAS language itself, Sec. 4 for the syntax and Sec. 5 for the semantics. All these definitions use many complex mathematical symbols. For pratical purposes, we list most of these symbols in Sec. A. Finally, we conclude in Sec. 6.

2

Running example

In this section we will describe an example of a LLAMAS model representing a clock. This example will be used in the next sections to describe the formal syntax and semantics of the LLAMAS language. Notice that, even though this section is mainly self-contained, a basic introduction of the language is out of the scope of this document. Many features presented in this example will be explained later, along with their formal definitions.

2. RUNNING EXAMPLE

2.1

2/58

Internal behavior of a module - Petri net

We will begin the description of our example with the Petri net from Fig. 1. Together with the compositions we will give in the next section, this Petri net will represent a bounded counter. It has two places named Bound and Counter. The initial value of the token in place Bound is a variable, and thus its actual value will be determined at instantiation (see Sec. 2.4). There are also three transitions named GetBound, Reset, and Inc. All these transitions are passive. Notice that, if it was an active transition, an execution of GetBound would remove the token from place Bound. We will see in the next section that this behavior will be restrained by the compositions. All three transitions have one parameter that unifies itself with the value taken from the respective place.

2.2

Compositions

Fig. 2 shows four compositions that have been added to the example in Fig. 1. The composition in the center is called ReadBound. It uses the observer read, whose symbol is , and it binds the transition GetBound . The read operator indicates that when the composition ReadBound is executed, it checks if transition GetBound can be executed and it unifies the variable $b with the value taken from place Bound, without any modification to the marking of the net. Composition ReadBound binds GetBound, which means that GetBound cannot participate in any other composition. Thus, even though an execution of ReadBound removes the token from place Bound, we ensured by means of the composition ReadBound that this token will never actually be removed. The second composition, called Reset, binds the transition Reset, and calls the composition ReadBound, and uses the merge operator. When it is executed, both composition ReadBound and transition Reset will be executed simultaneously, as long as the guard of the composition ($c = $b) is evaluated to true. Thus, the composition Reset checks if the counter has reached its bound and resets it to 0. Composition Inc works in a similar way. It increases the value of the counter if it has not reached the value of the bound. The final composition, Tick, binds both compositions Reset and Inc with the operator any. Whenever Tick is executed, one composition between Reset and Inc is also executed, but not both. If neither Reset nor Inc are enabled, neither is Tick. All these compositions are passive and thus, for now, we still did not define a single executable event in our example.

2.3

Interface - basic LLAMAS module

The notion of encapsulation is central in most modular formalisms. It implies the existence of some elements in a module that are available to other modules (the interface), and some elements that are internal to the module. Some modular Petri nets formalisms define some places and/or transitions as the interface of modules. Other formalisms define entirely new elements to define the interface. The LLAMAS Composition Mechanism (LCM) requires that we adopt the latter case. Indeed, following the definition of the compositions in the LCM, we interface elements that allow us to carry calls and bindings across modules. Moreover, as the compositions are directed, we need to distinguish between input elements and output elements (we respectively call them services and requests). Thus, we have $b GetBound($b)

{$i} Bound $c + 1

0 {0} $c Reset($c)

Counter

$c

Inc($c)

Figure 1: Petri net example.

2. RUNNING EXAMPLE

3/58

Reset $c = $b

∨

Tick

Inc $c < $b

∧

∧

ReadBound($b) $b

{$i}

GetBound($b)

Bound $c + 1

0 {0} $c Reset($c)

Counter

$c

Inc($c)

Figure 2: Compositions example. s1 c1

t1

∧

s2 t2 r1

t3 r2 t4

∧ c2

Figure 3: Interface. four kinds of elements in our module interfaces: binding and non-binding services and binding and nonbinding requests. Fig. 3 illustrates the four possible combinations. It shows two transitions and one composition (resp. t1, t2 and c2) inside a module and two transitions and one composition (resp. t3, t4 and c1) outside the module. The interface of the module contains a binding and a non-binding service (resp. s1 and s2), represented by triangles directed towards the interior of the module. It also contains a binding and a non-binding request (resp. r2 and r1), represented by triangles directed towards the environment. c1 binds t1 by means of s1, and thus t1 is not available to other compositions, including compositions inside the module. c1 also calls t2 (by means of s2) and t3. Similarly, c2 binds t4 and calls t3 and t2. The distinction between input and output interface elements can be found in many formalisms, see for instance the import/export interfaces from [KP09], or the distinction between sockets and ports in [HJS91]. Services and requests in a LLAMAS interface are parametric, similarly to the transitions and compositions. Fig. 4 shows an interface added to the example from Fig. 2. Together, a Petri net, a set of compositions, and an interface form a basic (non-hierarchical) LLAMAS module. The module from Fig. 4 is called BCounter, and it takes one parameter $i that sets the initial value of place Bound. The interface of BCounter is composed of a non-binding service called Tick and a non-binding request called Overflow. Service Tick calls composition Tick, thus making this composition available to the environment. The composition Reset now calls the request Overflow, apart from calling ReadBound and binding transition Reset. This means that whenever there is an overflow, not only the counter will be reseted, but a notification will be sent to the container of BCounter (see the next section). If the environment is not able to respond to this request, the composition Reset will fail. The next section will introduce the hierarchical models in LLAMAS, and we will see how to use some instances of BCounter to model a clock.

2. RUNNING EXAMPLE

4/58

Overflow

BCounter($i)

Tick ∨

Reset $c = $b

Tick

Inc $c < $b

∧

∧

ReadBound($b) $b

{$i}

GetBound($b)

Bound $c + 1

0 {0} $c Reset($c)

Counter

$c

Inc($c)

Figure 4: A LLAMAS module.

2.4

Hierarchy and static instantiation

Another important feature of modular formalisms is hierarchy. In hierarchical Petri nets a module (called the container) may encapsulate other modules (called submodules), which in turn may encapsulate their own submodules. The hierarchy is a partial order relation between the modules in a system. Each container defines how its submodules communicate, both between themselves and with the container. A hierarchical LLAMAS module is thus composed of a Petri net, an interface, a set of submodules and a set of compositions. The hierarchical mechanism we use in LLAMAS was inspired by Modular PNML [KP09]. In Modular PNML, each module defines a set of submodule sockets, and each submodule socket is denoted only by an interface, which defines the synchronization contract between the container and the submodule. Let us mention one last important feature of LLAMAS: instantiation. An instantiation mechanism facilitates the definition of various identical (or similar) modules. It means that the modules in a system are copies of an initial definition, a blueprint. These copies may be fine tuned when they are created. Following the vocabulary of object-oriented languages, we call this blueprint a class, and its copies instances of the class. The instantiation may be static, i.e., performed once during the initial definition of the system, or dynamic, i.e., instances may be created during the execution of the system. Fig. 5 shows a hierarchical module that defines three static instances of the module BCounter from Fig. 4. The hierarchical module Clock contains three submodules sockets, all of them have the same interface as BCounter. This hierarchical module represents a clock. The first submodule on the left (the hours) has a bound of 23, and the two others (minutes and second respectively) have a bound of 59. The module Clock defines a composition called Second, which is active. It is the first and only active event we encounter in the whole example (remember that all the transitions and compositions in BCounter were passive). Each time Second is executed, it calls the service Tick from the rightmost submodule (the Clock

Second ∧

IncDays

$c + 1

$c

Days 0

Overflow

Tick

Overflow

Tick

Overflow

Tick

BCounter(23)

BCounter(59)

BCounter(59)

Hours

Minutes

Seconds

Figure 5: A hierarchical LLAMAS module representing a clock.

2. RUNNING EXAMPLE

5/58

seconds). Whenever this submodoule has an overflow (i.e., when 60 seconds have passed), it calls the service Tick from the module in the center, by means of its Overflow request. Similary, whenever there is an overflow on the center module (60 minutes), the service Tick from the leftmost submodule is called. Finally, whenever this submodule calls its own request Overflow (24 hours), the transition IncDays is called, which is increases the counter in a place called Days. This counter is unbounded, and the module Clock has clearly an infinite number of reachable states. If we remove the place Days but keep the transition IncDays, the module will have 24 × 60 × 60 = 86400 reachable states, without any deadlock (executing Second from the last state would reset the whole system). If we also remove the transition IncDays, the request Overflow from the leftmost submodule will not be executable, and this submodule would be blocked when its counter would reach the value 23. The whole system would then have the same 86400 states, but the last one, with marking h23, 59, 59i, would be a deadlock.

2.5

Dynamic instantiation - the nets within nets mechanism

While static instantiation consists in creating instances during the initial declaration of the system, dynamic instantiation consists in creating instances during its execution. Traditionally, dynamic instantiation has been simulated with colored tokens, where a particular token in a particular place represents the identity of a module on a given state. This low-level approach has the disadvantage of mixing the data types, the process steps and the identity of the dynamic modules. This has three main drawbacks. First, the models are conceptually far away from the real system, which hinders the modeling activity. Second, the models may become cluttered if the models have complex instantiations, (i.e., a module that creates other modules that create other modules and so on). In this case, the complexity of the system is drowned in the definitions of the data types. Finally, the ability to identify the individual modules at runtime is lost. This is an important information that may be used to make more efficient computations Notice that these three problems are very similar to the motivations that lead to the definition of High Level Petri nets from the original low-level Petri nets. Many formalisms define specific mechanisms to handle dynamic instantiation. Most of them (e.g., [BBG01, Lak01]) use the Nets Within Nets paradigm [Val04]. Simply put, in the Nets Within Nets (NWN) approach, the tokens in the Petri nets places may represent entire modules, and thus creating one of these tokens means creating a new module. Most formalisms use a reference-based implementation of the NWN paradigm. This means that multiple references to a single module may be present in two different places from two different modules. In LLAMAS, we defined a standard reference-based NWN mechanism, where instances of each module can be created at runtime by means of a special operator, called new class(params), where class is the name of the class to be instantiated and params is the list of parameters. The use of the NWN paradigm in LLAMAS is illustrated in Fig. 6, where we dynamically create instances of our bounded counter from Fig. 4. We use a graphical notation inspired by the Object Petri nets [Lak01, Lak95] for the NWN compositions. The initial marking of the net in Fig. 6 has one black token • in place p1. Transition t1 removes this black token and adds a reference to a new instance of BCounter to place p2. Transition t2 then copies this reference to places p3 and p4. At this point, both p3 and p4 have a reference to the same module. Composition c1 calls transition t3, which takes the reference from p3 and unifies it with variable $c. At the same time, c1 calls the service Tick from the module referenced by $c. Composition c2 does exactly the same with the reference contained in p4. There is only one instance of BCounter in the entire system, and thus both c1 and c2 do exactly the same thing, they both increment the counter of the same module, even if the reference they use is taken from a different place.

3. DATA TYPES

6/58

new

BCounter(5)

p2

t1

• $c •

t2

p1

$c $c p3

p4

$c

$c $c

$c

t3

t4 c1

Tick

c2

∧

∧

Tick

$c $c Figure 6: A nets within nets example.

3

Data types

The objective of LLAMAS is to provide a single platform for most if not all modular Petri net variants. Among these variants, many belong the the category os the so-called HLPNs, that is, Petri nets that use complex data types as tokens. The data types defined in the Petri nets literature is extremely variable, and defining a standard for them is a complex task, which is out of the scope of the LLAMAS formalism. Nevertheless, many modular formalisms include the notion of sharing values between modules and thus, to represent them, LLAMAS itself must be an HLPN formalism. To define the data types in LLAMAS, we chose the formalism of ADTs [AKKB99]. Instead of giving a complete definition of the ADTs, such as the one in [Hos12], we will limit ourselves to a simplified definition.

3.1

Syntax

3.1.1

Basic notations

Definition 3.1: Basic notations For any natural numbers a, b ∈ N such that a < b, we note [a..b] the integer interval between a and b: [a..b] = {c ∈ N s.t. a ≤ c ≤ b}. S 1 × S 2 is the cartesian product (i.e., set of pairs) of S 1 and S 2: S 1 × S 2 = {(s1, s2) where s1 ∈ S 1 and s2 ∈ S 2}. Furthermore, we note S ∗ = S ∪ S ∪ S × S ∪ . . . the set of all lists in S where S is the empty list. A relation from S to S 0 is a set of pairs of elements from S and S 0 : Rel ⊆ S ×S 0 . A function from S to S 0 is a left-injective left-total relation, that is, a relation F ⊆ S × S 0 where ∀s ∈ S , ∃!s0 ∈ S 0 s.t. (s, s0 ) ∈ F. For each function F from S to S 0 , we note F(s) = s0 if (s, s0 ) ∈ F. We us the notation F : S 1 → S 2 to indicate that F is a function from S 1 to S 2. For each function F : S 1 → S 2 and each set S 10 ⊆ S 1, we note F|S 10 : S 10 → S 2 the restriction of F to S 10 , that is, the function such that ∀s ∈ S 10 , F|S 10 (s) = F(s). A partial order in a set S is a reflexive, anti-symmetric and transitive relation from S to itself. We use the symbol ≤ for partial relations, and we write s ≤ s0 if (s, s0 ) ∈ ≤. We define the reflexivity,

3. DATA TYPES

7/58

anti-symmetry and transitivitiy as follows: • ∀s ∈ S , s ≤ s (reflexivity) • ∀s, s0 ∈ S , s ≤ s0 ∧ s0 ≤ s ⇒ s = s0 (anti-symmetry) • ∀s, s0 , s00 ∈ S , s ≤ s0 ∧ s0 ≤ s00 ⇒ s ≤ s00 (transitivity) For each partially ordered set hS , ≤i, we extend the partial order ≤ to lists in S ∗ as follows: ∀l1 = (x1 , . . . , xn ), l2 = (y1 , . . . , ym ) ∈ S ∗ , we have l1 ≤ l2 if and only if: • n=m • ∀i ∈ [1..n], xi ≤ yi 3.1.2

Typing : S -sorted sets

Typing is a syntactical mechanism used in most programming languages. Pierce defined a type system as "a tractable syntactic framework for classifying phrases according to the kinds of values they compute"[Pie02]. In other words, every expression in a system is assigned a tag, called type. Defining a type system allows to perform syntactic checks on the expressions of a program (or, in our case, the expressions in a Petri net), thus catching many errors prior to execution. In the context of ADTs, the typing mechanism is called sorting, and it is defined through the notion of S-sorted sets defined in Def. 3.2. Definition 3.2: S-sorted set Let S be a set, called a set of sorts. An S -sorted set X is a family of sets X = {X s } s∈S . A disjoint sorted set is an S -sorted set {X s } s∈S where: ∀s, s0 ∈ S , s , s0 ⇒ X s ∩ X s0 = ∅ [ For an S -sorted set X, we note carrier(X) = ( X s ) the carrier set of X. With a slight abuse of s∈S

notation, we will sometimes use X instead of carrier(X). For instance, we note x ∈ X iff x ∈ carrier(X). Similarly, unless specified otherwise, a function between two S -sorted sets is in fact a function between their carrier sets. The union and intersection of an S 1-sorted sets X and an S 2-sorted set Y are S 1∪S 2-sorted sets defined as follows: X ∪ Y = {X s ∪ Y s } s∈S 1∩S 2 ∪ {X s } s∈S 1\S 2 ∪ {Y s } s∈S 2\S 1 X ∩ Y = {X s ∩ Y s } s∈S 1∩S 2 Naturally, both the union and the intersection of two S -sorted sets are also S -sorted sets. We note X ∗ the S ∗ -sorted set of lists of X. It is the least S ∗ -sorted set such that: ∀(s1 , . . . , sn ) ∈ S \{S }, (X ) s1 ,...,sn ∗

where X ∗ is the empty list of X.

∗

(X ∗ )S = {X ∗ } = {(x1 , . . . xn ) ∈ carrier(X)∗ s.t.∀i ∈ [1..n], xi ∈ X si }

3. DATA TYPES

8/58

Example 3.3 gives an example of S -sorted set.

Example 3.3: S-sorted set Let us consider the set {true, f alse, 0, 1, 2}. We may wish to identify which elements are booleans, and which are natural numbers. For this, we define a set with two sorts, S = {bool, nat}, and we build the following S -sorted set: X = {{true, f alse}bool , {0, 1, 2}nat } Notice that X is a disjoint S -sorted set, as no element belongs to Xbool ∩ Xnat . We have for instance: (true, 1, 1, f alse) ∈ (X ∗ )bool,nat,nat,bool The definition of S -sorted sets will allow us to define typing in our data types definition. In simple typed systems, each expression has one type, but in richer definitions, some expressions may have more than one type. For instance, in most mathematical definitions, the number 0 is at the same time a natural number and an integer. In our data types definitions, we will define order-sorted systems. In such systems, the types are ordered. For instance, as the set of natural numbers N is included in the set of integers Z, we can define an ordering such that N ≤ Z. To define this, we rely on the notion of order-sorted sets, defined in Def. 3.4. Definition 3.4: Order-sorted set . Let S be a set and ≤ be a partial order in S . An S -sorted set X is an order-sorted set if and only if ∀s, s0 ∈ S , we have X s ⊆ X s0 .

Example 3.5 gives a simple example of order-sorted set. Example 3.5: Order-sorted set Let us consider the set {true, f alse, 0, 1, 2}, the set of sorts S = {bool, nat, nil, pos}, the h that pos ≤ nat and nil ≤ nat. Let X be the S -sorted set defined as follows: X = {{true, f alse}bool , {0, 1, 2}nat , {0}nil , {1, 2} pos } X is an order-sorted set, as X pos ⊆ Xnat and Xnil ⊆ Xnat . In Def. 3.4 we defined ≤ as an ordering in S , and we showed how ≤ is extended to an ordering between the families X s that compose an S -sorted set X. We will now extend this ordering to order the S -sorted sets themselves. This non-trivial notion will be useful later, when we will define compatibilities between interfaces (see Def. 4.13). Definition 3.6: S-sorted sets ordering Let S be a set and ≤ a partial order in S . Let X1 and X2 be two S -sorted sets. We say that X1 is compatible with X2 , noted X1 ≤ X2 , if an only if: ∀x ∈ carrier(X1 ), ∃s, s0 ∈ S such that s ≤ s0 ∧ x ∈ (X1 ) s ∧ x ∈ (X2 ) s

3. DATA TYPES

9/58

Note that this definition requires that carrier(X1 ) ⊆ carrier(X2 ). Roughly stated, an S -sorted set X1 is compatible with an S -sorted set X2 if X2 is "more general" than X1 . A bit more precisely, X2 contains all the elements of X1 , and that the elements, and the sorts of the elements in X1 are smaller than the sorts of the same elements in X2 . While the intention of such definition may be obscure at this point, it will become useful in the context of interfaces compatibility (see Def. 4.13). For now, let us give an example in Example 3.7. Example 3.7: S-sorted sets ordering Let us consider the set S = {nat, nil, pos} and an ordering ≤ such that nil ≤ nat and pos ≤ nat. Let us consider the S -sorted X1 = {{0}nil , {1, 2} pos , {3}nat } and the S -sorted set X2 = {{1, 3} pos , {0, 2, 4}nat }. We have X1 ≤ X2 because: • 0 ∈ (X1 )nil and 0 ∈ (X2 )nat with nil ≤ nat • 1 ∈ (X1 ) pos and 1 ∈ (X2 ) pos with pos ≤ pos • 2 ∈ (X1 ) pos and 2 ∈ (X2 )nat with pos ≤ nat • 3 ∈ (X1 )nat and 3 ∈ (X2 )nat with nat ≤ nat All the elements in X1 appear in X2 with "bigger" sorts. 3.1.3

Signature

In the simplest terms, a data type consists in a set of values and a set of operations that work on these values. A general notation for the values and the application of the operations on these values is the syntactical notion of expressions, or terms. The general form of a term will be either op where op is a constant, or op(sub1 , ..., subn ), where op is an operation, and sub1 , ..., subn are called arguments or subterms. We consider constant to be a special kind of operations without arguments. Usually, we want to restrict which terms can be used with each operator. For instance, if we define an addition operator +, we may wish to define it only for the natural numbers. To do this, we leverage the typing mechanism we defined in the previous paragraph and we define a profile for each operator. This profile indicates the sorts of the arguments that are allowed, and a return sort. For instance, if we consider the S-sorted set from Example 3.3, we may wish to define an addition operator, +, which takes two natural numbers and returns another natural number. In this case, the profile of + is noted + : nat, nat− > nat. Thus, to define the profile of each operator, we associate him a (possibly empty) list of sorts to define its arguments, and another sort to define its return type. This is reflected in Def. 3.8, where we define the signature of an ADT. Definition 3.8: Algebraic signature A signature, noted Σ, is a tuple hS , ≤, Opi where: • S is a finite set of sorts, • ≤ is a partial order in S , • Op is a disjoint S ∗ × S -sorted set of operations. Usually, a signature Σ = hS , ≤, Opi is accompanied by an S -sorted set of variables X such that S , Op and X are pairwise disjoint.

3. DATA TYPES

10/58

Note that in Def. 3.8 we restricted the set of operations so that no operation can have multiple profiles. This is not the usual case in the literature, and it restricts the expressivity of our data types, as we do not have general polymorphism on the operators. Nevertheless, the definitions become more simple as we do not need complex notions such as pre-regular an regular signatures, as defined in [Hos12]. We will see in Def. 3.10 that we simulated some kind of polymorphism in the terms themselves, by allowing the terms to belong to multiple sorts if they respect the order sorting defined by ≤. Example 3.9 gives an example of signature. Example 3.9: Algebraic signature An example of signature is the pair hS , ≤, Opi, where: • S = {bool, nat, nil, pos} • ≤= {(nil, nat), (pos, nat)} (we note nil ≤ nat and pos ≤ nat) • Op = {{true, f alse}bool , {0}nil , {1, 2, ..., 99} pos , {>}nat,nat,bool , {+}nat,nat,nat , {/}nat,pos,nat } where we represented the 100 first natural numbers in N, the addition + and the division /. Notice that Op is a disjoint S -sorted set. We will see later that 0 actually belongs to the natural numbers because nil ≤ nat. The distinction between zero (nil) and the positive naturals (pos) allows us to safely define the division operation /. Let us also consider the S -sorted set of variables X = {{x, y}nat , {b}bool }, which will be used in the next examples. 3.1.4

Terms

Having defined a set of values and a set of operations, we can now define the terms (i.e., expressions) we will use in our models. These terms are built upon the values and operations of a signature, and a disjoint S -sorted set of variables. The terms built using the operations of a signature may contain subterms, that must follow the pattern of the operation. More details are to be found in Def. 3.10. Definition 3.10: Terms of a signature upon a set of variables Let Σ = hS , ≤, Opi be a signature and X a disjoint S -sorted set of variables. The set of terms of Σ upon X, noted T (Σ, X), is the least S -sorted set inductively defined by: • ∀s ∈ S , ∀var ∈ X s , we have var ∈ T (Σ, X) s • ∀(s1 , ..., sn , s) ∈ S ∗ × S , ∀op ∈ Op s1 ,...,sn ,s , ∀(t1 , ..., tn ) ∈ (T (Σ, X) s1 × . . . × T (Σ, X) sn ), we have op(t1 , ..., tn ) ∈ T (Σ, X) s • ∀s, s0 ∈ S s.t. s ≤ s0 , we have T (Σ, X) s ⊆ T (Σ, X) s0 The last condition means that hT (Σ, X), ≤i is an order-sorted set. Thus, even if the set of operators Op is a disjoint S -sorted set, T (Σ, X) is generally not. The set T (Σ, ∅), consisting in the terms with no variables, is called the set of closed terms of a signature. Note that for any sets of variables X and X 0 such that X ⊆ X 0 we have T (Σ, X) ⊆ T (Σ, X 0 ). In particular, for any set of variables X, we have T (Σ, ∅) ⊆ T (Σ, X).

3. DATA TYPES

11/58

With this definition, we see that we allow some kind of restricted but safe polymorphism on our operators. Example 3.11 shows some examples of terms. In that example, we see that the operator 0, that was of sort pos in Example 3.9, is a term that belongs both to sorts pos and sorts nat. Thus, we do not allow to have polymorphism on the operators, but the terms themselves can belong to multiple sorts if they respect the order sorting ≤ defined by the signature. Example 3.11: Terms of a signature upon a set of variables Let us consider the signature Σ and the variables X from Example 3.9. The set of terms of Σ upon X is the S -sorted set T (Σ, X) = {T (Σ, X)bool , T (Σ, X)nat , T (Σ, X)nil , T (Σ, X) pos }. This set is infinite, and it contains the following terms: • true ∈ T ermsbool • $b ∈ T (Σ, X)bool • T (Σ, X)nil = {0}, and thus {0} ⊂ T (Σ, X)nat • T (Σ, X) pos = {1, . . . , 99}, and thus {1, . . . , 99} ⊂ T (Σ, X)nat • 0/3 ∈ T (Σ, X)nat , but 0/0 < T (Σ, X)nat , as the operator / takes a positive number as second parameter • 0 + (0 + 1) ∈ T (Σ, X)nat but 0 + (0 + 1) < T (Σ, X) pos . This is an unfortunate result of disallowing polymorphism. • (1 + $y) + ($x + 1) ∈ T (Σ, X)nat • ((1 + $y) + ($x + 1)) > (0 + 1) ∈ T (Σ, X)bool A dollar sign $ is used to distinguish the variables from the operations in terms. Parenthesis are used to denote the operators precedence. Moreover, binary terms may be noted using an infix notation, e.g., 0 + 1 instead of +(0, 1). 3.1.5

Substitutions

The variables in the terms are meant to be used as placeholders to be replaced by other terms. This replacement is called the application of a substitution, and it is formally defined in Def. 3.12. Definition 3.12: Substitution and application of a substitution Let Σ = hS , ≤, Opi be a signature, X a disjoint S -sorted set of variables, and T (Σ, X) the set of terms of Σ upon X. A substitution of X in Σ is a function σ : X → T (Σ, X) such that ∀s ∈ S , ∀x ∈ X s , σ(x) ∈ T (Σ, X) s . The application of a substitution σ : X → T (Σ, X) is a function applyσ : T (Σ, X) → T (Σ, X) defined as follows: • Variables: ∀var ∈ X, applyσ (var) = σ(var) • Constants: ∀s ∈ S , ∀op ∈ Op s , applyσ (op) = op • Other terms: ∀t = op(t1, ..., tn) ∈ T (Σ, X), applyσ (t) = op(applyσ (t1), ..., applyσ (tn)) In this document, we will naturally extend the application of a substitution to different structures that will contain terms. For instance, we define the application of a substitution in the lists of terms as

3. DATA TYPES

12/58

follows: ∀list = (t1, ..., tn) ∈ T (Σ, X)∗ , applyσ (list) = (applyσ (t1), ..., applyσ (tn)) We note subst(Σ, X) the set of all possible substitutions of X in Σ. The elements of subst(Σ, X) that only return closed terms are called closed substitutions. This set is noted subst_cl(Σ, X), defined as follows: subst_cl(Σ, X) ⊆ subst(Σ, X) and σ ∈ subst_cl(Σ, X) ⇔ ∀x ∈ X, σ(x) ∈ T (Σ, ∅) Note that the application of any substitution is the identity function on the closed terms of a signature: ∀sigma ∈ subst(Σ, X), ∀t ∈ T (Σ, ∅), applyσ (t) = t. Example 3.13: Substitution and application of a substitution Let us consider the signature Σ = hS , ≤, Opi from Example 3.9. An example of substitution of X in Σ is the function σ defined by: • σ($x) = 1 • σ($y) = 2 • σ($b) = f alse The application of σ to some terms from Example 3.11 gives the following results: • applyσ ($b) = σ($b) = f alse • applyσ (2) = 2 • applyσ (0 + 1) = applyσ (0) + applyσ (1) = 0 + 1 • applyσ ((1 + $y) + ($x + 1)) = applyσ (1 + $y)

3.2

+ applyσ ($x + 1)

= (applyσ (1) + applyσ ($y))

+ (applyσ ($x) + applyσ (1))

= (1 + σ($y))

+ (σ($x) + 1)

= (1 + 2)

+ (1 + 1)

Semantics

The semantics of ADTs have been discussed in many contexts in the literature (see for instance [HO80]), including inductive theories (e.g., [Aub79]), translation to Σ-algebras (e.g., [Rei91]) and rewriting [Ter03, DW91]. To simplify a bit the definitions of this document, we will give an extremely simplified definition of the semantics for our data types, without defining an application mechanism. We defined previously that a signature with a set of variables defines a set of terms, that is, a set of expressions. Some of these terms must be evaluated to compute a result, while some others do not need further evaluation. We call the latter normal terms. For instance, if we consider two terms 2 and 0 + 1, we say that the first one is a normal term, it is its own result (eval(2) = 2), while the second one is evaluated to another expression (eval(0 + 1) = 1). This evaluation is defined in Def. 3.14. Definition 3.14: Evaluation function Let Σ = hS , ≤, Opi be a signature, and T (Σ, ∅) the S -sorted set of closed terms of Σ. An evaluation function of Σ is a function eval : T (Σ, ∅) → T (Σ, ∅) such that: • The image of eval is its kernel, i.e., ∀t ∈ Norm, eval(eval(t)) = eval(t)

3. DATA TYPES

13/58

• eval preserves the sorts of the terms, i.e., ∀s ∈ S , ∀t ∈ T (Σ, ∅) s , we have eval(t) ∈ T (Σ, ∅) s • eval can be applied to the subterms of a complex term before being applied to the complete term: ∀s ∈ S , ∀(t1 , ..., tn ) ∈ T (Σ, ∅)∗ , ∀t = op(t1 , ..., tn ) ∈ T (Σ, ∅) s , ∀i ∈ [1..n], we have that eval(op(t1 , ..., ti , ..., tn )) = eval(op(t1 , ..., eval(ti ), ..., tn )). Given a closed substitution σ ∈ subst_cl(Σ, X), we can generalize any evaluation function eval to the whole set of terms of a signature upon a set of variables, by defining a function evalσ : T (Σ, X) → Norm such that: ∀t ∈ T erms, evalσ (t) = eval(applyσ (t)) Remember that any substitution is the identity function on the closed terms of a signature, and thus we have: ∀σ ∈ subst_cl(Σ, X), ∀t ∈ T (Σ, ∅), evalσ (t) = eval(t) For any closed term t ∈ T (Σ, ∅), we call eval(t) the normal form of t. Whenever a closed substitution σ has been specified, we may extend the notion of normal form to any term t0 ∈ T (Σ, X), by saying that evalσ (t0 ) is its normal form. Example 3.15 gives an example of an evaluation function. Example 3.15: Evaluation function Let us consider the signature from Example 3.9. If we define the following S -sorted set of terms Norm = {{true, f alse}bool , {0, 1, 2, ..., 99}nat } as the terms in normal form, it means that any evaluation function must preserve, among others, the following results: • eval(true) = true • eval( f alse) = f alse • eval(1) = 1 • eval(2) = 2 • ... We may define an evaluation function that follows the usual definitions in N bounded to 99 and B, i.e., a function eval where: • eval(0 > 1) = true • eval(99 + 1) = 0 • eval(0 + 1) = 1 • eval(0 + (0 + 1)) = 1 Notice that for any evaluation function eval, we have eval(0 + (0 + 1)) = eval(0 + eval(0 + 1)). Given the substitution from Example 3.13, we have: • evalσ ($b) = eval(applyσ ($b)) = eval(σ($b)) = f alse • evalσ (2) = 2

3. DATA TYPES

14/58

• evalσ (0 + 1) = eval(0 + 1) = 1 • evalσ ((1 + $y) + ($x + 1)) = evalσ (applyσ ((1 + $y)

+ $x + 1))

= evalσ (applyσ (1 + $y)

+ applyσ ($x + 1))

= evalσ ((applyσ (1) + applyσ ($y))

+ (applyσ ($x) + applyσ (1)))

= evalσ ((1 + σ($y))

+ (σ($x) + 1))

= evalσ ((1 + 2)

+ (1 + 1))

=5

3.3

Dynamic references

The survey in [MB12] showed that a wide range of Petri nets-based modular formalisms use the NWN paradigm [Val04] mechanism. This mechanism allows dynamic instantiation of modules, i.e., the creation (and usually destruction) of modules during the execution of a system. In reference-based implementations of the NWN paradigm (e.g., [BBG01, Lak01]), the tokens in the Petri nets places may be references to dynamically created modules. To handle such paradigm in LLAMAS, our data types definitions must be extended, to allow the following operations: Manipulation of the module references For safety reasons, the values of the references themselves must not be included in the syntactic definition of our models. Rather, the users have access to some variables that may contain module references. The value of these variables is meant to be computed at runtime. Creation of a module (instantiation) Most object-oriented formalisms include a special operator for the dynamic instantiation of modules (create in Concurrent Object-Oriented Petri Nets (COOPN)[BBG01] and [SB94], new in [Val04] and [MM01]). In LLAMAS we chose to use the keyword new for the creation of module instances. For each class with name name, we define an operator new name, whose arguments are determined by the parameters of the module (see Sec. 4.4 for more details). As for the destruction of modules, we use a garbage collection mechanism, as in most object-oriented Petri nets-based formalisms. Thus, we do not need to define a special operator for the destruction of dynamic modules. As a summary, we need to define a data types signature that will include a set of sorts, values and operations to create and manipulate modules. We call this kind of signature a NWN-signature, defined in Def. 3.16. Definition 3.16: Nets within nets signature Let ClassNames be a disjoint S ∗ -sorted set of class names where S is a set of sorts such that carrier(ClassNames) ⊆ S . Let ObjIds be a possibly infinite disjoint ClassNames-sorted set of object identifiers. Let us note S 0 = S \carrier(ClassNames) the set of "normal" sorts. A signature Σ = hS , ≤, Opi is a NWN-signature based on ClassNames and ObjIds if and only if: • ∀s ∈ S 0 , ∀cname ∈ ClassNames, (s, cname) < ≤ ∧ (cname, s) < ≤ • Op = Op0 ∪ Opinst ∪ ObjIds where: – Op0 is an S ∗ × S 0 -sorted set of operations (usual operations)

3. DATA TYPES

– Opinst =

15/58

[

[

{new cname}(s1,..,sn,cname) (module creation)

(s1,...,sn)∈S ∗ cname∈ClassNames s1,...,sn

– Op0 , OpInst and ObjIds are pairwise disjoint. The first condition indicates that the class names and the normal sorts cannot be compared with the operator ≤. The elements in S 0 and Op0 are simple data types elements similar to what has been defined in Def. 3.8. Notice that the operations in Op0 may have parameters from both S 0 and ClassNames, but their return type must be exclusively in S 0 . Thus, no operator in Op0 can create a module reference. The elements in Opinst are the instance creation operators. There is exactly one operator to create instances for each class name in ClassNames. The domain of the operator is what defines the parameters of the creation of the module. In Def. 3.16, we consider signatures that have some elements that were already defined in Def. 3.8 (informally called "normal" elements), and some elements specific to the NWN-paradigms. A naive approach to create this definition would have been to take the definition in Def. 3.8 and extend it, but this would not take into account the fact that the "normal" operations can be built by using the NWN-sorts. Indeed, notice that the set of "normal" operations Op0 defines operations that have a "normal" sort as return type but can take both "normal" and NWN sorts as parameters. An example will be presented later, in Example 3.18, with the operator pair. This operator is a "normal" operator, but it uses the NWN sorts of the signature. As in most object-oriented languages, we do not wish to make the values of the references themselves accessible in the definition of the syntax of the system. Rather, we will only manipulate these values at runtime. Because of this, we will define a restricted version of a signature to be used in the syntactic definition of the LLAMAS models. This restriction is defined in Def. 3.17. Definition 3.17: Restriction of a NWN-signature Let ClassNames be an S -sorted set of class names and Σ = hS , ≤, Opi a NWN-signature based on ClassNames and Ob jIds. The restriction of Σ, noted ~Σ = hS , ≤, ~Opi, is the signature Σ without the object identifiers: ~Op = Op\ ObjIds We will give two examples of NWN-signatures. The first one is a complete example that shows the possibility of using the class names as sorts, and it is presented in Example 3.18. The second one is the signature that was used to create the BCounter and Clock modules in Figure 4 and Figure 5 respectively. This signature is defined in Example 3.19. Example 3.18: Nets within nets signature We will build in this example a NWN-signature by extending the signature Σ and the variables X from Example 3.9. Let us consider a set two class names: ClassNames = {{module1}bool,bool , {module2}nat,module1 }} The instances of module1 take two booleans as parameters, and the instances of module2 take on natural number and one reference to some instance of module1. Let us also consider the following ClassNames-sorted set of object identifiers: Ob jIds = {{idi , i ∈ N}module1 , {id10 , id20 }module2 }

3. DATA TYPES

16/58

There are infinite object identifiers for module1, but only two object identifiers for module2. In our signature, we will consider a new sort, pair, that represents pairs of references (module1, module2). The signature Σ1 = hS 1 , ≤1 , Op1 i defined as follows is a NWN-signature based on ClassNames and Ob jIds: • S 1 = {bool, nat, pair, module1, module2} • ≤1 = {} • Op1 = Op0 ∪ Opmod ∪ Ob jIds where: – Op0 = {{true, f alse}bool , {0, 1, 2, ..., 100}nat , {>}(nat,nat,bool) , {+}(nat,nat,nat) , {pair}(module1,module2,pair) } – Opmod = {{new module1}(bool,bool,module1) , {new module2}(nat,module1,module2) } – ObjIds = {{idi , i ∈ N}module1 , {id10 , id20 }module2 } Some terms of this signature upon X are: • 1 + 99 (usual term) • new module1(true, true) (creation term of sort module1) • pair(id25 , new module2(0, id13 )) (a pair that contains a reference to a module1 with id id25 , and the creation of a module2, which itself references to a third module1 with id id13 ) The restriction of Σ is the signature ~Σ = hS 1 , ≤1 , ~Opi, where: • ~Op ={{true, f alse}bool , {0, 1, 2, ..., 100}nat , {>}(nat,nat,bool) , {+}(nat,nat,nat) , {pair}(module1,module2,pair) , {new module1}(bool,bool,module1) , {new module2}(nat,module1,module2) }

Example 3.19: Nets within nets signature from the model in Figure 5 Let us consider the set of sorts S = {nat, bool, BCounter, Clock}, the S ∗ -sorted set ClassNames = {{BCounter}nat , {Clock}S }, the S -sorted set of variables X = {{$c, $b, $i}nat } and the trivially ClassNames-sorted set ObjIds = ClassNames ×N. The signature Σ = hS , ≤, Opi is a NWN-signature based on ClassNames if: • Op = Op0 ∪ Opmod ∪ ObjIds q where: – Op0 = {{true, f alse}bool , {0, 1, 2, ..., 59}nat , {>}(nat,nat,bool) } – Opmod = {{new BCounter}(nat,BCounter) , {new Clock}(Clock) } – ObjIds = {hBCounter, 0i, hBCounter, 1i, ...}BCounter , {hClock, 0i, hClock, 1i, ...}Clock }

4. THE LLAMAS LANGUAGE - SYNTAX

17/58

An evaluation on a NWN-signature must preserve the identities of the object identifiers. This is reflected in Def. 3.20. Definition 3.20: Evaluation on a NWN-signature Let Σ be a NWN-signature based on ClassNames and ObjIds. Any evaluation eval on Σ must meet the following condition: ∀id ∈ ObjIds, eval(id) = id This means that all the object identifiers are already in their normal form.

4

The LLAMAS language - syntax

4.1

Petri nets

As has been stated previously, modularity is the ability of define complex systems by assembling smaller systems called modules. The behavior of the complete system depends on the behavior of each individual module. In LLAMAS, the behavior of the modules is represented with a particular version Algebraic Petri Nets (APNs)[Vau85, Rei91]. In order to use the Petri nets in a modular context, we made some modifications to the traditional definition of APN. Our version of APNs has three novel features that distinguish it from the usual definitions: • The transitions may be either passive and active. In usual Petri nets, each transition is an independent event, while in modular formalisms, the events may be defined as compositions of smaller events. Thus, it makes sense to be able to define some transitions that cannot be executed unless they are part of a more complex event. We call such transitions passive. This notion already defined in some variants of modular Petri nets (e.g., the hierarchical colored Petri nets [HJS91]). • Parametric transitions, to enable the transfer of values between transitions. Parametric transitions are defined in formalisms such as the M-nets [DKR03] and the colored Petri nets with channels [CH94]. • Global parameters of the Petri net, to tune the initial marking of the systems at instantiation. A similar feature has been defined for the M-nets [DKR03]. We call our version of APNs, enriched with these three features, Parametric Activatable Algebraic Petri Nets (P/A APNs). The definition of P/A APNs is given in Def. 4.7, preceded by the definition of the classic multisets, given in Def. 4.1, and the definition of guards in Def. 4.3. 4.1.1

Multisets

Multisets are the basic data type structure used in HLPNs. A multiset is basically a set-like structure where there may be more than one instance of each element. Many authors (e.g., [BBG01]) give an inductive algebraic definition of the multisets. We consider that our definition, given in Def. 4.1, is more straightforward. In this definition, each element of the multiset is associated with a natural number to indicate its cardinality, i.e, the number of instances of the element present in the multiset. Definition 4.1: Multiset Let Σ = hS , ≤, Opi be a signature and X a disjoint S -sorted set of variables. A multiset of Σ upon X is a function m : T (Σ, X) → N where the number of terms t such that m(t) > 0 is finite.


18/58

The set of all multisets of Σ upon X is noted mult(Σ, X). For any multiset m ∈ mult(Σ, X) and any term t ∈ T (Σ, X), the natural number m(t) is called the cardinality of t in m. The set of multisets where all the terms whose cardinality is not null are from the same sort s ∈ S is noted mult(Σ, X) s : ∀s ∈ S , mult(Σ, X) s = {m ∈ mult(Σ, X) s.t. ∀t ∈ T (Σ, X), mult(t) > 0 ⇒ t ∈ T erms s } Note that, with this definition, the set mult(Σ, X) is not an S -sorted set, as some multisets may contain terms with heterogeneous sorts. In other words, there are some multisets in mult(Σ, X) that do not belong to any set multi(Σ, X) s . In all the following definitions, we will never use any of these heterogeneous multisets.

Example 4.2: Multiset An example of multiset over the terms in Example 3.11 is given by the following function m1: • m1(true) = 3 • m1(2 + $x) = 4 • m1($y + 1) = 2 • ∀t ∈ T (Σ, X)\{true, (2 + $x), ($y + 1)}, m1(t) = 0 This multiset may be represented by the following notation: m1 = [30 true, 40 (2 + $x), 20 ($y + 1)] We will use this notation in the rest of this document. The empty multiset, i.e., the multiset where every term has a cardinality of 0, is noted []. A cardinality of 1 is usually omitted, i.e., [10 true, 10 f alse] is noted [true, f alse].

4.1.2

Guards

In Petri nets, as in any event-based formalism, the state of the system must meet certain conditions for each event to be executable. Traditionally, in Petri nets, each event is represented with a transition, and each transition defines a set of pre-conditions that define the situations in which the transition can be fired. In HLPN, the firing conditions are further refined by means of guards attached to the transitions. The syntax of the guards in P/A APN is defined in Def. 4.3. Definition 4.3: Guards Let Σ = hS , ≤, Opi be a signature and X a disjoint S -sorted set of variables. The set of guards of Σ upon X, noted guard(Σ, X), is inductively defined by: • true, false ∈ guard(Σ, X) (atomic guards) • ∀s ∈ S , ∀t, t0 ∈ T (Σ, X) s , t = t0 ∈ guard(Σ, X) (terms equality) • ∀s ∈ S , ∀t, t0 ∈ T (Σ, X) s , t , t0 ∈ guard(Σ, X) (terms difference) • ∀guard1, guard2 ∈ guard(Σ, X), guard1 ∧ guard2 ∈ guard(Σ, X) (conjunction)


19/58

• ∀guard1, guard2 ∈ guard(Σ, X), guard1 ∨ guard2 ∈ guard(Σ, X) (disjunction) Note that this definition corresponds to propositional logic where propositions are equalities and inequalities of terms, restricted to the conjunction and disjunction operators. Example 4.4: Guards Let T (Σ, X) be the set of terms in Example 3.11. The set of guards of T (Σ, X), noted guard(T (Σ, X)), contains the following expressions: • 0=0 • true , true • 1+1=2 • (1 + 1 = $x) ∧ (true = $b) We will see later that the first guard will always be evaluated to true, and the second to false. The result of the other two guards depends on a particular assignment and evaluation function. 4.1.3

Place markings

The P/A APNs, as most variants of Petri nets, are state transition formalisms. Each net defines a set of states meant to represent the states of a given system, and a transition relation between these states. The states of a P/A APN are represented by values inside a set of containers, called places. Formally, each state of a P/A APN is defined as a place marking, as in Def. 4.5. Definition 4.5: Place marking Let Σ = hS , ≤, Opi be a signature, X a disjoint S -sorted set of variables, and P a finite S -sorted set of places. A place marking of P is a function that associates a multiset of the adequate sort to each place: marking : P → mult(Σ, X), such that ∀s ∈ S , ∀p ∈ P s , marking(p) ∈ mult(Σ, X) s We note mark(Σ, X, P) the set of place markings of P on the terms T (Σ, X). Note that, similarly to Def. 3.10, for any S -sorted set of variables X, we have mark(Σ, ∅, P) ⊆ mark(Σ, X, P). The elements of mark(Σ, ∅, P) are called closed markings. We will give an example of place marking as part of the complete example of a P/A APN in Example 4.8. 4.1.4

Transitions

Loosely put, each event in an transition state system is represented as the passage from some state (the predecessor state) to some other state (the successor state). As seen previously, the states of our P/A APNs are defined as place markings. The events themselves are represented by transitions, formally defined in Def. 4.6. Definition 4.6: Transition axiom Let Σ = hS , ≤, Opi be a signature, X a disjoint S -sorted set of variables and P a finite S -sorted set of places. A transition axiom is a tuple hParam, guard, pre, posti where:


20/58

• Param = (x1 , . . . , xn ) ∈ X ∗ is a list of formal parameters of the transition • guard ∈ guard(Σ, X) is a guard • pre ∈ mark(Σ, X, P) is a preconditions marking • post ∈ mark(Σ, X, P) is a postconditions marking The domain of a transition axiom is the list of sorts of its parameters. Formally, for a transition axiom t = hParam, guard, pre, posti, where Param = (x1 , ..., xn ) and ∀i ∈ [1..n], xi ∈ X si , we note: domain(t) = (s1 , ..., sn ). Thus, any set of transitions T can be trivially represented as an S ∗ -sorted set, by indexing every transition t with domain(t). We will give examples of transition axioms as part of the complete example of a P/A APN in Example 4.8. 4.1.5

Parametric Activatable Algebraic Petri Nets

Definition 4.7: Parametric Activatable Algebraic Petri Net Let Σ = hS , ≤, Opi be a signature and X a disjoint S -sorted set of variables. A Parametric Activatable Algebraic Petri Net (P/A APN) is a tuple net = hP, T, Param, guard, M0 i, where: • P is a finite S -sorted set of named places. We note τ the function that computes the sort of a place: ∀p ∈ P s , τ(p) = s • T = T act ∪ T pass is a finite S ∗ -sorted set of transition axioms as defined in Def. 4.6, where T act ∩ T pass = ∅. T act is called the set of active transitions and T pass is called the set of passive transitions • M0 ∈ mark(Σ, X, P) is the initial marking of the net Notice that the markings may contain variables. We will see later that these variables will be bound when we will instantiate LLAMAS modules. We gave a small example of P/A APN in Figure 1 using a graphical notation. Example 4.8 gives the formal notation of that example1 . Example 4.8: Parametric Activatable Algebraic Petri Net This net defines a counter that stores two values, one for the current value of the counter in a place Counter, and another for the maximum value that the counter may reach in a place Bound. This maximum value is determined by a parameter of the net noted $i. The net also defines three transitions: • A transition called Inc to increment the value of the counter • A transition called Reset to reset the value to zero • A transition called GetBound to read the value of the bound 1

Note that not all the elements of the formal definition are represented in the graphical notation


21/58

The four transitions are passive transitions, which means that they will never be fired unless an external event triggers them. Formally, this P/A APN is built over the signature Σ from Example 3.9 and the set of variables X = {{$b, $c, $i}nat }. It is formally defined by the tuple net = hP, T, M0 i where: • P = {{Counter, Bound}nat } • T = T pass = {Inc, Reset, GetBound} where: –

Inc

=h($c), true,

(guard)

hCounter := [$c]i, hCounter := [$c + 1]ii –

Reset

(parameters) (pre-conditions) (post-conditions)

=h($c), true, hCounter := [$c]i, hCounter := [0]ii

–

GetBound

=h($b), true, hBound := [$b]i, hii

• M0 = hCounter := [0], Bound := [$i]i Notice that we used a compact notation for the place markings. The notation hCounter := [$c]i represents a function marking such that: • marking(Counter) = [$c] • marking(Bound) = [] Moreover, the notation hi stands for the markings where all the places are empty.

4.2

Encapsulation : interface

A key concept in modular formalisms is encapsulation, i.e., the possibility of restricting the elements of a module that are accessible by other modules and the elements that are internal to the module. Encapsulation is usually defined by means of interfaces. In LLAMAS, we define the communication between modules by means of directed service calls. Thus, an interface must define which services are offered by a given module to its environment, and which services it requires from the environment. Because of this, the interfaces are made up of two kinds of elements: services, to indicate that a component is willing to offer a service to its environment, and requests, to indicate that a component requests a service from its environment. Def. 4.9 gives the formal definition of a module interface, composed of four sets of interface elements. Both the services and the requests in an interface are parametric, and thus they have a profile as noted in Def. 4.9. The distinction between services and requests is part of the synchronization contract between LLAMAS components, that will be explicit in Sec. 4.5.


22/58

Definition 4.9: Module Interface Let Σ = hS , ≤, Opi be a signature and X a disjoint S -sorted set of variables. A LLAMAS module interface is a tuple Ξ = hServ, BServ, Req, BReqi where: • Serv is a disjoint S ∗ -sorted set of non-binding services • BServ is a disjoint S ∗ -sorted set of binding services • Req is a disjoint S ∗ -sorted set of non-binding requests • BReq is a disjoint S ∗ -sorted set of binding requests • The four disjoint S ∗ -sorted sets are pairwise disjoint The interface of the module BCounter from Figure 4 is formally defined in Example 4.10. Example 4.10: Module interface The interface of the module BCounter is quite simple. It has a non-binding service called Tick and a non-binding request. Neither defines any parameters, an thus, both will be indexed by the empty list. Formally, this interface is noted Ξ = h{Tick}S , ∅, {Overflow}S , ∅i.

4.3

Hierarchy and static instantiation

With the notion of interface defined in the previous paragraph comes the notion of encapsulation, i.e., the ability to differentiate the elements in a module that will participate in interactions with other modules from the elements that will not (the latter being called internal elements). A direct extension of encapsulation is the notion of hierarchy: the ability to create compound modules, that encapsulate entire modules, called submodules. A submodule may in turn be itself the container of some other sub-submodules, and so-on. The notion of hierarchy is very common in modular Petri nets formalisms. The mechanism to represent hierarchies in LLAMAS is called submodule sockets. It was partly inspired by the hierarchical mechanism from Modular PNML [KP09]. Similarly to Modular PNML, the submodule sockets define at the same time the hierarchy and the static instantiation in LLAMAS. Each submodule socket is a placeholder for a submodule. More precisely, each submodule socket is a communication interface between two modules, one of them called the container, and the other the submodule. The distinction between the submodule socket and the module it contains will be justified later, when we will describe the semantics of the instantiation mechanism. For now, let us say that each submodule socket is defined by an interface and a module creation term that is used to initialize the submodule itself. This is formally defined in Def. 4.11. Definition 4.11: Submodule socket Let Σ = hS , ≤, Opi be a NWN-signature based on ClassNames, where ClassNames is an S ∗ -sorted set of class names, and X a disjoint S -sorted set of variables. A submodule socket is a pair socket = hΞ, termi, where: • Ξ is an interface [ • term ∈

T (Σ, X)(s1 ,...,sn ,name) is a module creation term

name∈Names(s1 ,...,sn )

Following Def. 3.16, we have term = new module(t1 , ..., tn ), where module ∈ ClassNames is the name


23/58

of a class to instantiate and (t1 , . . . , tn ) is the list of effective parameters of the instantiation. More details about the instantiation of modules will be given later. The module from Figure 5 contains three submodule sockets that have the same interface. Two of them (minutes and seconds) have also the same module creation term. They third one is described by the submodule socket defined in Example 4.12. Example 4.12: Submodule socket The submodule socket Hours from Figure 5 is defined by the pair hΞ, termi where: • Ξ is an interface as defined in Example 4.10 (Ξ = h{Tick}S , ∅, {Overflow}S , ∅i) • term = new BCounter(23) Notice that the interface of the submodule socket in Example 4.12 is the same as the interface in Example 4.10. This is not always the case. The interface of the submodule socket defines a service, Tick, and a request, Overflow. This means that the module Clock requires the corresponding submodule to define a service Tick. The submodule itself could offer more services, and it would not be a problem. Similarly, Clock is ready to respond to a request Overflow from the submodule. The submodule does not necessarily use this request. In a nutshell, the set of services defined in the interface of a submodule socket must be included in the set of services in the interface of the associated module. Likewise, the set of requests in the interface of this module must be included in the set of requests in the interface the socket. This leads us to a definition of interface compatibility , given in Def. 4.13, which is covariant on the set of requests and contravariant on the set of services. Notice that our definition of compatibility takes into account the sub sorting in our data types definition. Definition 4.13: Interface compatibility Let Σ = hS , ≤, Opi be a signature and X a disjoint S -sorted set of variables. Let also Ξ1 = hServ1, BServ1, Req1, BReq1i and Ξ2 = hServ2, BServ2, Req2, BReq2i be two module interfaces as defined in Def. 4.9. Ξ1 is compatible with Ξ2 , noted Ξ1 ≤ Ξ2 if and only if: • Serv2 ≤ Serv1 • BindingServ2 ≤ BindingServ1 • Req1 ≤ Req2 • BindingReq1 ≤ BindingReq2 Here, ≤ is the ordering between S -sorted sets as defined in Def. 3.6. Remember that if Req1 ≤ Req2, then the elements in Req1 are included in Req2, and the sorts of the elements in Req2 are bigger than the sorts in Req1. If Ξ1 is compatible with Ξ2 , it means that the elements in Ξ1 are present in a module with interface Ξ1 may replace any module with interface Ξ2 (at least syntactically). An example of interface compatibility is to be found in Example 4.14. Example 4.14: Interface compatibility Let us consider the set S = {nat, nil, pos} and an ordering ≤ such that nil ≤ nat and pos ≤ nat. Consider also an interface Ξ1 that defines two non-binding service serv and serv0 that take no


24/58

parameter, and one binding request req that takes one natural and one positive parameter. Thus Ξ1 = h{serv, serv0 }S , ∅, ∅, {req}(nat,pos) i. Consider also an interface Ξ2 that defines a non-binding parameter serv and a binding request req that takes two natural numbers as parameters. Thus, Ξ2 = h{serv}S , ∅, ∅, {req}(nat,nat) i. We have that Ξ1 ≤ Ξ2 . Now, suppose that Ξ1 is the interface of a submodule, and Ξ2 is the interface in a submodule socket from the container. The submodule offer two services serv and serv0 , but the container only need one of these services, serv. Moreover, the submodule requires a service req from the container, and the container if willing to answer to this request. Notice that the sorts of req in the submodule are more specific than the sorts of req in the container. Example 4.14 features two interfaces whose graphical representation is given in Figure 7. In this figure, the inner interface is the interface Ξ1 and the outer interface is Ξ2 from Example 4.14. Notice that the container may call service serv through Ξ2 , and the submodule si ready to respond to this call. Moreover, the submodule may call the request req, and the container is ready to respond. The request req in the container is even more general than what is required from the submodule. Notice that Figure 7 represents both interfaces one inside the other only to facilitate the comprehension. In the following, the interfaces of the submodule sockets and the interfaces of the corresponding modules will be completely separated.

4.4

LLAMAS class

At this point the main components of a LLAMAS class are defined. We defined the Petri nets we will use to define the internal behavior of each module, the notion of interface in order to provide encapsulation and the submodule sockets in order to obtain a hierarchical formalism with static instantiation. The only thing remaining to define the mechanism to "glue" all these components together. We call such mechanism a composition mechanism. Unfortunately, the definition of the composition mechanism and the definition of a LLAMAS class are mutually dependent: a class contains compositions, the compositions link the elements of a class. Furthermore, the complete definition of our composition mechanism is quite complex. Because of this, we decided to give first the definition of a LLAMAS class and a LLAMAS specification, and then we will end this section with the definition of the composition mechanism in LLAMAS: the LCM. A LLAMAS class is a template that may be instantiated, either statically or dynamically, in order to build the modules in our models. Thus, every module in a LLAMAS model will actually be an instance of a LLAMAS class. The definition of a LLAMAS class is given in Def. 4.15. In this definition, we allow the

serv

serv’

req(nat, nat)

Ξ2 serv

req(nat, pos)

Ξ1

Figure 7: Interface compatibility.


25/58

classes to have parameters that will fine tune the initial marking of their respective P/A APNs. Moreover, we define a guard to constraint these values, similarly to what is done in the Object Petri nets [Lak95]. Definition 4.15: LLAMAS class Let Σ = hS , ≤, Opi be a NWN-signature based on ClassNames, where ClassNames is an S ∗ -sorted set of class names, and X a disjoint S -sorted set of variables. A LLAMAS class is a tuple class = hname, Param, guard, net, Ξ, Sockets, Comp, Deli where: • name ∈ ClassNames s1 ,...,sn is the name of the class • Param = (x1 , . . . , xn ) ∈ X ∗ is a list of formal parameters of the class compatible with the sorts of name, i.e., we have: ∀i ∈ [1..n], xi ∈ X si • guard ∈ guard(Σ, X) is a guard to validate the values of the concrete parameters of the instances • net = hP, T, M0 i is a P/A APN • Ξ = hServ, BServ, Req, BReqi is the interface of the class • Sockets = {hΞi , termi i}, i ∈ [1..m], is a set of submodule sockets • Comp = CompAct ∪ CompPass is a set of composition axioms, where CompAct ∩ CompPass = ∅ • Del : Callersclass → Decclass is an interface delegation The composition axioms and the interface delegation will be defined later, respectively in Def. 4.21 and Def. 4.24. Both are part of the LCM, The set CompAct is called the set of active compositions, and CompPass the set of passive compositions.

We saw an example of a LLAMAS class in Figure 4. We give the formal definition of this class without the compositions in Example 4.16. Example 4.16: LLAMAS class Let us consider the NWN signature and the variables from Example 3.19. The class in that example is defined by the tuple hname, Param, guard, net, Ξ, Sockets, Comp, Deli where: • name = BCounter • Param = ($i) • guard = true • net is the P/A APN we defined in Example 4.8 • Ξ is the interface we defined in Example 4.10 • Sockets = ∅ • Comp and Del will be defined later, respectively in Def. 4.21 and Def. 4.24.


4.5

26/58

The LLAMAS Composition Mechanism

LLAMAS aims at encompassing most if not all the various extensions of Petri nets in the field of modularity. The composition mechanisms in the literature may be divided in two main categories: structural compositions and runtime communications, both categories having synchronous and asynchronous variants. We propose in this thesis a single mechanism encompassing these four variants, called the LLAMAS Composition Mechanism (LCM). This mechanism combines structural compositions and runtime communications in a single notation. Simply put, a composition in the LCM is a set of participants linked by an operator. More precisely, a composition is defined by an operator and two sets of participants, a set of called participants and a set of bound participants. The called participants are, as their name indicates, simply called by the compositions, and the same participant can be called by more than one composition. On the other hand, the bound participants become structurally part of the compositions, they are "consumed" by them. Thus, if a participant is bound by a composition, it cannot participate in any other compositions. The possible participants in a {llamas class are: • The transitions of Petri nets. For instance, two transitions may be composed in order to be fired simultaneously, which corresponds to the usual merge of transitions. • The elements of the module interfaces, to allow communication between modules. For instance, a module may call a service of a submodule while simultaneously executing some local transition. This is expressed by a composition that merges the transition with a service of the submodule interface. • The compositions themselves. For instance, when two transitions are merged together, the resulting composition constitutes a new event, that may itself participate in another composition. • The NWN calls. We saw earlier that LLAMAS implements a reference-based version of the NWN paradigm. In this paradigm, the values that are taken from the places of Petri nets may be references to other values. To communicate with the modules that are referenced with this mechanism, we allow to call the services of the corresponding module during the execution of the events. All this is described more precisely in Def. 4.17. 4.5.1

Composition participants

The transitions, the submodule services, the requests, and the compositions axioms are the elements that may participate in a composition. Together, they all called the composition participants of a LLAMAS class. This set is formally defined in 4.17. Definition 4.17: Composition participant Let class = hname, Param, guard, net, Ξ, Sockets, Comp, Deli be a LLAMAS class as defined in Def. 4.15 where: • net = hP, T, M0 i is a P/A APN as defined in Def. 4.7 • T is an S ∗ -sorted set of transition axioms as defined in Def. 4.6 • Ξ = hServ, BServ, Req, BReqi is the interface as in Def. 4.9 • Sockets = {socketi = hΞi , termi i} is a set of submodule sockets as in Def. 4.11, where each Ξi = hServi , BServi , Reqi , BReqi i


27/58

• Comp is an S ∗ -sorted set of composition axioms as defined later in Def. 4.21 Let also Impl be a function that associates a LLAMAS class to each name in ClassNames. Impl will be defined more precisely later, in Def. 4.27. We will define here the set of elements of the LLAMAS class that may participate in a composition, called the set of composition participants of the class, noted Partclass = CPartclass ∪ BPartclass where: • CPartclass = T ∪ Comp ∪ Req ∪ SubServ ∪ NWNServ is a set of calling participants where: [ [ – SubServ = {socketi .serv} is the set of services of the submodules socketi ∈S ockets serv∈Servi

– NWNServ =

[

[

[

{x.serv} is the set of services of the

name0 ∈ClassNames x∈(X)name0 serv∈Impl(name0 ).Ξ. Serv

modules references by variables • BPartclass = T ∪ Comp ∪ BReq ∪ BSubServ is a set of binding participants where: [ [ – BSubServ = {socketi .serv} is the set of services of the submodules socketi ∈S ockets serv∈BServi

Notice that CPartclass , BPartclass and Partclass are all defined as a unions of S ∗ -sorted sets, and thus they all are S ∗ -sorted sets themselves. The set CPartclass is the set of elements in class that can be called in a compositions, that is, the set of elements that can eventually participate in multiple compositions. The set BPartclass is the set of elements in class that can be bound by a composition, in which case they would only participate in this composition. The transitions and the compositions belong to both sets, which means that both the transitions and the compositions can be either called or bound. The binding interface elements, either from the submodule sockets and the interface of the class itself, can only be bound (i.e., they belong to BPartclass ), and the non-bonding interface elements can only be called (i.e., they belong to CPartclass ). Finally, the set NWNServ is the set of the services that can be accessed through a variable that references a module. Notice that the services of the class S erv are not defined as possible participants in Def. 4.17. Likewise, we did not define a set S ubReq that would contain the requests from the submodules. We will see later, in Def. 4.23, that these elements participate in another component of the LCM, the interface delegation, that will be defined later. Moreover, only the non-binding services of the modules references by NWN variables are defined as participants. Indeed, the NWN paradigm is by nature a dynamic paradigm. Each variables may reference different modules during the execution of the system. The reader may remember that the bindings in the LLAMAS compositions have a static nature, a participant bound by a composition is structurally consumed by this composition. Thus, the dynamic nature of the NWN paradigm is not compatible with the static structure of the bindings. Def. 4.17 defines two complex sets, the set of calling participants and the set of binding participants. We give examples of the elements that go in both sets in Example 4.18. Example 4.18: Composition participant In Def. 4.17 we defined the set of participants that can be called by the compositions as follows: CPartclass = T ∪ Comp ∪ Req ∪ SubServ ∪ NWNServ. We saw some examples of these elements in the various examples that we previously:


28/58

• T : the transitions t3 and t4 in Figure 6 were called respectively by the compositions c1 and c2. • Comp: the composition ReadBound in Figure 4 was called by both compositions Reset and Inc. • Req: the request Overflow in Figure 4 was called by composition Reset. • SubServ: in the module Clock from Figure 5, we say three services from the submodules that were called: Seconds.Tick, Minutes.Tick, and Hours.Tick. • NWNServ: in Figure 6 we saw an example of compositions that involved the NWN paradigm. Both compositions c1 and c2 called the service $c.T ick. We defined also the binding participants as follows: BPartclass = T ∪Comp ∪ BReq ∪ BSubServ. We also saw some examples of this set in the previous examples: • T : the transition Reset was bound by the composition Reset in Figure 4. • Comp: the composition Reset in the same figure was bound by the composition Tick. • BReq: the only example of binding request that participated in a composition was shown in Figure 3. In that figure, the request r2 was bound by composition c2. Note that composition c2 belong to the submodule in that figure. • BSubServ: once again, the only example of binding service from a submodule we saw was in Figure 3, where the service s1 was bound by the composition c1. Note that, unlike c2, c1 is defined in the container of the submodule. We defined in Def. 4.17 the set of elements that may participate in a composition, called Partclass . This set was actually defined as an S ∗ -sorted set. Indeed, all the participants may define some formal parameters, which means that every call to a composition participant must be accompanied by a list of effective parameters. The association of a participant with an adequate list of effective parameters is called a participant expression, formally defined in Def. 4.19. Definition 4.19: Participant expression Let Σ = hS , ≤, Opi be a signature and X a disjoint S -sorted set of variables. Let also Partclass be an S ∗ -sorted set of composition participants as defined in Def. 4.17, based on Σ and X. Following Def. 4.17, we define two sets of participant expressions. The set of calling participant expressions CPartExprclass is the least set such that: ∀(s1 , . . . , sn ) ∈ S ∗ , ∀part ∈ (CPartclass )(s1 ,...,sn ) , ∀(t1 , ..., tn ) ∈ T (Σ, X) s1 × ... × T (Σ, X) sn , we have call(part(t1 , ..., tn )) ∈ (CPartExprclass )(s1 ,...,sn ) . Similarly, we define the set of binding participant expressions BPartExprclass as the least set such that: ∀(s1 , . . . , sn ) ∈ S ∗ , ∀part ∈ (BPartclass )(s1 ,...,sn ) , ∀(t1 , ..., tn ) ∈ T (Σ, X) s1 × ... × T (Σ, X) sn , we have bind(part(t1 , ..., tn )) ∈ (BPartExprclass )(s1 ,...,sn ) . The set of all participant expressions built on a set Partclass is noted PartExprclass CPartExprclass ∪ BPartExprclass .

=

Example 4.20: Participant expression Consider for example the transition Inc from Figure 5. Following Example 4.8, we know that this


29/58

transition takes one parameter of sort nat. Following Def. 4.17, Inc is a composition participant of the class Clock. The participant expressions that can be defined with Inc include: • call(Inc(0)) • call(Inc(0 + 1)) • bind(Inc($c)) • bind(Inc($c + 3)) The two first expressions belong to CPartExprclass and the other two belong to BPartExprclass . 4.5.2

Compositions

In the previous paragraph we defined the set of expressions that may participate in a composition. We are now able to define what is an actual composition in the LCM. A composition is defined by a composition operator that links a list of participant expressions. We define five operators for our compositions. The first three are the merge, non-deterministic and sequential operators, noted respectively merge, any and sequence. They are called the behavioral operators, because they allow the creation of new events by combining other events. The merge operator corresponds to the classical fusion operator. The three behavioral operators are directly taken from CO-OPN [BBG01]. The other two operators, the negation and the read, respectively noted not and read, are called the observers. They they define an event that does not change the state of the system but observes if and how another actual event may be fired. Inhibitor and read arcs have been used in many high level formalisms, let us cite in particular the Object Petri Nets [Lak95]. The formal definition of the compositions is to be found in Def. 4.21. Definition 4.21: Composition axiom Let Σ = hS , ≤, Opi be a signature and X a disjoint S -sorted set of variables. Let also PartExprclass = CPartExprclass ∪ BPartExprclass be a set of participant expressions as defined in Def. 4.19. We define B = {merge, any, sequence} be the set of behavioral operators, and O = {not, read} the set of observers. A composition axiom is a tuple hop, Param, guard, Parti where: • op ∈ (B ∪ O) is a composition operator • Param = (x1 , . . . , xn ) ∈ X ∗ is a list of formal parameters of the composition • guard ∈ guard(Σ, X) is a guard ∗ • Part = (expr1 , . . . , exprm ) ∈ PartExprclass is a list of participant expressions

• if op ∈ O then m = 1: the observers can only take one and only one participant expression • if op ∈ B then m ≥ 1: the behavioral operators can work on multiple participant expressions Let us add one restriction for the binding participants in a composition. If a participant is bound by a composition, it can only be bound once, and it cannot be called at the same time. Formally: • ∀i, j ∈ [1..m], if Part[i] = bind(part(...)) and Part[ j] = call(part0 (...)) or Part[ j] = bind(part0 (...)) then ∧ part = part0 ⇒ i = j


30/58

Notice the similarity between this definition and the definition of the P/A APN transition axioms (cf. Def. 4.6). We may also define the domain of a composition axiom as domain(comp) = (s1 , . . . , sn ) where Param = (x1 , ..., xn ) and ∀i ∈ ~1, n we have xi ∈ X si . Similarly to Def. 4.6, a set of compositions can thus be trivially represented as an S ∗ -sorted set. Back in Example 4.16 we gave the formal definition of the class BCounter from Figure 4, but we did not define the compositions in Comp nor the interface delegation Del. Example 4.22 gives the formal definition of Comp, while Del will be defined in Def. 4.24. Example 4.22: Composition Let us consider the class BCounter = hParam, net, Ξ, Sockets, Comp, Deli as defined in Example 4.16. The set Comp of compositions in BCounter as depicted in Figure 4 is defined as follows: Comp = { ReadBound = hread, ($b), true, (bind(GetBound($b)))i, Reset = hmerge, X , $c = $b, (call(ReadBound($b)), bind(Reset($b)))i, Inc = hmerge, X , $c < $b, (call(ReadBound($b)), bind(Inc($b)))i, Tick = hany, X , true, (bind(Reset), bind(Inc))i } Let us see in detail the structure of the composition Reset. The first element is the merge operator, graphically represented in Figure 4 by a conjunction symbol ∧. The second element is the list of parameters, which in the case of the composition Reset is empty. The third element of the composition is its guard, $c = $b. The fourth element is the set of called participant expressions, in this case the composition ReadBound with the parameter $b. Finally, the last element of this composition is the set of bound participant expressions, in this case the transition Reset with the parameter $c. 4.5.3

Interface delegation

In the previous section we saw that a module can communicate with its container (or its submodules) by calling or binding the requests in its interface. For instance, in Figure 4, we can see that a call to the service Tick is delegated to the composition Tick. This delegation was not described by the compositions from the previous sections. Indeed, the call from the service Tick to the composition Tick is not a composition, it is what we call a delegation. Similarly, in Figure 5, we have some delegations, such as the one from the request second.overflow to the service minutes.tick. There are two kinds of delegations in a module. First, the module may receive calls or bindings from its container, by means of the services in its interface. Second, the module may also receive calls or bindings from its submodules, by means of the requests defined in the interfaces of these modules. Together, the services of the module interface and the requests of the submodules are called the interface delegates of the module, that is, the elements that receive calls and bindings from other modules. This set is formally defined in Def. 4.23

Definition 4.23: Interface delegate Similarily to Def. 4.17, let class = hname, Param, guard, net, Ξ, Sockets, Comp, Deli be a LLAMAS class as defined in Def. 4.15 where: • net = hP, T, M0 i is a P/A APN as defined in Def. 4.7 • T is an S ∗ -sorted set of transition axioms as defined in Def. 4.6


31/58

• Ξ = hServ, BServ, Req, BReqi is the interface as in Def. 4.9 • Sockets = {socketi = hΞi , termi i} is a set of submodule sockets as in Def. 4.11, where each Ξi = hServi , BServi , Reqi , BReqi i The set of elements of the LLAMAS class that are meant to receive and respond to service requests from other modules is called the set of interface delegates of the class, noted Delegatesclass . We distinguish two kinds of delegates, the calling delegates noted CDelclass and the binding delegates noted BDelclass . We define: [ [ {socket_i.req} s1,...,sn • CDelclass = Serv ∪ socket_i∈S ockets req∈(Req_i s1 ,...,sn )

• BDelclass = BServ ∪

[

[

{socket_i.req} s1,...,sn

socket_i∈S ockets req∈(BReq_i s1 ,...,sn )

Similarly to the sets of participants from Def. 4.17, the sets CDelclass , BDelclass and Delegatesclass = CDelclass ∪ BDelclass are all S ∗ -sorted sets. Notice that, unlike the sets of calling and binding participants, the sets CDelclass and BDelclass are disjoint. To define how a module responds to these requests, we will use a mechanism very similar to the compositions. In 4.21 we defined a composition as a set of composition participants linked by means of an operator. To define the behavior of a caller, we will reuse these composition participants. We call this mechanism an interface delegation, formally defined in Def. 4.24. Definition 4.24: Interface delegation Let Delegatesclass = CDelclass ∪ BDelclass be a set of delegates as defined in Def. 4.23, and PartExprclass = CPartExprclass ∪ BPartExprclass be a set of participant expressions as defined in Def. 4.19. An interface delegation is a function Del : Delegatesclass → PartExprclass such that: • ∀(s1 , . . . , sn ) ∈ S ∗ , del ∈ (Delegatesclass ) s1 ,...,sn ⇒ Del(del) ∈ (PartExprclass ) s1 ,...,sn • ∀del ∈ CDelclass , Del(del) ∈ CPartExprclass • ∀del ∈ BDelclass , Del(del) ∈ BPartExprclass • ∀part ∈ BPartclass , there is at most one delegate del ∈ Delegatesclass such that Del(del) = bind(part(t1 , . . . , tn )) The first of these conditions means that the parameters of the delegation must be compatible with the parameters sorts of the delegate del. The second and third conditions means that calling delegates must be associated with calling participant expressions, and binding delegates with binding participant expressions. The fourth condition means that each binding participant expression in BPartclass is used at most once in the delegation.


32/58

Example 4.25: Interface delegation The class Clock from Figure 5 showed the following interface delegation Del: • Del(Seconds.Overflow) = call(Minutes.Tick) • Del(Minutes.Overflow) = call(Hours.Tick) • Del(Hours.Overflow) = call(IncDays)

4.6

LLAMAS specification

In this section, we gave all the detailed definitions of the LLAMAS formalism. We defined what is a LLAMAS class, by defining all its components (a Petri net for the behavior, an interface for the encapsulation, a set of submodules for the hierarchy). We defined the LCM that provides the mechanisms to glue all these components together. There is only one feature to cover, to ensure the correctness of the bindings. In our informal description of the LLAMAS language, we indicated that each element that was bound could only be bound by one and only one composition. A more precise description of this conditions is defined in Def. 4.26, where we define what is a coherent LLAMAS class. In the following, every class we will mention will always be a coherent class. Definition 4.26: Coherent class Let class = hname, Param, guard, net, Ξ, Sockets, Comp, Deli be a LLAMAS class. class is called a coherent class if and only if each binding composition participant is bound at most once in the compositions Compor in the delegation Del. Let BindPartclass be the set of binding participants of the class as defined in Def. 4.17. class is coherent if and only if: ∀part ∈ BindPartclass , there is at most one expr = bind(part(t1 , . . . , tn )) ∈ BindPartExprclass such that: • There is a composition comp = hop, Param, guard, Parti ∈ Comp such that expr ∈ Part, or • There is an interface delegate del ∈ Delegatesclass such that Del(del) = expr The set of all the possible coherent classes that can be defined with the elements Σ, ClassNames and X is noted Classes(Σ, ClassNames, X). Having defined what a coherent class is, we are now able to give the definition of an actual LLAMAS model, called a LLAMAS specification. A LLAMAS specification is composed of a NWN-signature based on a set of class names, as defined in Def. 3.16, and, for each class name, a coherent LLAMAS class with compatible parameters. The reader may recall from Def. 4.11, that each submodule socket in a LLAMAS class has a module creation term, which is built based on a class name. Thus, each submodule socket is associated with a class name. In a LLAMAS specification, each class name is associated with a LLAMAS class. By transitivity, each submodule socket ends up associated with a unique LLAMAS class. Following 4.13, the interface of this class must be compatible with the interface of the submodule socket. The formal definition of a LLAMAS specification is given in Def. 4.27. Definition 4.27: LLAMAS specification A LLAMAS specification is a tuple hΣ, ClassNames, ObjIds, X, eval, Impli where: • Σ = hS , ≤, Opi is a NWN-signature based on ClassNames and ObjIds

5. THE LLAMAS LANGUAGE - SEMANTICS

33/58

• X is a disjoint S -sorted set of variables • eval is an evaluation function of terms • Impl : ClassNames → Classes(~Σ, ClassNames, X) is a function that associates each class name with a coherent class. Recall that each class is defined by a tuple: class = hname, Param, guard, net, Ξ, Sockets, Comp, Deli. The following conditions must be met by Impl: – Each name must be used in exactly one class: ∀cname ∈ ClassNames, Impl(cname).name = cname – The submodule sockets and the associated classes must have compatible interfaces following Def. 4.13: ∀cname ∈ ClassNames, ∀socket = hΞ socket , new module(args)i ∈ (Impl(cname). Sockets), where module ∈ ClassNames, we have (Impl(module).Ξ) ≤ Ξ socket – The ordering between the class names must reflect interface compatibility: ∀name, name0 ∈ ClassNames, name ≤ name0 ⇒ (Impl(name).Ξ) ≤ (Impl(name0 ).Ξ) following Def. 4.13 Notice that the classes in a LLAMAS specification use a restricted NWN-signature noted ~Σ, as defined in Def. 3.17. With this, we guarantee that module references cannot be used in the syntactic definitions of the classes. Module references will be created during the computation of the transition relation of a LLAMAS specification, which will be the subject of Sec. 5. Note also that two classes with compatible interfaces can be independent with relation to the subsorting relation ≤.

5

The LLAMAS language - semantics

The LLAMAS language aims at defining a standard for the definition of modular Petri nets-based formalisms. The objective is to be able to define the semantics of each formalism by creating a translation from the formalism to LLAMAS. Two main advantages arise from this approach. First, it constitutes a unified approach for defining formalisms and, as such, it can be used to reason about the common features of the formalisms. Second, the definitions of the most complex formalisms are simplified. Indeed, many advanced formalisms define the semantics (i.e., the executions defined by the models of the formalism) by translating the formalism to low-level Labelled Transition Systems (LTSs). One drawback of this approach is that it creates a conceptual gap between the high level models defined with Petri nets and their low level semantics. Another drawback is that the basic LTSs are not modular by nature, which leaves the authors with the choice of loosing the modular aspects of their formalism at runtime, or extending the basic LTSs to include the notion of modularity. In the latter case, the author had to define a new low-level formalism in order to define the semantics of his high-level formalism. While, the latter point is addressed by the Instantiable Transition Systems (ITSs) [CTM05], which defines a modular version of transition systems, we have found that this formalism is not expressive enough to define the semantics of the most advanced modular Petri nets formalisms. In short, LLAMAS is meant to be used like a virtual machine to define the executions of high-level formalisms. Unfortunately, this means that the definition of the semantics of LLAMAS, which is the purpose of this section, must use the low level approach of working directly at the LTSs level. The objective of this section is thus to obtain an LTS for any LLAMAS model as defined in Def. 5.1.


34/58

Definition 5.1: Labelled Transition System A Labelled Transition System is a triple hM, L, T ri where: • M is a possibly infinite set of states (in our case, it will be a set of markings) • L is a possibly infinite set of labels • T r ⊆ M × L × M is a transition function l

For any m, m0 ∈ M and l ∈ L, we note m −→ m0 if (m, l, m0 ) ∈ T r.

5.1

A note on the inference rules

This section makes a heavy use of inference rules. As this rules tend to be extremely complex, we tried to clarify them by using a particular syntax. An inference rule is noted as a list of premises and a conclusion. For indicative purposes (without any formal meaning), we will distinguish three kind of premises: Variable definitions These premises that indicate the structure of the different variables. These premises are noted with a letter d. Conditions These premises constrain the applicability of our inference rules. They are noted with a letter g, for "guard". Computations These are the premises where we perform the actual computations. They are indicated by the letter c. We will use inference rules to define the behavior of certain operations. Many of the operations we use are non-deterministic, and many return composite results. Usually, these definitions are given as complex terms with the form OPERAT ION(expr1 , . . . , exprn ), where the expressions are either inputs of the operation or outputs. This notation is similar to most logic programming languages, such as PROLOG. Instead, we will distinguish between the inputs and output of the operations, by using a notation OPERAT ION(expr1 , . . . , exprn ) → hexpr10 , . . . , exprm0 i, to indicate an operation that takes n inputs and returns a result composed of m elements. Please note that this does note mean that our operations are functions, they are still non-deterministic and they can return different results. For instance, the operation FIRE(gm, ev) → gm0 indicates that firing the event ev from the marking gm, one possible result is the marking gm0 .

5.2

LLAMAS model

In Def. 4.27 we defined a LLAMAS specification, that gave the basic structure on which the LLAMAS models are built. A LLAMAS model is built by creating one main instance of a LLAMAS specification, called the "root" instance. This root will be the main instance during the whole execution of the system, the other instances will be referenced by this root, either directly or indirectly. Thus, to define a LLAMAS model, we need three elements: a LLAMAS specification, a module creation term to create the "root" instance, and the identifier of this root instance. This is formally defined in Def. 5.2. Definition 5.2: LLAMAS model A LLAMAS model is defined by a triple model = hSpec, termroot , idroot i where: • Spec = hΣ, ClassNames, ObjIds, X, eval, Impli is a LLAMAS specification


35/58

• termroot ∈ T (Σ, ∅)name is a module creation term, where name ∈ ClassNames is the name of a LLAMAS class • idroot ∈ ObjIdsname is the identifier of the root instance. In the following, we will assume that a LLAMAS model has been correctly defined, and most definitions will reference these elements.

5.3

Evaluation of guards

We gave in Def. 4.3 the definition of the guards that constrain the behavior of the LLAMAS modules. The evaluation of these guards is based on the evaluation of the terms they contain, as in Def. 3.14. Simply put, an equality between two terms t = t0 is evaluated to the boolean value true if the two terms are evaluated to the same value. The formal definition of this evaluation is given in Def. 5.3. Definition 5.3: Evaluation of guards Back in Def. 4.3, the guards we defined were based on equalities and inequalities of terms. To define the semantics of these guards, we will rely on the evaluation of terms from Def. 3.14. Let σ ∈ subst(Σ, ∅) be a closed substitution. The evaluation of guards based on σ is a function evalσ : guard(T (Σ, X)) → B defined by: • evalσ (true) = trueB • evalσ ( f alse) = f alseB • evalσ (t = t0 ) = trueB ⇔ evalσ (t) = evalσ (t0 ) • evalσ (t , t0 ) = trueB ⇔ evalσ (t) , evalσ (t0 ) • evalσ (g1 ∧ g2) = trueB ⇔ evalσ (g1) = trueB ∧B evalσ (g2) = trueB • evalσ (g1 ∨ g2) = trueB ⇔ evalσ (g1) = trueB ∨B evalσ (g2) = trueB Note that we are only defining the evaluation of guards based on closed substitutions, and thus, there are not variables in the evaluations of the terms inside the guard. Example 5.4 gives some examples of guard evaluations. Example 5.4: Evaluation of guards Consider the evaluation function eval and the substitution σ from Example 3.15. This substitution was defined by σ($x) = 1 and σ($y) = 2. We have the following results: • evalσ (true) = trueB • evalσ (0 + 1 = 1 + 0) = trueB as evalσ (0 + 1) = evalσ (1 + 0) = 1 • evalσ (1 + $y = $x + 1) = f alseB as evalσ (1 + $y) = 3 and evalσ ($x + 1) = 2 • evalσ (1 + $y , $x + 1) = trueB


5.4

36/58

Operations on place markings

Back in Def. 4.5 we defined the markings of our P/A APN. During the execution of our modules, these markings will be modified at each step by adding and removing resources. To define this, we must first define some basic operations both in the multisets we defined in Def. 4.1 and in the place markings we defined in Def. 4.5. The first of these definitions is given in Def. 5.5. Definition 5.5: Operations on multisets We define the following operations on multisets by using the standard operations on the natural numbers: • inclusion: ∀m1, m2 ∈ mult(Σ, X), We note m1 ⊆ m2 ⇔ ∀t ∈ T (Σ, X), m1(t) ≤N m2(t) • addition: ∀m1, m2, m3 ∈ mult(Σ, X), m1 + m2 = m3 ⇔ ∀t ∈ T (Σ, X), m3(t) = m1(t) +N m2(t) • substraction: ∀m1, m2, m3 ∈ mult(Σ, X), m1 − m2 = m3 ⇔ ∀t ∈ T (Σ, X), m3(t) = max(m1(t) −N m2(t), 0) • application of a substitution: ∀m1, m2 ∈ mult(Σ, X), σ ∈ subst(Σ, X), applyσ (m1) = m2 ⇔ ∀t ∈ T (Σ, X), m2(t) = Σt1∈T (Σ,X) s.t. applyσ (t1)=t m1(t1) • evaluation: ∀m1, m2 ∈ mult(Σ, X), and for each evaluation evalσ , evalσ (m1) = m2 ⇔ ∀t ∈ T (Σ, X), m2(t) = Σt1∈T (Σ,X) s.t. evalσ (t1)=t m1(t1) The application of a substitution and the evaluation in the terms as we defined them in Def. 3.12 and Def. 3.14 are not injective functions. This means that multiple terms in a multiset could give the same result. To get the cardinality of such result, we compute the sum of the cardinalities of its pre-images. Note that the addition, the subtraction, the application of substitutions and the evaluations in multisets all return a multiset as a result. We give small examples of these operations in Example 5.6. Example 5.6: Operations on multisets Let us consider the multisets m1 = [30 true, 40 (2+$x), 20 ($y+1)] and m2 = [40 true] (we use the notation introduced in Example 4.2). We have the following results: • Neither m1 ⊆ m2 nor m2 ⊆ m1 are true • m1 + m2 = m2 + m1 = [70 true, 40 (2 + $x), 20 ($y + 1)] • m1 − m2 = [40 (2 + $x), 20 ($y + 1)], more specifically, m1 − m2(true) = 0 • m2 − m1 = [true] Let us consider a substitution σ such that σ($x) = 1 and σ($y) = 2. The application of this substitution to our multiset gives the following result:


37/58

applyσ (m1) = [30 true, 60 (2 + 1)] Note that both terms (2 + $x) and ($y + 1) gave the result (2 + 1) after applying the substitution σ. Thus, following the last point in Def. 5.5, the cardinality of (2 + 1) in the resulting multiset is the sum of the cardinalities of (2 + $x) and ($y + 1) in the original multiset. Finally, let us consider the evaluation function from Example 3.15 and apply it to m1. We get: evalσ (m1) = [30 true, 60 3] The operations we defined for the multisets are directly extensible to the place markings, as defined in Def. 5.7. Definition 5.7: Operations on the place markings The operations that may be performed on the place markings are a trivial extension of the operations defined for the multisets in 5.5: • inclusion: ∀ma1, ma2 ∈ mark(Σ, X, P), ma1 ⊆ ma2 ⇔ ∀p ∈ P, ma1(p) ⊆ ma2(p) • addition: ∀ma1, ma2, ma3 ∈ mark(Σ, X, P), ma3 = ma1 + ma2 ⇔ ∀p ∈ P, ma3(p) = ma1(p) + ma2(p) • substraction: ∀ma1, ma2, ma3 ∈ mark(Σ, X, P), ma3 = ma1 − ma2 ⇔ ∀p ∈ P, ma3(p) = ma1(p) − ma2(p) • evaluation: ∀ma1, ma2 ∈ mark(Σ, X, P), and for each evaluation evalσ , ma2 = evalσ (ma1) ⇔ ∀p ∈ P, ma2(p) = evalσ (ma1(p))

5.5

States of a LLAMAS : global markings

Up until now, we have defined some operations on the structures that were syntactically defined in the previous section. These operations will be useful while building the transition relation of a LLAMAS model. We will now define the set of possible states of a LLAMAS specification, called global markings (by opposition to the place markings, which were local markings to a single module). A global marking is composed of instances of LLAMAS classes. The reader may recall that a LLAMAS class was defined in Def. 4.15 as a tuple that included a P/A APN and a set of submodule sockets. To define an instance of a LLAMAS class, we need three elements: • The identifier of the instance • The place marking of the P/A APN • A function to associate each submodule socket with the instance it contains Moreover, as in most object-oriented formalisms, there is one special instance called root, which is the main instance of the model. This instance will reference other instances, which will reference other instances, and so on. We will see later, in Def. 5.34 that the instances not referenced (either directly or indirectly) by the root will be discarded at each computation step. For simplicity reasons, we separate the association of an instance identifier with a place marking (called an instance marking and formally defined in Def. 5.8), from the hierarchical structure (called instance hierarchy and formally defined in Def. 5.9). This is because, during the execution of the system,


38/58

the marking of each instance will evolve, while the hierarchical structure will remain fixed (unless the instance itself is destroyed). Definition 5.8: Instance marking Let Spec = hΣ, ClassNames, ObjIds, X, eval, Impli be a LLAMAS specification and class = hname, Param, guard, net, Ξ, Sockets, Comp, Deli be a class from Impl. An instance marking of class is a pair mark = hid, pmi where: • id ∈ ObjIdsname is the instance identifier • pm ∈ mark(Σ, ∅, P) is a place marking, where P is the set of places of net as defined in Def. 4.5 In Def. 4.5 we defined that pm is a function that associates a multiset of the right sort to each place in net (pm : P → multi(Σ, X)). We note hid, emptyPmi the particular instance marking where each place is associated with the empty multiset: ∀p ∈ P, ∀t ∈ T (Σ, X), emptyPm(p)(t) = 0

Definition 5.9: Instance hierarchy Let Spec = hΣ, ClassNames, ObjIds, X, eval, Impli be a LLAMAS specification and class = hname, Param, guard, net, Ξ, Sockets, Comp, Deli be a class from Impl. A class hierarchy of class is a pair mark = hid, subi where: • id ∈ ObjIdsname is the instance ID • sub : Sockets → ObjIds is a function that associates each submodule socket of the class to an instance ID During the execution of a LLAMAS system, the states of the model will be defined by multiple instances, each one with its own instance marking and instance hierarchy. The association of multiple instances is called a global marking, defined in Def. 5.10. Each state of a LLAMAS model will be defined as a global marking. Definition 5.10: Global marking Let Spec = hΣ, ClassNames, ObjIds, X, eval, Impli be a LLAMAS specification. A global marking of Spec is a triple gm = hIds, Marks, Hi where: • Ids = {id1 , . . . , idn } ⊆ carrier(ObjIds) is a finite set of instance identifiers • Marks = {hidi , pmi i}, i ∈ [1..n] is a set of instance markings such that each id ∈ Ids appears in exactly one instance marking. • H = {hidi , subi i}, i ∈ [1..n] is a set of instance hierarchies such that each id ∈ Ids appears in exactly one instance hierarchy. Notice that Marks and H can be easily viewed as functions. The only reason for not defining them as such is the complexity of their co-domains. Indeed, in an instance marking hid, pmi, the domain of the place marking pm depends on the identifier id. Nevertheless, with a slight abuse of notation, we will note both Marks and H as if they were defined as functions. Thus, we note Marks(id) = pm if hid, pmi ∈ Marks and H(id) = sub if hid, subi ∈ H. We will only define one operation for our global markings: the disjoint union. The union of two global markings is only defined in their sets of identifiers are non-overlapping. This restriction is very


39/58

important, as it ensures that there will always be only one instance in a global marking for every instance identifier. This disjoint union, noted ADD is deterministic, but it is only partially defined, not all pairs of global markings can be added. Because of this, the definition of ADD is the first of many inference rules in this document, given in Inference 5.11. Inference rule 5.11: Addition of global markings

ADD

mark1 = hIds1 , Marks1 , H1 i mark2 = hIds2 , Marks2 , H2 i Ids1 ∩ Ids2 = ∅

d(0) d(1) g(2)

mark2 = hIds1 ∪ Ids2 , Marks1 ∪ Marks2 , H1 ∪ H2 i ADD(mark1, mark2) → mark3

c(3)

Remarks: (1) (2) (3) Both global markings must be defined over different instances, with different identifiers. (4) The addition of global markings is simple the union of their instance identifiers, their respective instance markings and their respective instance hierarchies. The operation ADD is trivially associative and commutative, and thus we can trivially extend it to take more than two arguments, by noting: ADD(mark1 , mark2 , . . . , markn ) = ADD(mark1 , (mark2 , (. . . , markn ))) . . .)

5.6

Events in a LLAMAS model

Having defined the set of possible states of a LLAMAS model, we can now start to build the transition relation itself. From each state of our model (defined by a global marking), some events may be executed, leading to some successor states, thus building the transition relation of the model. The next step in our definition is to determine what are the events that can be executed from a marking. The first events we will mention are the most obvious ones, the Petri nets transitions. Indeed, traditionally, Petri nets formalisms define the events by means of transitions. In LLAMAS, we add another kind of events, the composition axioms. Indeed, we defined our compositions as elements that combine the behavior of some participants to form a new event. Thus, to define the behavior of a composition, we have to define the behavior of each one of its participants. The reader may recall that the participants of the compositions include the transitions, the compositions themselves, and the elements in the interface of the different modules. In a nutshell, to define the behavior of a LLAMAS module, we have to define the behavior of all the composition participant from each class in the model. This is formally defined in Def. 5.12. Definition 5.12: Set of events Let S pec = hΣ, ClassNames, Ob jIds, X, veal, Impli. Remember that for each class name cname ∈ ClassNames, Impl(name) = hcname, Param, guard, net, Ξ, Sockets, Comp, Del is the class [ that implements cname. The set of possible events that can be executed is the set PartExprImpl(cname) , where PartExprclass is the set of participant expressions of each cname∈ClassNames

class in the model as defined in Def. 4.19. The reader may recall that each set PartExprclass is built over the set of participants Partclass , which is defined by: • The transitions of the Petri net,


40/58

• The compositions, • The requests of the interface of the class, • The services in the interface of each submodule, and, • The NWN calls, i.e., the calls to the interface of the modules referenced by variables. Thus, to define the behavior of a LLAMAS model, we have to define the behavior of each one of these elements. In LLAMAS, this behavior is defined by means of structures called event effects.

5.7

Pre and Post conditions : event effects

Usually, in most Petri nets formalisms, each event is defined by a set of pre-conditions (tokens removed from the current marking) and a set of post-conditions (tokens added to the current marking), and define the execution of the event with the ubiquitous formula M 0 = M − Pre + Post. In our definition, we extend this approach by including the fact that, during the execution of each event, some modules may have been dynamically created. Thus, the execution of some event is defined by a pre-condition, a post-condition and a set of new modules. This structure is called the effect of the event, formally defined in Def. 5.13. Definition 5.13: Event effect An event effect is a tuple hOldIds, Pre, Post, NewGmi where: • OldIds = {id1 , . . . , idm } ⊆ carrier(Ob jIds) is a set of instance identifiers • Pre = {hidi , pmi i}, i ∈ [1..m] is a set of instance markings called pre-conditions such that each id ∈ OldIds appears in exactly one instance marking. We note Pre(id) = pm if hid, pmi ∈ Pre. • Post = {hidi , pmi i}, i ∈ [1..m] is a set of instance markings called post-conditions such that each id ∈ OldIds appears in exactly one instance marking. We note Post(id) = pm if hid, pmi ∈ Post. • NewGm = hNewIds, NewMarks, NewHi is a global marking containing the instances that have been created by the event, such that OldIds ∩ NewIds = ∅. The event effects will be the central pivot of our definition of the semantics of LLAMAS. Contrary to most modular formalisms in the literature, the computation of the event effects in LLAMAS is computed at runtime, to cope with the recursive nature of our compositions. Thus, to define the execution of an event from a given marking, we will first compute the effect of this event, and then we will apply this effect to the current marking. Let us first see how to compute the effect of each event in a LLAMAS model.

5.8

Computing event effects

In Def. 5.12 we defined the set of events in a model as the set of participant expressions from all the classes in the model. Back in Def. 4.19, we defined these participant expressions with the form call(part(t1 , . . . , tn )) and bind(part(t1 , . . . , tn )). The distinction between calling and binding participant expressions is purely syntactical, it served its purpose to restrain the number of bindings that a given element can have, but it has no more use in the computation of the semantics. This leads us to the defini-


41/58

tion in Inference 5.14, where we indicate that we can simply forget about the call and bind element in a participant expression. Inference rule 5.14: Computing the effects of the events: participant expressions EFFECT

EFFECT(gm, hid, part(t1 , . . . , tn )i) → eff EFFECT(gm, hid, call(part(t1 , . . . , tn ))i) → eff

c(1) *

EFFECT

EFFECT(gm, hid, part(t1 , . . . , tn )i) → eff EFFECT(gm, hid, bind(part(t1 , . . . , tn ))i) → eff

c(1) *

Remarks: (1) These two rules are identical, they indicate that the effect of an expression does not depend on it being a calling or a binding participant expression.


42/58

We are now ready to go into the most complex definitions of the behavior of a LLAMAS model. Let us first start by the computation of the effect of a transition, defined in Inference 5.15. This definition is quite complex, and this is mainly because of the instantiation mechanism. Indeed, our instantiation mechanism is based on special terms, called instance creation terms. These terms can appear in multiple locations in a transition, they can appear in the parameters, the guard, the pre-conditions and the postconditions. All these instantiations must be dealt with during the computation of the execution of the transition. The precise definition of the different instantiation operations will be given later, in Sec. 5.10. Inference rule 5.15: Computing effects of the events : transitions gm = hIds, Marks, Hi tr = hParam, guard, pre, posti ∈ T t1 , . . . , tn ∈ T (Σ, ∅) INST_LIST((t1 , . . . , tn )) → h(t10 , . . . , tn0 ), markParamsi σ ∈ subst(Σ, ∅) applyσ (Param) = (t10 , . . . , tn0 )

d(1) d(2) d(3) c(4) c(5) * g(6)

INST_GUARD(apply sigma (guard)) → hguard0 , markGuardi evalσ (guard0 ) = true

c(7) g(8)

INST_PM(applyσ (pre)) → hpre, ∅i INST_PM(applyσ (post)) → hpost0 , markPosti

c(9) c(10)

ADD(markParams, markGuard, markPost) → NewGm [ Pre = {hid, evalσ (pre)i} ∪ {hid0 , emptyPmi} 0 id ∈Ids\{id} [ {hid0 , emptyPmi} Post = {hid, evalσ (post0 )i} ∪

c(11) c(12) c(13)

id0 ∈Ids\{id}

EFFECT

eff = hIds, Pre, Post, NewGmi EFFECT(gm, hid, tr(t1 , . . . , tn )i) → eff

c(14)

Remarks: (1) (2) gm is a global marking, tr is a transition axiom (3) The parameters must be closed terms (4) Instantiate the effective parameters of the transition. If any parameter contains an instance creation term, an instance will be created in markParams and the term will be replaced by the identifier of this instance. (5) (6) Consider some substitution σ that satisfies the parameters of tr. Note that there may be potentially infinite substitutions that satisfy this condition. (7) (8) Instantiate the guard of the transition, and we check that the guard is evaluated to true. (9) There cannot be any module creation term in the pre-conditions of the transition. Indeed, the pre-conditions represent the tokens that will be removed from the current marking, and we cannot remove any reference that was not created previously. (10) Instantiate the post-conditions of the transition (11) Join the instances that were created in the parameters, the guard and the post-conditions in NewGm (12) (13) Define the pre and post-conditions of the transition in the instance with identifier id. A transition is always a local event, and it affects only the instance in which it is being executed. (14) Together, Pre, Post and NewGm define the effect of the transition on the identifiers Ids.


43/58

After defining the effect of the transitions, we can define the behavior of the compositions. Back in Def. 4.21 we defined a composition axiom as an operator, a set of parameters, a guard and a list of participant expressions. We can clearly separate the behavior of a composition in two. First, we define what the behavior of the parameters and the guard. Then, we will define the behavior of the composition itself, by means of a special operation called EFFECT_COMP, which will be defined later. Let us first start by the first part of this definition, in Inference 5.16. Inference rule 5.16: Computing the effects of the events: composition axioms gm = hIds, Marks, Hi comp = hop, Param, guard, Parti t1 , . . . , tn ∈ T (Σ, ∅)

EFFECT

d(1) d(2) d(3)

INST_LIST((t1 , . . . , tn )) → h(t10 , . . . , tn0 ), markParamsi σ ∈ subst(Σ, ∅) applyσ (Param) = (t10 , . . . , tn0 ) INST_GUARD(apply sigma (guard)) → hguard0 , markGuardi evalσ (guard0 ) = true Part = (part1 , . . . , partn )

c(4) c(5) * g(6) c(7) g(8) d(9)

applyσ (part1 ) = part10 .. .

c(10)

applyσ (partn ) = partn0

c(11)

EFFECT_COMP(gm, hid, op(part10 , . . . , partn0 )i) → efftemp efftemp = hIds, Pre, Post, NewGmtemp i ADD(markParams, markGuard, NewGmtemp ) → NewGm eff = hIds, Pre, Post, NewGmi EFFECT(gm, hid, comp(t1 , . . . , tn )i) → eff

c(12) c(13) c(14) c(15)

Remarks: (1) (2) gm is a global marking, event defined over a composition axiom comp (3) The parameters must be closed terms (4) We instantiate the effective parameters of the composition. If any parameter contains an instance creation term, an instance will be created in markParams and the term will be replaced by the identifier of this instance. (5) (6) We consider some substitution σ that satisfies the parameters of comp. Note that there may be potentially infinite substitutions that satisfy this condition. (7) (8) We instantiate the guard of the composition, and we check that the guard is evaluated to true. (9) (10) - (11) We apply the substitution to the participants of the composition and... (12) (13) ...we compute the effect of the composition itself by means of the operation EFFECT_COMP. It returns some temporary effect efftemp . (14) (15) The complete effect of the composition axiom is the pre and post-conditions of the composition itself, and the new instances that were created in the parameters, the guard and the composition itself. At this point, we have defined the behavior of the two biggest events in the LLAMAS models: the transitions and the compositions. The other events, i.e., the services in the submodule interfaces, and, the requests and the NWN calls, are events that serve to communicate between different modules. To execute them, we must simply look for the corresponding event in the module that receives the communication.


44/58

Consider for instance the submodule services, whose behavior is defined in Inference 5.17. Whenever a module calls a service from one of its submodule sockets, this call is transmitted to the instance referenced by this socket (by using the instance hierarchy H as defined in Def. 5.9). Then, to determine what element in this instance must respond, we use the interface delegation Del from the corresponding class, as defined in Def. 4.24. Inference rule 5.17: Computing effects of the events : submodule services

EFFECT

gm = hIds, Marks, Hi H(id)(socket) = id0 id0 ∈ Ob jIdsname Impl(name) = hname, Param, guard, net, Ξ, Sockets, Comp, Deli Del(serv) = expr EFFECT(gm, hid0 , expr(t1 , . . . , tn )i) → eff EFFECT(gm, hid, socket.serv(t1 , . . . , tn )i) → eff

d(1) d(2) d(3) d(4) d(5) c(6)

Remarks: (1) gm is a global marking. (2) (3) The instance referenced by the submodule socket socket has the identified id0 , which is an identifier of the class name name. (4) (5) We use the interface delegation Del from the class corresponding to name in order to determine the expression that must receive this call. (6) This expression is called with the same parameters as the original call. The behavior of a request mirrors the behavior of the submodule services. While calling a submodule service forwards the call to a submodule, calling a request forwards the call to the container of the instance. This is formally defined in Inference 5.18. Notice the similarity between Inference 5.17 and Inference 5.18. Inference rule 5.18: Computing effects of the events : requests

EFFECT

gm = hIds, Marks, Hi H(id0 )(socket) = id id0 ∈ Ob jIdsname Impl(name) = hname, Param, guard, net, Ξ, Sockets, Comp, Deli Del(socket.req) = expr EFFECT(gm, hid0 , expr(t1 , . . . , tn )i) → eff EFFECT(gm, hid, req(t1 , . . . , tn )i) → eff

d(1) d(2) d(3) d(4) d(5) c(6)

Remarks: (1) gm is a global marking. (2) (3) The container of id has the identifier id0 , and id0 references id in the submodule socket socket. id0 is an identifier of the class name name. (4) (5) We use the interface delegation Del from the class corresponding to name in order to determine the expression that must receive this call. (6) This expression is called with the same parameters as the original call. There is one final kind of composition participant that we must define, the NWN calls. In our implementation of the NWN paradigm, an instance can call a service of a dynamically created instance by


45/58

means of its identifier, by using an expression id0 .serv(t1 , . . . , tn ). This call is trivially forwarded to the corresponding instance, as defined in Inference 5.19. Inference rule 5.19: Computing effects of the events : NWN calls EFFECT

EFFECT(gm, hid0 , serv(t1 , . . . , tn )i) → eff EFFECT(gm, hid, id0 .serv(t1 , . . . , tn )i) → eff

c(1)

Remarks: (1) Whenever a module id calls a service from an identifier id0 by means of a call id0 .event, the call is trivially forwarded to the instance with identifier id0 .

5.9

Computing the effects of compositions

Back in Inference 5.16, we delegated the definition of the behavior of the actual compositions to an operation EFFECT_COMP. This is arguable the most interesting operation in our definitions, as it precisely defines the behavior of our composition operators. Remember that there are five of these operators in LLAMAS, the behavioral operators merge, any and sequence, and the observers not and read. The behavior of the first of these operators, the merge, is defined in Inference 5.20. Inference rule 5.20: Composition effects : merge

EFFECT_COMP

gm = hIds, Marks, Hi

d(1)

EFFECT(gm, hid, part1 i) → hIds, Pre1 , Post1 , NewGm1 i .. .

c(2)

EFFECT(gm, hid, partn i) → hIds, Pren , Postn , NewGmn i

c(3)

Pre1 + . . . + Pren = T otalPre Post1 + . . . + Postn = T otalPost ADD(NewGm1 , . . . , NewGmn ) → T otalNewGm eff = hIds, T otalPre, T otalPost, T otalNewGmi EFFECT_COMP(gm, merge(part1 , . . . , partn )) → eff

g(4) g(5) g(6) c(7)

Remarks: (1) gm is a global marking. (2) -(3) Compute the individual markings of all the participants in the composition. (4) (5) (6) The pre and post-condition of the composition is simply the addition of all the pre and postconditions of the individual participants. The instances created in all the participants are also added. Note that the operator ADD implies that all the instances created by the various participants must have different identifiers. (7) These elements allow to define the effect of the whole composition. The operator any is simpler to define. Indeed, if a set of participants is composed with this operator, executing the composition is the same as executing one of these participants, chosen non-deterministically.


46/58

This is defined in Inference 5.21. Inference rule 5.21: Composition effects : any

EFFECT_COMP

i ∈ [1..n] EFFECT(gm, hid, parti i) → eff EFFECT_COMP(gm, hid, any(part1 , . . . , partn )) → eff

c(1) * d(2)

Remarks: (1) (2) Choose any of the participants of the composition, and compute its effect. The result is the effect of the composition. While the behavior of the compositions that use the non-deterministic operator any is very simple to define, the same cannot be said about the sequential operator sequence. Indeed, if two events are composed with this operator, the first one is fully executed, and the the second one is executed. This means that we must not only compute the effect of the first event, but we must also compute its result in order to be able to compute the behavior of second event. All this becomes more complex when considering more than two events. To define this behavior, we will use an inductive definition, broken into a basic case with only one event in Inference 5.22, and an inductive case of more than one event in Inference 5.23. Inference rule 5.22: Composition effects : sequence (1) EFFECT_COMP

EFFECT(gm, hid, event1 i) → eff EFFECT_COMP(gm, hid, sequence(event1 )i) → eff

c(1)

Remarks: (1) The basic case of the sequence operator, where we compose only one event, is trivially defined as the execution of this single event.


47/58

Inference rule 5.23: Composition effects : sequence (2)

EFFECT_COMP

n>1 EFFECT(gm, hid, event1 i) → hIds, Pre1 , Post1 , NewGm1 i NewGm1 = hIds1 , Marks1 , H1 i

g(1) c(2) d(3)

FIRE(gm, hid, event1 i) → gm1 EFFECT_COMP(gm1 , hid, sequence(event2 , . . . , eventn )i) → eff2 eff2 = hIds ∪ Ids1 , Pre2 , Post2 , NewGm2 i

c(4) c(5) d(6)

efftemp = hIds ∪ Ids1 , Pre2 |Ids1 , Post2 |Ids1 , NewGm2 i APPLY_EFFECT(NewGm, efftemp ) → NewGmT otal T otalPre = Pre1 + (Pre2 |Ids − Post1 ) T otalPost = Post2 + (Post1 |Ids − Pre2 |Ids ) eff = hIds, T otalPre, T otalPost, NewGmT otali EFFECT_COMP(gm, hid, sequence(event1 , . . . , eventn )i) → eff

c(7) c(8) c(9) c(10) c(11)

Remarks: (1) The inductive case of our definition is more complex. This case is only applied if we have strictly more than one participant composed. (2) (3) Compute the effect of the first participant event1 . (4) Now we need to actually fire the first participant, by using the operation FIRE, which will be defined later, in Inference 5.35. (5) (6) From the resulting marking, we fire all the other participants and get their effect eff2 . This effect works both in the instances that were defined in the original marking gm and the instances that were created by event1 . We must separate the treatment for both sets of instances. (7) (8) First, we apply eff2 to the instances NewGm that were created by event1 . For this, we use a restriction of eff2 . (9) (10) Second, we compute the pre and post-conditions on the instances that were already defined in the original marking. The second event can use the resources that were produced by the first event. (11) The complete effect is obtained by this modified pre and post conditions, and the instances created by event1 and modified by eff2 . Finally, we define the behavior of the two observers, the negation not and the read operator read. These two operators have very simple and very similar definitions: they have absolutely no effect, but they simple check that their participants respectively cannot and can be fired. These two definitions are


48/58

to be found in Inference 5.24 and Inference 5.25. Inference rule 5.24: Composition effects : not successors(gm, [ event) = ∅ EmptyPre = {hid, emptyPmi} id∈Ids [ EmptyPost = {hid, emptyPmi}

g(1) c(2) c(3)

id∈Ids

EFFECT_COMP

EFFECT_COMP(gm, not(event)) → hIds, EmptyPre, EmptyPost, ∅i

Remarks: (1) Check that the event cannot be executed from the marking gm. For this, we use the function successors, which computes the set of successors of gm by executing event. The function successors will be defined later, in Def. 5.37. (2) (3) The effect of a composition that uses the operator not is empty, no marking is modified by such composition.

Inference rule 5.25: Composition effects : read successors(gm, [ event) , ∅ EmptyPre = {hid, emptyPmi} id∈Ids [ EmptyPost = {hid, emptyPmi}

g(1) c(2) c(3)

id∈Ids

EFFECT_COMP

EFFECT_COMP(gm, read(event)) → hIds, EmptyPre, EmptyPost, ∅i

Remarks: (1) Check that the event can be executed from the marking gm. For this, we use the function successors, which computes the set of successors of gm by executing event. The function successors will be defined later, in Def. 5.37. (2) (3) The effect of a composition that uses the operator read is empty, no marking is modified by such composition.

5.10

Instantiation

Up until now, we have defined the effects of all the events in a LLAMAS model. Many of these events involved the operation of instantiation, where instances are dynamically created and added to the markings of the model. This operation occurs in different places: in the parameters of the events, in the post conditions, in their submodule sockets, etc. Nevertheless, any instantiation is always indicated by an instance creation term. Because of this, we will start by defining the instantiation of a single term. The instantiation of a single term returns another term where the instance creation terms have been replaced by the identifiers of the instances created, and a global marking containing all the instances created. This definition is split in two. First, we define in Inference 5.26 the instantiation of a term other than an instance creation term. Then we define in Inference 5.27 the instantiation of an instance creation term. Notice that both definitions work on closed terms, we assume that closed substitutions have already been


49/58

applied to the terms prior to using this operation. Inference rule 5.26: Instantiation of a term

INST_TERM

term = op(t1 , . . . , tn ) ∈ T (Σ, ∅) op ∈ Op0

d(1) d(2)

INST_LIST((t1 , . . . , tn )) → h(t10 , . . . , tn0 ), markS ubT ermsi term0 = op(t10 , . . . , tn0 ) INST_TERM(term) → (term0 , markS ubT erms)

c(3) c(4)

Remarks: (1) (2) The term is a closed term that uses the operator op, which is a "normal" operator as defined in Def. 3.16. Thus, this is not an instance creation term. Nevertheless, one or more of its subterms could be or contain instance creation terms. (3) Because of this, we instantiate the list of subterms by using the operator INST_LIST, which will be defined later, in Inference 5.28. (4) The resulting term is the original term where the eventual instance creation subterms have been replaced with the identifiers of the instances created.


50/58

Inference rule 5.27: Instantiation of a term (2) term = new cName(t1 , . . . , tn ) ∈ T (Σ, ∅) cName ∈ ClassNames Impl(cName) = hcName, Param, guard, net, Ξ, Sockets, Comp, Deli net = hP, T, M0 i Sockets = {hΞi , termi i}

INST_TERM

d(1) d(2) d(3) d(4) d(5)

id ∈ Ob jIdscname

c(6) *

INST_LIST((t1 , . . . , tn )) → h(t10 , . . . , tn0 ), markParami σ ∈ subst(Σ, ∅) applyσ (Param) = (t10 , . . . , tn0 )

c(7) c(8) * g(9)

INST_GUARD(apply sigma (guard)) → hguard0 , markGuardi evalσ (guard0 ) = true

c(10) g(11)

INST_PM(applyσ (M0 )) → hM00 , markM0i INST_SOCKETS(applyσ (Sockets)) → hsubs, markS ocketsi mark = h{id}, {(id, M00 )}, {(id, subs)}i ADD(mark, markParam, markGuard, markM0, markSockets) → markT otal INST_TERM(term) → hid, markT otali

c(12) c(13) c(14) c(15)

Remarks: (1) (2) (3) The term is a closed instance creation term, that creates an instance of the class Impl(cName). (4) (5) We extract the Petri net and the submodule sockets of the class Impl(cName), as they will be used to create the instance marking and the instance hierarchy of the resulting marking. (6) We chose an identifier of the right class name. Any identifier can be chosen here. (7) We instantiate the subterms of term. (8) (9) We consider some substitution σ that satisfies the parameters of the class. Note that there may be potentially infinite substitutions that satisfy this condition. (10) (11) We instantiate the guard of the class, and we check that the guard is evaluated to true. (12) (13) (14) We instantiation the place marking M0 and the submodule sockets. These elements define the instance marking and the instance hierarchy of the local instance. (15) Add the instances created in all the elements considered until now. Note that all these instances must have different identifiers. The operation to instantiate a term INST_TERM is trivially extended to a list of terms in Infer-


51/58

ence 5.28. Inference rule 5.28: Instantiation of a list of terms

INST_LIST

list = (t1 , . . . , tn ) ∈ T (Σ, ∅)∗

d(1)

INST_TERM(t1 ) → (t10 , mark1 ) .. .

c(2)

INST_TERM(tn ) → (tn0 , markn )

c(3)

ADD(mark1 , . . . , markn ) → markT otal INST_LIST(list) → ((t10 , . . . , tn0 ), markT otal)

c(4)

Remarks: (1) All the terms in the list must be closed terms. (2) - (3) Instantiate each term in the list, and keep the markings obtained. (4) Add the markings obtained from all the terms. Note that the ADD operation ensures that the instances that were created in all the terms have different identifiers. The definition of the instantiation on the guards is rather trivial, and can be quite cumbersome to define. We give an example in Inference 5.29, where we define the instantiation of the equalities. The instantiation of the other guards can be easily derived from this simple example. Inference rule 5.29: Instantiation of a guard (equalities)

INST_GUARD

t1 , t2 ∈ T (Σ, ∅) INST_TERM(t1 ) → (t10 , mark1 ) INST_TERM(t2 ) → (t20 , mark2 ) ADD(mark1 , mark2 ) → markT otal INST_LIST(t1 = t2 ) → ((t10 = tn0 ), markT otal)

g(1) c(2) c(3) c(4)

Remarks: (1) We consider a guard that represented an equality between two closed terms. (2) (3) (4) Instantiate both terms, and add the resulting global markings. The result is the equality between the instantiations of the two original terms. Apart from the guards, the module creation terms can also be present in the multisets contained in the different place markings. The definition of the instantiation of a multiset is rather straightforward, and it


52/58

is given in Inference 5.30. Inference rule 5.30: Instantiation of a multiset

INST_MS

T erms = {term ∈ T (Σ, X) s.t. ms(term) > 0} T erms = (term1 , . . . , termn ) ∀i ∈ [1..n], termi ∈ T (Σ, ∅)

c(1) d(2) g(3)

INST_TERM(term1 ) → hterm01 , mark1 i .. .

d(4)

INST_TERM(termn ) → hterm0n , markn i

d(5)

∀term ∈ T (Σ, ∅), ms0 (term) = Σtermi s.t. term0i =term ms(termi ) ADD(mark1 , . . . , markn ) → markT otal INST_MS(ms) → hms0 , markT otali

c(6) c(7)

Remarks: (1) (2) Each multiset has a finite set of terms whose cardinality is not null. We build a list with these terms. Notice that the order in which we consider these terms does not change the result. (3) All the terms in the multiset must be closed terms. (4) -(5) Instantiate all the terms in the multiset that have non-null cardinality, and keep the resulting markings. (6) The result is a multiset ms0 , which corresponds to ms where the instance creation terms have been replaced by adequate instance identifiers. We consider the sum of the cardinalities of all the terms that would give the same result after their instantiation. (7) Add the markings obtained from all the terms. Note that the ADD operation ensures that the instances that were created in all the terms have different identifiers. The following structure for which we must define the instantiation is the places markings. A place marking was defined in Def. 4.5 as a function that associates each place in a Petri net with a multiset. To instantiate this place marking, we simply instantiate each multiset and replace it in the place marking


53/58

with the instantiated version. This is formally defined in Inference 5.31. Inference rule 5.31: Instantiation of a place marking

INST_PM

pm ∈ mark(Σ, ∅, P) P = (p1 , . . . , pn )

d(1) d(2)

INST_MS(pm(p1 )) → hms01 , mark1 i .. .

d(3)

INST_MS(pm(pn )) → hms0n , markn i

d(4)

pm0 ∈ mark(Σ, ∅, P) ∀pi ∈ P, pm0 (p) = ms0i ADD(mark1 , . . . , markn ) → markT otal INST_PM(pm) → hpm0 , markT otali

d(5) d(6) c(7)

Remarks: (1) (2) pm must be a closed marking defined over the set of places P. (3) -(4) Instantiate all the multisets assigned to the places in P by the place marking pm. (5) (6) pm0 is the place marking pm where where marking of each place has been replaced with the instantiated version. (7) All the markings of the multisets are added with the operator ADD. This ensures that all the identifiers of all the instances created are different. There is one final structure for which we have to define the instantiation: the submodule sockets. This definition is a bit different from all the previous ones. Indeed, all the other instantiation operations take an element and return an element of the same type where the instance creation terms have been replaced by appropriate instance identifiers. The instantiation of a set of submodule sockets does not return a set of submodule sockets, it returns a hierarchical function in order to be able to define an instance hierarchy as in Def. 5.9. This substitution is defined in Inference 5.32. Inference rule 5.32: Instantiation of set of submodule sockets

INST_SOCKETS

Sockets = {hΞ1 , term1 i, . . . , hΞn , termn i}

d(1)

INST_TERM(term1 ) → hterm01 , mark1 i .. .

d(2)

INST_TERM(termn ) → hterm0n , markn i

d(3)

∀socketi ∈ S ockets, subs(socketi ) = term0i ADD(mark1 , . . . , markn ) → markT otal INST_SOCKETS(Sockets) → hsubs, markT otali

d(4) c(5)

Remarks: (1) Sockets is a set of submodule sockets, as defined in Def. 4.11. (2) -(3) Instantiate all the terms contained in the submodule sockets. (4) subs is a function that associates each submodule socket with its respective identifier.


5.11

54/58

Events firing and garbage collection

We have now defined the effects of all the possible events in a LLAMAS model. As mentioned previously, the successors markings are computed by applying these event effects to the current global marking. The result of this application is a new global marking. This application is formally defined in Inference 5.33. Inference rule 5.33: Application of the effect of an event

APPLY_EFFECT

gm = hIds, Marks, Hi eff = hIds, Pre, Post, NewGmi

d(1) d(2)

∀hidi , pmi i ∈ Pre, evalσ (Pre(idi )) ⊆ Marks(idi )

g(3)

Marks1 = {hidi , pmi i}, idi ∈ Ids ∀id ∈ Ids, Marks1(id) = Marks(id) − evalσ (Pre(id)) + evalσ (Post(id)) ADD(hIds, Marks1, Hi, NewGm) → gm2 APPLY_EFFECT(gm, eff) → gm2

c(4) c(5) c(6)

Remarks: (1) (2) gm is a global marking, eff is the effect of an event. (3) The preconditions of the effect must be met by the global marking. This corresponds to the usual enabling of the Petri nets transitions. (4) (5) Marks1 is the set of instance markings from gm where we have applied the pre and post-conditions from eff. This corresponds to the usual firing of the Petri nets transitions. (6) The new instances created by eff are added to the resulting marking.

As indicated previously, LLAMAS implements a particular garbage collection mechanism to get rid of the instances that are not referenced anymore in the model. In our garbage collection mechanism, all the instances that are not directly or indirectly referenced by the root instance are removed from the marking. This garbage collection is performed after executing every transaction, and between two events in a sequential composition. The formal definition of our garbage collection mechanism is to be found in Def. 5.34. It is a particular implementation of the mark and sweep garbage collection strategy. Definition 5.34: Garbage collection mechanism Let gm = hIds, Marks, Hi be a global marking, and let idroot ∈ Ob jIds be an identifier, called "root" identifier. The garbage collection mechanism identifies the instances that are iteratively referenced from the root, and deletes the ones that don’t meet this criterion. Formally, we define the set of "surviving" identifiers S urv ⊆ Ids as the least set such that: • idroot ∈ S urv • ∀id ∈ S urv, ∀socket ∈ S ocketsid , we have H(id)(socket) ∈ S urv • ∀id ∈ S urv, ∀p ∈ Pid , ∀t ∈ T (Σ, ∅) s.t. Marks(id)(p)(t) Ids s.t. id0 is a subterm of t, we have id0 ∈ S urv

>

0, ∀id0

∈

The first condition means that the root instance must always survive to the garbage collection. The second means that the submodules of a surviving instance must also survive, while the third means that the instances referenced by a surviving instance must also survive.


55/58

We note GCOLLECT(gm) = hS urv, Marks|S urv , H|S urv i the global marking where only the surviving identifies have been kept. At this point, we have defined how to compute the effect of all the events in a LLAMAS model, how to apply these effect in the global markings in order to compute their successors, and our garbage collection mechanism to clean to undesirable instances. These three elements allow us to finally define the firing of the events in a LLAMAS module. This firing is expressed as an operation FIRE, that takes a global marking and an event, and computes a result of the execution of this event in this global marking. This is formally defined in Inference 5.35. Inference rule 5.35: Firing events

FIRE

EFFECT(gm, event) → eff APPLY_EFFECT(gm, eff) → gmtemp GCOLLECT (gmtemp ) → gm0 FIRE(gm, event) → gm0

c(1) * c(2) c(3)

Remarks: (1) Compute the effect of the event on the global marking. (2) Apply this effect in order to obtain a new global marking. (3) Perform a garbage collection on this new global marking.

5.12

The transition relation of a LLAMAS model

Having defined the firing of the events in a LLAMAS model, we are almost ready to define its transition relation. The firing of the events in Inference 5.35 was defined for all the events in the model, including the active and passive transitions, the active and passive compositions and the other participants of the different classes. The transition relation of the system is computed only on the active events of the classes, i.e., the active transitions and the active compositions. This set of events is called the set of active events, defined in Def. 5.36. Definition 5.36: Set of active events The set of active events of an instance identifier is the set of active transitions and active compositions defined in the corresponding class. Formally, let S pec = hΣ, ClassNames, Ob jIds, X, veal, Impli. Let id ∈ Ob jIdsname be an instance identifier, where name ∈ ClassNames. Let Impl(name) = hname, Param, guard, net, Ξ, Sockets, Comp, Del be the class corresponding to name, where Comp = CompAct ∪ CompPass, net = hP, T, M0 and T = T act ∪ T pass. We define the set of active events of id, noted active(id), as the set of pairs hid, act(t1 , . . . , tn )i where: • act ∈ (T act ∪ CompAct)(s1 ,...,sn ) is either an active transition or an active composition of the class. Remember that both T act and CompAct where defined as S ∗ -sorted sets, and thus their union is also an S ∗ -sorted set. • (t1 , . . . , tn ) ∈ T (Σ, ∅)(s1 ,...,sn ) is a set of compatible effective parameters. The execution of the active events from a given marking gives us its set of successor markings. This set is defined in Def. 5.37.

6. CONCLUSION

56/58

Definition 5.37: Successors of a global marking Let gm be a global marking, let id be an instance identifier and let event be some active event from active(id). The set of successors of gm with event, noted successors(gm, hid, eventi) is defined as the set {gm0 s.t. FIRE(gm, hid, eventi) → gm0 } At this point, having defined the active events in a model, and how to fire them, we are finally able to define the transition relation of a LLAMAS model. This final definition is given in Def. 5.38. Definition 5.38: Transition relation Let model = hSpec, termroot , idroot i be a LLAMAS model, where Spec = hΣ, ClassNames, ObjIds, X, eval, Impli is a LLAMAS specification, termroot = new cname(t1 , . . . , tn ) ∈ T (Σ, ∅) is an instance creation term and idroot is the identifier of the instance root. Consider an instantiation INST_TERM(termroot ) → hidroot , mark0 i. With these elements, we will define an LTS. We note active(id) the set of active events of an identifier id ∈ Ob jIds, as defined in Def. 5.36. We define the sets of reachable states M, the sets of labels L and the transition function T r as the least sets such that: • mark0 ∈ M • ∀gm ∈ M where gm = hIds, Mark, Hi, ∀id ∈ Ids, ∀event ∈ active(ids), if FIRE(gm, hid, eventi) → gm0 then: – gm0 ∈ M – event ∈ T – hgm, event, gm0 i ∈ T r The triplet hM, T, T ri forms an LTS as defined in Def. 5.1.

6

Conclusion

We presented in this document a thorough definition of the formal concepts of the LLAMAS formalism. Both the syntax and semantics were completely defined, by means of a running example. As LLAMAS is a very expressive language, the definitions given in this document are quite complex. This complexity is itself a justification for the existence of our language. Indeed, LLAMAS is itself a modular formalism, and if we had a semantic platform on which we could base the definitions of the language, this definition would be certainly simplified. A reflexion on the theoretical aspects of the language and a comparison with existing languages are out of the scope of this document. We plan to discuss such issues in our close future work. In particular, we plan to compare LLAMAS to important formalisms such as Modular PNML [KP09], the M-nets [DKR03], the object Petri nets [Lak01] and CO-OPN [BBG01].

A. MEANING OF MATHEMATICAL SYMBOLS

A

57/58

Meaning of mathematical symbols

This section gave extensive and detailed definitions for the LLAMAS language. As is usual in definition of this magnitude, we defined many mathematical symbols that were used in various definitions. We will give in this section two tables that describe these symbols, along with the definition where they were introduced for the first time and a quick description of their meaning. The first table, table 1, shows the symbols that were defined in the section about the data types. The second table, table 2, shows the symbols that were defined in the context of the LLAMAS formalism itself. Symbol

Defined in

Meaning

[a..b] S σ

Def. 3.1 Def. 3.1 Def. 3.12

Σ T (Σ, X)

Def. 3.8 Def. 3.10

T (Σ, ∅) applyσ carrier(X) eval

Def. 3.10 Def. 3.12 Def. 3.2 Def. 3.14

new class Op S subst(Σ, X) subst_cl(Σ, X) T (Σ, X) T (Σ, ∅) X Xs

Def. 3.16 Def. 3.8 Def. 3.8 Def. 3.12 Def. 3.12 3.10 3.10 Def. 3.8 Def. 3.8 and Def. 3.2

The integer interval between naturals a and b the empty list of a set S a substitution, i.e., an function that assigns a value to the variables in a term a signature, i.e., a set of sorts, values and operations the set of terms (or expressions) that can be built with the symbols in Σ and the variables in X the set of closed terms that can be built with the symbols in Σ the application of a substitution σ the carrier set of an S -sorted set X en evaluation function, that returns a value for every term in T (Σ, X) the operation that allows to create instances of class a set of operations a set of sorts the set of all the possible substitutions on a set of variables X the set of closed substitutions on a set of variables X The set of terms of the signature Σ upon the set of variables X The set of closed terms of the signature Σ an S -sorted set of variables the elements of X that have the same sort s ∈ S

Table 1: List of symbols used in the data types definitions

Symbol

Defined in

Meaning

[] τ(p) Ξ Classes(Σ, ClassNames, X)

Def. 4.1 Def. 4.7 Def. 4.9 Def. 4.15

Comp

Def. 4.21 and Def. 4.15 Def. 4.24 and Def. 4.15 Def. 4.3 Def. 4.7 Def. 4.5 Def. 4.1

the empty multiset the sort of a place p a llamas module interface all the classes that can be defined with Σ, ClassNames and X a set of compositions

Del guard(Σ, X) M0 mark(Σ, X, P) mult(Σ, X)

an interface delegation the set of guards of Σ and X the initial marking of a P/A APN the set of markings of the places P on Σ and X the set of multisets of Σ and X

A. MEANING OF MATHEMATICAL SYMBOLS

mult(Σ, X) s

Def. 4.1

net P Param

Def. 4.7 Def. 4.7 Def. 4.6 and Def. 4.7 Def. 4.5 Def. 4.11 and Def. 4.15 Def. 4.27 Def. 4.6 and Def. 4.7

pm Sockets Spec T

58/58

the set of multisets where all the terms are of the same sort s a Parametric Activatable Algebraic Petri Net an S -sorted set of places a list of formal parameters a place marking a set of submodule sockets a LLAMAS specification a set of transition axioms

Table 2: List of symbols used in the syntactic definition of LLAMAS

Symbol

Defined in

Meaning

active(id)

Def. 5.36

ADD

Inference 5.11

APPLY_EFFECT

Inference 5.33

eff EFFECT

Marks NewGm Pre, Post

Def. 5.13 Inference 5.14 to Inference 5.19 Inference 5.20 to Inference 5.25 Def. 5.8 Inference 5.35 Def. 5.34 Def. 5.10 Def. 5.10 Inference 5.26 to Inference 5.32 Def. 5.10 Def. 5.13 Def. 5.13

The set of active events on a class with instance identifier id The addition of two global markings defined over disjoint set of identifiers The application of the effect of some event to a global marking The effect of some event The operation that computes the effect of an event on a global marking The operation that computes the effect of a composition on a global marking A place marking where all the places are empty The firing of some event on some global marking The garbage collection mechanism A global marking A set of instance hierarchies The instantiation mechanism on various structures

sub

Def. 5.9

EFFECT_COMP emptyPm FIRE GCOLLECT gm H INS T _ ∗ ∗∗

A set of instance markings A global marking containing a set of new instaces The pre and post conditions of an event, encoded as sets of instance markings A function that associates the submodule sockets of a class with instance identifiers

Table 3: List of symbols defined in the definition of the semantics of LLAMAS

REFERENCES

References [AKKB99] Egidio Astesiano, Hans-Joerg Kreowski, and Bernd Krieg-Brueckner, editors. Algebraic Foundations of Systems Specification. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 1999. [Aub79]

Raymond Aubin. Mechanizing structural induction part i: Formal system. Theor. Comput. Sci., 9:329–345, 1979.

[BBG01]

Olivier Biberstein, Didier Buchs, and Nicolas Guelfi. Object-Oriented Nets with Algebraic Specifications: The CO-OPN/2 Formalism. In G. Agha, F. De Cindio, and G. Rozenberg, editors, Advances in Petri Nets on Object-Orientation, LNCS, pages 70–127. Springer, 2001.

[CH94]

Søren Christensen and Damgaard Hansen. Coloured Petri Nets Extended with Channels for Synchronous Communication. In R. Valette, editor, Proceedings of the 15th International Conference on Applications and Theory of Petri Nets, volume 815, pages 159–178. SpringerVerlag, 1994.

[CTM05]

Jean-Michel Couvreur and Yann Thierry-Mieg. Hierarchical Decision Diagrams to Exploit Model Structure. In Farn Wang, editor, Formal Techniques for Networked and Distributed Systems - FORTE 2005, volume 3731 of Lecture Notes in Computer Science, pages 443–457. Springer Berlin / Heidelberg, 2005.

[DKR03]

Raymond Devillers, Hanna Klaudel, and Robert-C. Riemann. General parameterised refinement and recursion for the M-net calculus. Theoretical Computer Sc., 300:259–300, 2003.

[DW91]

A. J. J. Dick and P. Watson. Order-sorted term rewriting. Comput. J., 34(1):16–19, 1991.

[HJS91]

Peter Huber, Kurt Jensen, and Robert M. Shapiro. Hierarchies in coloured petri nets. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1990, volume 483 of Lecture Notes in Computer Science, pages 313–341. Springer Berlin Heidelberg, 1991.

[HO80]

Gerard Huet and Derek C. Oppen. Equations and rewrite rules: a survey. Technical report, Stanford, CA, USA, 1980.

[Hos12]

Steve Hostettler. High-Level Petri Net Model Checking, The Symbolic Way. Ph.D. dissertation, University of Geneva, 2012.

[KP09]

Ekkart Kindler and Laure Petrucci. Towards a Standard for Modular Petri Nets: A Formalisation. In Proceedings of the 30th International Conference on Applications and Theory of Petri Nets, PETRI NETS ’09, pages 43–62, Berlin, Heidelberg, 2009. Springer-Verlag.

[Lak95]

Charles Lakos. From coloured petri nets to object petri nets. In Giorgio De Michelis and Michel Diaz, editors, Application and Theory of Petri Nets, volume 935 of Lecture Notes in Computer Science, pages 278–297. Springer, 1995.

[Lak01]

Charles Lakos. Object Oriented Modeling with Object Petri Nets. In Concurrent ObjectOriented Programming and Petri Nets, pages 1–37, 2001.

[MB12]

Alexis Marechal and Didier Buchs. Modular extensions of Petri nets: a survey. Technical Report 218, University of Geneva, june 2012. Available at: http://smv.unige.ch/ technical-reports/pdfs/ModularitySurvey.pdf.

REFERENCES

[MM01]

Christoph Maier and Daniel Moldt. Object coloured petri nets - a formal technique for object oriented modelling. In Gul A. Agha, Fiorella De Cindio, and Grzegorz Rozenberg, editors, Advances in Petri Nets: Concurrent Object-Oriented Programming and Petri Nets, LNCS, pages 406–427. Springer, 2001.

[Pie02]

Benjamin C. Pierce. Types and programming languages. MIT Press, 2002.

[Rei91]

Wolfgang Reisig. Petri nets and algebraic specifications. Theor. Comput. Sci., 80:1–34, March 1991.

[SB94]

Christophe Sibertin-Blanc. Cooperative nets. In Proceedings of the 15th International Conference on Application and Theory of Petri Nets, pages 471–490, London, UK, 1994. Springer-Verlag.

[Ter03]

Terese. Term Rewriting Systems, volume 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.

[Val04]

Rüdiger Valk. Object Petri Nets – Using the Nets-within-Nets Paradigm. In Jörg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Advances in Petri Nets: Lectures on Concurrency and Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 819–848. Springer, Springer-Verlag, Berlin, Heidelberg, New York, 2004.

[Vau85]

Jacques Vautherin. Un modèle algébrique, basé sur les réseaux de Petri, pour l’étude des systèmes parallèles. PhD thesis, Université de Paris-Sud, LRI, 1985. Thèse de Doctorat d’Ingénieur.

SMV Technical Reports This report is in the series of SMV technical reports. The series editor is Didier Buchs (Didier. [email protected]). Any views or opinions contained in this report are solely those of the author, and do not necessarily represent those of SMV group, unless specifically stated and the sender is authorized to do so. You may order copies of the SMV technical reports from the corresponding author or the series editor. Most of the reports can also be found on the web pages of the SMV group (http://smv.unige.ch/).

Abstract LLAMAS is a modular Petri nets formalism that was defined to serve as a semantic platform to define modular extensions of Petri nets. Its objective is to be expressive enough to gather even the most complex modular features from the modular formalisms in the literature. This document gives the formal definition of the LLAMAS language. While this document is self contained, some prior knowledge of the basic features of the language is useful to understand the complex definitions we give here. Keywords: LLAMAS, Petri Nets, Modularity, Formal definition, Syntax, Semantics