General composition for Symmetric Net arc functions with applications L. Capra1 , M. De Pierro2 , and G. Franceschinis3 1 Dip. di Informatica, Università di Milano, Italy 2 Dip. di Informatica, Università di Torino, Italy 3 DISIT, Università del Piemonte Orientale, Alessandria, Italy Abstract. Structural analysis of High-Level Petri Nets is a powerful technique, but it is less supported than in PNs. A symbolic calculus for Symmetric Nets (SNs) has been developed and implemented, which allows one to check structural properties directly on SNs without unfold- ing: however it is limited to a particular form of composition, restricted to functions that map to sets. To complete the calculus for more general applications the ability to solve the composition of general SN arc ex- pressions in a symbolic way is required. In literature, a few papers show how to solve this operation for a restricted category of SN. In this pa- per, we formalize the algebraic composition of general SN bag-functions. Some applications are also discussed. 1 Introduction The possibility of checking some properties of PN models on their structure instead of (or before) generating their state space is a strong point in favour of the PN formalism. The extension of the structural analysis techniques to High Level Petri Nets (HLPNs), without resorting to unfolding, has been considered in the literature and some interesting results have been published [11,13], however the applicability of the proposed methods is often limited to particular classes of HLPNs and not completely supported by software tools. A contribution in this direction has been proposed in [6,4] for models repre- sented with the Symmetric Net (SN) formalism: it consists of a symbolic calculus operating on the arc expressions of the formalism, allowing to derive several in- teresting structural properties in a symbolic and parametric form; the software tool SNexpression [7] (http://www.di.unito.it/∼depierro/SNexpression/) im- plements the results developed so far in this direction. One limitation of such calculus concerned the composition operator, which could be applied only to the support of arc expressions (hence to functions mapping to sets): although this is sufficient for the computation of several symbolic structural relations (e.g. symbolic structural conflict or causal connection [5]) it is not enough e.g. for checking some invariant properties based on the definition of P and T-semiflows, or for applying model reduction by agglomeration of transitions, two techniques Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). 136 L. Capra, M. De Pierro, and G. Franceschinis that have been applied to concurrent programs verification [11]. This paper fills the gap by defining the theory allowing to symbolically apply the composition operator to general SN arc functions. Paper organization: Some definitions and notations are introduced in Sec. 1.1 and 1.2. Sec.s 2 and 3 introduce some useful definitions and properties, while in Sec. 4 we describe the steps to solve the general composition of SN functions. In Sec. 5 two example applications are illustrated. Sec. 6 concludes the paper and outlines directions for future work. 1.1 Generalized Bags: basic definition, notation and properties A (generalized) bag b over a domain A is a map b : A → Z. Bag[A] is the set of bags over A. Let a ∈ A and b ∈ Bag[A]: we write a ∈ b if and only if b(a) 6= 0. The set b = {a, a ∈ b} is the support of b. The bag with an empty support, is denoted ∅A or just ∅ if its domain is clear from the context. Bags b1 , b2 ∈ Bag[A] are disjoint if and only if b1 ∩b2 = ∅. A proper bag is a map b : A → N. The P set of proper bags over A is denoted Bag + [A]. The size of b ∈ Bag + [A], |b|, is a b(a). Bag bPis type-set if ∀a ∈ b b(a) = 1. A bag b 6= ∅ may be represented as a formal sum a∈A b(a).a. Let b1 , b2 ∈ Bag[A], k ∈ Z. The scalar product k · b1 and the sum (diff) b1 ± b2 are operations in Bag[A] defined as (k · b1 )(a) = b1 (a) · k and b1 ± b2 (a) = b1 (a) ± b2 (a), ∀a ∈ A. Operator + is associative, − is associative on Bag[A], not on Bag + [A], + is commutative. ∅ is the neutral element for +,−. The Cartesian product is defined as follows. Let b1 ∈ Bag[A], b2 ∈ Bag[B]: b1 ×b2 ∈ Bag[A × B] is b1 ×b2 (ha, bi) = b1 (a)·b2 (b), ∀a ∈ A, b ∈ B. The notation hb1 , b2 , . . .i is used in place of b1 × b2 × . . .. The Cartesian product is associative and may be distributed over inner +, −: h. . . , b1 op b2 , . . .i, op ∈ {+, −} = h. . . , b1 , . . .i op h. . . , b2 , . . .i. Finally, h. . . , k · b1 , . . .i = k · h. . . , b1 , . . .i. Generalized bags allow to distribute composition over sum or difference: in our context it simplifies the symbolic treatment of general composition. 1.2 A brief introduction to Symmetric Nets Note: GreatSPN GUI syntax Cij and Xij ++ correspond to Si,j and !Xij , respectively. Fig. 1. A SN example: Producers and Consumers Composition of SN arc functions 137 The SN formalism belongs to the HLPN class: places and transitions are associated with a color domain C(.) expressing the possible colors of tokens and of the transition instances. Arcs are annotated by expressions, representing functions from C(t) to multisets Bag + [C(p)]; W − (p, t) and W + (p, t) denote t input and output arc expressions. The structure of a color annotation is based on the definition of color classes (finite not empty sets), which may be parti- tioned into (static) subclasses or be circularly ordered, and on a restricted set of basic functions: Si , Si,k , Xi , !Xi namely diffusion/synchronization (on class Ci or subclass Ci,k ), projection Xij and successor !Xij (only for ordered classes). Color domains are defined as Cartesian products of n classes, where classes may be repeated. The arc expressions are weighted sums of tuples (Cartesian prod- uct) of basic functions (see Def. 4). The SN in Fig.1, represents a classical inter process communication example: producer and consumer processes communi- cating through a buffer (FIFO queue). There are two color classes, C1 (circu- larly ordered, representing the position of messages in the buffer) and C2 (id of producers/consumers), partitioned into two subclasses C21 , C22 . The places color domains are C2 , C1 , C1 × C2 (tokens are tuples of one or two elements); some places and one transition in this net have neutral color (as in PNs, e.g. place empty and transition ProduceBurst). The transitions have color domain C2 , C1 × C2 , C1 × C22 , depending on the projection symbols appearing on their arcs; transition Get has a guard : a predicate restricting the allowed color instances. Arc expressions in Fig.1 are quite simple: hX21 i, h!X11 i, hX11 , X22 i, hS2,2 i. A guard is a boolean expression whose terms can be either (Xij = Xik )/(!Xij = Xik ) or Xij ∈ Ci,k . An example of transition instance is Get(pos1, pc1, pc2): it satis- fies the guard (the two colors pc2, pc3 ∈ C2 belong to the same subclass C22 ), and the projection X11 (pos1, pc2, pc3) = pos1, while X12 (pos1, pc2, pc3) = pc2, X22 (pos1, pc2, pc3) = pc3, finally !X11 (pos1, pc2, pc3) = pos2. A more formal defi- nition of the SN arc expressions is deferred to Def. 4. Produce burst has only one instance since the functions hS22 i on its arcs are constant, mapping on C22 . An incidence matrix can be derived from the SN structure: Definition 1 (Incidence Matrix). The incidence matrix C of a HLPN model N is a P × T matrix of functions: C[p, t] = W + (p, t) − W − (p, t). If a transition instance t(c) enabled in marking mi fires, the corresponding state change can be defined in terms of the incidence matrix as: mj = mi + C[., t](c). Among the structural analysis techniques that can be applied to SN models those based on the definition of P and T-semiflows allow to check interesting invariant properties of the model. The general composition proposed in this paper enables such possibility by allowing to compose the functions in C with T or P-indexed vectors of functions to check if they are semiflows, as discussed in Sec. 5. 2 Bag-expressions: general properties of composition Operators op ∈ {+, −} on functions mapping to Bags are defined as follows, in terms of Bag-operations. Let f, h : A → Bag[D], op ∈ {+, −}: (f op h)(a) = 138 L. Capra, M. De Pierro, and G. Franceschinis f (a) op h(a), (k · f )(a) = k · f (a), ∀a ∈ A. The constant function mapping to the null bag is denoted A,D (or just ). Let {fi : A → Bag[Di ]} be a family of functions: the function-tuple hf1 , f2 , . . .i (or ⊗i fi ), is a map A → Bag[D1 × D2 × . . .]: hf1 , f2 , . . .i(a) = hf1 (a), f2 (a), . . .i. The properties of operations on bags, as well as the type-set notion, apply to bag-functions by considering all function arguments. We call any expression built of bag-functions a bag-expression. Definition 2 (composition). Let f : A → Bag[D], h : C → Bag[A]. Then f ◦ h : C → Bag[D] is f ◦ h(c) = f ∗ (h(c)), ∀c ∈P C, where f ∗ : Bag[A] → Bag[D] ∗ is the linear extension of f defined as f (b) = a∈A b(a) · f (a), ∀b ∈ Bag[A]. We shall use the same symbol for a function and its linear extension. When a function takes a bag as an argument we implicitly refer to its linear extension. The possibility to distribute composition over a difference or sum during the symbolic calculus, thanks to generalized bags, is very helpful because a complex composition may be reduced to an algebraic sum of simpler ones. Bag-expressions may be prefixed by filters and suffixed by guards, both ex- pressed as predicates. A [true] guard/filter is usually omitted. Let p : A → {true, f alse}. A filter or guard [p] is a function A → Bag[A] such that [p](a) = 1 ∗ a if p(a) = true, [p](a) = ∅ otherwise. Let f : A → Bag[D], and p0 be a predi- cate on D. The expressions f [p] and [p0 ]f stand for f ◦[p] and [p0 ]◦f , respectively. The following definition characterizes an important class of functions. Definition 3 (constant-size function). f : A → Bag + [D] is constant-size iff ∃n ∈ N+ such that ∀a ∈ A f (a) 6= ∅ ⇒ |f (a)| = n. Hereafter, with f constant-size we mean f ≡ f 0 [p], with f 0 [p] =  iff p = f alse. The following two general properties of composition concern constant and constant-size functions. Property 1 (composition of a constant and a constant-size function). Let f : B → Bag[D] be a constant function so defined: f (b) = d, ∀b ∈ B. And let h[g] : A → Bag[B] be a n constant-size function, where h[g](a) = ∅ iff g(a) = f alse. Then, the composition f ◦ h[g] is defined as follows: ∀a ∈ A, f ◦ h[g] = n · f 0 [g], where f 0 [g] : A → Bag[D] is such that ∀a ∈ A, g(a) = true ⇒ f 0 (a) = d. Property 2 (composition of a tuple including a constant). Let f 0 be a constant function. Then hf, f 0 i ◦ h = hf ◦ h, f 0 i. Since f and f 0 might be tuples in turn, Property 2 applies (up to a permutation of tuple positions) to any T ◦ h, where T := hf1 , . . . , fm i contains some constant components and others non-constant. We may thus reduce such a composition to T 0 ◦ h, where T 0 is built of all and only the non-constant components fi of T . In the sequel, we focus on this case. Composition of SN arc functions 139 3 A language for composition of SN functions Let us anticipate the main result presented in this paper by introducing the language used to calculate and express the composition of SN functions. Definition 4 (Language Lc ). Let - D = C1e1 × C2e2 × ... × Cnen , e∗ ∈ N, be any color domain, i.e., a Cartesian product nof colour classes ( ei = 0 means that o Ci doesn’t occur on D). j s j - Bi = Xi , Si , Si,k , ! Xi : D → Bag[Ci ] , i : 1, . . . , n, j : 1, . . . , ei , k : D 1, . . . , ||Ci ||, s ∈ Z; be the set of elementary functions, where !s denotes the s-th mod|Ci | successor on Ci (!s Xij ≡ !s ◦ Xij , !0 = id) 4 . 0 - Tj : D P → Bag[D ], Tj = hf1 , . . . flD i, and ∀r : 1, . . . , l, fr : D → Bag[Ci ], fr = m βm · hm , βm ∈ Z, hm ∈ Bi ; fr is said a class-function. - gj0 and gj be SN predicates on D0 and D, respectively, such that all class functions appearing in Tj [gj ] map to proper bags when gj is true. n X o Lc = E : D → Bag[D0 ], E = λj [gj0 ]Tj [gj ], ∀D, D0 , λj ∈ Z j Any class-function fr has as implicit guard: the guard of the tuple it belongs to. Theorem 1. Lc is closed under composition. The properties and lemmas presented in the rest of the paper justify the claim above5 . Before that, let us point out a few interesting facts about Lc . Lc includes SN arc-functions, where scalars are such that they map to Bag + [D0 ]. The possibility of prefixing function-tuples with filters makes Lc slightly more ex- pressive than the language of SN arc-functions, and has recently been included in the GreatSPN GUI. With respect to the language (L) of SN structural relations defined in [4,5] and implemented in SNexpression [7] the main difference is that class-functions belong to SN legacy: Si − Xij is a difference between elementary functions (often treated as an idiom), not a new symbol; the intersection opera- tor (though helpful) is not part of the language; scalars are in Z; class-functions and, consequently, function-tuples are themselves bag-expressions, whereas both in L and the new GreatSPN GUI [2] they are set-expressions. As long as we re- strict to expressions mapping to proper bags, however, L and Lc are equivalent. We use Lc for the sake of convenience/efficiency during the symbolic calculus. The next important properties of Lc directly follow from the definition of Lc , the Cartesian product and filter/guard properties, and the basic predicate reduc- tions listed in [8], Appendix A.2; these properties ensure that a few assumptions, prerequisites for the application of the lemmas presented in next section, can al- ways be met, possibly after the transformation of the involved expressions into equivalent ones satisfying such assumptions. The proof of all relevant properties and lemmas of this paper are reported in [8], Appendix A.1. 4 symbols !s Xij , with s 6= 0, and Si,k are mutually exclusive because we assume a color class is either partitioned or circularly ordered. 5 showing the closure of Lc under all the other operations on bag-expression (sum, difference, intersection, transpose), though much simpler, is not the focus here. 140 L. Capra, M. De Pierro, and G. Franceschinis Property 3 (conjunctive form equivalence). Any E ∈ Lc can be rewritten into E 0 ∈ Lc , E 0 ≡ E, in which the predicates of filters/guards are conjunctive forms exclusively composed of (in)equality/membership clauses. Property 4 (type-set equivalence). Any E ∈ Lc can be rewritten into E 0 ∈ Lc , E 0 ≡ E, in which class-functions (therefore, function-tuples) are type-set. Property 5 (constant-size function). Any class-function fr is constant-size when considering its implicit guard. |fr | is the weighted algebraic sum of sizes of el- ementary terms of fr . A function-tuple not prefixed by a filter is constant-size. Its size is the product of sizes of tuple’s components. For instance, |(S1 − X11 − X12 )|, with the implicit guard X11 6= X12 , is equal to |C1 | − 2. This expression is also type-set. A function-tuple prefixed by a filter may not be constant-size. An example is [X11 = X12 ]hS1 − X12 , S1 − X11 i: the size of this function-tuple depends on whether the 1st and 2nd element of a color-tuple argument are the same or not, it is |C| − 1 when applied to hc, ci and |C| − 2 when applied to hc, c0 i, c 6= c0 . Observe that the projection symbols appearing in the filter refer to the elements of the tuple (X1j is the j-th element of class C1 in the tuple), and should not be confused with the projection symbols appearing within the tuple or the guard. Property 6 (constant-size equivalence). Any E ∈ Lc can be rewritten into E 0 ∈ Lc , E 0 ≡ E, uniquely composed of constant-size terms. Thus, if needed, we can transform any expression into an equivalent sum of constant-size (and/or type-set) terms. We will return to this in Section 4.1. When calculating a Cartesian product, we have to take care of possible filters. Since we consider domains ordered by color, we only have to deal with two cases. Property 7 (Lc tuple Cartesian product with filters adaptation). Let F1 , F2 ∈ Lc , F1 : D → D0 , F1 = [g1 ]T1 ; F2 : D → D00 , F2 = [g2 ]T2 , such that D0 , D00 are either a) disjoint or b) D0 = Cim , D00 = Cin , n, m ∈ N+ . Then hF1 , F2 i = [g1 ∧ g2 ∗ ]hT1 , T2 i, where g2 ∗ = g2 in case a), g2 ∗ is obtained by replacing each Xij in g2 with Xij+m in case b). All results we are presenting hold modulo a permutation of tuple elements. 3.1 Conventions/notations used in the sequel Lower-case letters f, g, h, p denote class-functions and predicates, if enclosed be- tween angular and square brackets, respectively, otherwise represent any bag- expression (like in Section 2). Upper case F denotes any expression in Lc whereas T any (guarded) function-tuple in Lc . V ar(f ) denotes the set {Xji } of variables (projections) appearing in f : if f = [g]f 0 [g 0 ] then V ar(f ) = V ar(f 0 ) ∪ V ar(g 0 ). Let X be a non-empty set of typed variables: f (X) denotes a function such that V ar(f ) = X. We may list all function variables, e.g., f (Xij , Xhw ) meaning that V ar(f ) = {Xij , Xhw }. The subset X i ⊆ X holds the class-Ci variables. Composition of SN arc functions 141 Index restriction r Let D: C1e1 ...×Cnen , f = f (X) : D → Bag[D0 ], and e0j = |X j | e0 e0 (by the way, e0j ≤ ej ). The index restriction of f is a function f r : C1 1 ... × Cnn → Bag[D0 ], obtained from f by replacing symbols in Xji ∈ X j , in superscript order, e0 with Xj1 , . . . , Xj j , for each j, e0j < ej . For example, let T = hX11 + 2X13 , X13 , X22 i: C1 3 × C2 2 → C1 2 × C2 , then T = hX11 + 2X12 , X12 , X21 i : C1 2 × C2 → C1 2 × C2 . r Let X be a set {Xji }, Xji : D → Cj . Domain projection Π By convenience, we assume X ordered, first by class index then by superscript. We say the tuple ΠX,D : D → D0 = ⊗X i ∈X Xji projection j of D (on D0 ) induced by X. D is omitted when clear from the context. Projection image X Let T 0 = hh1 , . . . , hm i with codomain D. The image of X on T 0 is the subtuple TX 0 = ⊗i:∃X i ∈X hi , with the same domain as T 0 . We denote j by T¬X the residual sub-tuple of T 0 . 0 4 Composing Lc expressions Let T : D → Bag[D0 ], T 0 : D00 → Bag[D], D = C1e1 ... × Cnen , X = V ar(T ) and V ar(T ) 6= ∅. Tuple T may have a guard, i.e., T = hf1 , . . . , fn i[g]. Solving T ◦ T 0 means being able to rewrite this expression into F ∈ Lc . The algorithm to solve composition operates top-down. Each step is described in detail in this section. We proceed by making assumptions more and more stringent on T, T 0 , until we get a base form. Figure 2 outlines the main steps of the composition procedure on an exam- ple. At each step some rewriting rule is applied, possibly involving a sub-term (highlighted using under-braces): it is described in the legend along with the reference(s) to the corresponding lemma(s). We hereafter assume to have preliminarily operated all generic reductions described in Sec.2 (see e.g. the first step in the example of Fig. 2), thus we let T be hf1 , . . . , fn i[g], where ∀i V ar(fi ) 6= ∅, and T 0 = hh1 , . . . , hm i. Property 8. T = T r ◦ ΠX . A first basic result says that we can solve T ◦ T 0 by considering T r and the image of V ar(T ) on T 0 . 0 Lemma 1. Let T = T (X) and TX 6= T 0 . If T¬X 0 is of constant-size k, then: T ◦ T 0 [g 0 ] = k · T r ◦ TX 0 [g 0 ] Lemma 1 is applied twice in Fig. 2; follows a third example (|2S1 −X12 | = 2|C1 |−1): hX11 , X11 , S1 −X13 i◦hS1 , 2S1 −X11 , S1,1 +X12 i = (2|C1 |−1)·hX11 , X11 , S1 −X12 i◦hS1 , S1,1 +X12 i Based on Lemma 1 (and Property 6), we focus on tuple compositions where the image of left tuple’s variables coincides with the entire right tuple. A second basic result allows one to distribute a composition over the inde- pendent parts of the left operand (up to a permutation of tuple elements). 142 L. Capra, M. De Pierro, and G. Franceschinis 1 2 3 4 5 6 8 7 9 10 11 12 composition's result rule short description reference(s) 1 constant pulled-out of the left tuple Property 2 2,8 left tuple restriction and projection on the right tuple Lemma 1 3,6 distribution of composition on independent left sub-tuples Lemma 2 4 reduction (move) of a membership clause of g see [8], Appendix A.2 5 distribution property, reduction to a simple tuple-prefix Claim 1, Def. 5 7 elimination of an in-between guard built of inequalities Corollary 2, Lemma 5 9 distribution property and composition of a left constant Property 1 10 elementary composition Sect. 4.1 (table) 11, 12 basic composition (variable repetitions on the left tuple) Property 14 Fig. 2. A complete composition example (C1 is a partitioned class, C2 is ordered). Composition of SN arc functions 143 Lemma 2. 0 Let T = hF1 (X 1 ), . . . , Fh (X h )i ∧ ∀i, j, i 6= j, X i ∩ X j = ∅, ∧TX = T 0. T ◦ T 0 = hF1 r ◦ TX 0 1 0 , . . . , Fh r ◦ TX i h In other words, one can separately compose independent sub-tuples of T with their images on T 0 , whatever form they have. As a consequence, due to color independence, one can partition T (and T 0 ) in sub-tuples based on color-classes. 0 We therefore focus on function-tuples Cie → Cie and hereafter omit class index in basic functions: X j replaces Xij , Sj replaces Si,j , S replaces Si . We assume that monochromatic tuples do not include independent sub-tuples. Lemma 2 exploits a nice property of linear extension of Cartesian product of bag-functions by which, if an argument is in turn a product of bags, it is possible to evaluate the product-function in a modular way. In Fig. 2 this Lemma is applied twice; follows another non-trivial example: hX 1 , X 3 , S − X 2 , X 2 i[X 1 6= X 3 ∧ X 2 6= X 4 ] ◦ hS, 2S − X11 , S, S1 + 2X2 i = Lem.2 hhX 1 , X 3 i[X 1 6= X 3 ], hS − X 2 , X 2 i[X 2 6= X 4 ]i ◦ hS, 2S − X 1 , S, S1 + 2X2 i = 1 2 1 2 1 1 1 2 1 hhX , X i[X 6= X ] ◦ hS, Si, hS − X , X i[X 6= X ] ◦ h2S − X , S1 + 2X2 ii The two compositions that we ended up with are representatives of the base cases of tuple composition we have to solve. 4.1 Tuple composition’s base cases We can identify a few base cases of function-tuple composition as a result of Lemma 2 application. One in which the left-hand tuple is a one-variable function and the right tuple is a singleton. The others in which there is an infix predicate (guard/filter) that cannot be eliminated. The presence of an infix predicate com- plicates the solution of a composition. Based on properties of filters and filter reduction rules we may reduce such expressions to a particular form. The follow- ing statements assume that the right operand of a composition (T 0 ) is possibly followed by a guard. Definition 5 (tuple prefix/composition simple form(s)). Let T 0 = hh1 , . . . , hm i. A tuple-prefix [g]T 0 is simple if and only if 6= 1. g is a conjunction of (in)equalities, such that for each clause (X i =!s X j ) in g: hi is type-set, |hi | > 1, and hi =!s hj 2. let g= ∪ g6= be the partition of g in equalities and inequalities (a) if g6= 6= ∅, each partition g1 ∪ g2 of g6= is such that V ar(g1 ) ∩ V ar(g2 ) 6= ∅ (b) if g= 6= ∅, then g= may be partitioned in g= i w , . . . , g= , w ∈ N+ , such that i j ∀i, j, i 6= j, V ar(g= ) ∩ V ar(g= ) = ∅ i i ∀g= V ar(g= ) ∩ V ar(g6= ) = {X j } T [g] ◦ T 0 is a simple form of composition if and only if [g] ◦ T ’ is a simple i tuple-prefix and ∀i |V ar(g= ) ∩ V ar(T )| ≤ 1. 144 L. Capra, M. De Pierro, and G. Franceschinis Claim 1 We can rewrite any composition T [g] ◦ T 0 that cannot be decomposed according to Lemma 2 in terms matching Definition 5 (see [8], Appendix A.2) In other words, if required we may assume that infix predicates are made of (in)equalities between projections which point to equal (modulo-successor) type- set class-functions of T 0 of size > 1. Equalities define equivalence classes of projections, one representative of each class must appear in inequalities, and at most one occur on T . In Fig. 2 steps 4 and 5 lead to a form satisfying Def.5; follows another example: Let (|C2 | > 1): hS2 − X 3 , X 1 i[X 1 6= X 2 ∧ X 1 ∈ C2 ∧ X 1 = X 3 ] ◦ hS, S, S + X 1 i → hS2 − X 1 , X 1 i[X 1 6= X 2 ∧ X 1 = X 3 ] ◦ hS2 , S2 , S2 i+ hS2 − X 1 , X 1 i[X 1 = X 3 ] ◦ hS2 , S − S2 , S2 i + hS2 − X 1 , X 1 i ◦ hX 1 , S − X 1 , X 1 i[X 1 ∈ C2 ] Tuples prefixed by a filter matching Definition 5 have an important property. Property 9. A simple tuple-prefix [p]T : D → Bag[D0 ] is constant-size. Four base cases have to be considered, they are listed below. 1. T (X 1 ) ◦ hhi 2. T (X)[g] ◦ T 0 , with |X| > 1 and X ⊇ V ar(g) 3. T (X)[g] ◦ T 0 , with X ⊂ V ar(g) 4. T [g] ◦ T 0 , with V ar(T ) ∩ V ar(g) = ∅ Case 1: T (X 1 ) ◦ hhi In absence of infix predicates, we can always reduce to one such form due to the distribution property of sum/diff. For example: hS −X 1 +2X 2 , X 2 i◦hh1 , h2 i = h(S −X 1 )◦hh1 i, X 1 ◦hh2 ii+2|h1 |·hX 1 , X 1 i◦hh2 i Case 1.a: |h| = 1; this is the simplest situation. Property 10. Let |h| = 1. Then F (X 1 ) ◦ hhi is obtained by replacing each occur- rence of symbol X 1 in F with h. It directly follows from the definition of composition. For example, hS + X 1 , X 1 i ◦ hh2 i, |h2 | = 1 −→ hS + h2 , h2 i. Case 1.b: |h| > 1. The basic compositions are summarized in the following table (omitting tuple notation),the first one is applied in Fig. 2, step 10: Basic composition rules and some useful identities X 1 ◦ h = h !s X 1 ◦ h =!s h S − X 1 ◦ h = |h| · S − h S−!r X 1 ◦ h = |h| · S−!r h !r S = S !s !r X i =!s+r X i !r (h1 ± h2 ) =!r h1 ±!r h2 If T = hf1 (X 1 )i the above basic rules (and property 2) are enough. For example, letting |C1 | = 3: h2S − X 1 −!X 1 i ◦ hS − X 2 i → h4S − S + X 2 − S+!X 2 i ≡ h2S + X 2 +!X 2 i. Composition of SN arc functions 145 Repetition of a projection in T Let T = hf1 (X 1 ), . . . , fm (X 1 )i, where (without loss of generality due to Property 4) fi (X 1 ) =!si X 1 , ∀i (symbol !s X i from now on denotes a projection possibly prefixed by the s-th successor). We consider first an unordered color class, then we generalize. Property 11. Let h be type-set. hX 1 , . . . , X 1 i ◦hhi = [ i:2...m X 1 = X i ] hh, . . . , hi V | {z } | {z } m>1 m 6 Here are some non-elementary, type-set class-functions : S − X 1 ; S − X 1 − X 2 [X 1 6= X 2 ]; Si − X 1 [X 1 ∈ Ci ]; S − X 1 −!X 1 . We can extend the above outcome to any color class. Property 12. Let h be type-set. ^ h!r1 X 1 , . . . , !rm X 1 i ◦ hhi = [ X 1 = !(r1 −ri ) X i ]h!r1 h, . . . , !rm hi i:2...m As an example: h!X 1 , X 1 , !X 1 i ◦ hS − X 2 i = [X 1 =!X 2 ∧ X 1 = X 3 ]hS−!X 2 , S − X 2 , S−!X 2 i. In some cases may treat the idiom S − X 1 as a single function for convenience. Here are two situations that are more efficiently processed applying the following properties, although they could be solved applying the previous rules. Without loss of generality, in both cases S − X 1 is the last element of T . Property 13. Let h be a type-set function. V hX 1 , . . . , X 1 , S − X 1 i ◦hhi = [X 1 6= X m i:2...m−1 X 1 = X i ] hh, . . . , h, Si | {z } | {z } m m 1 If there are no repetitions of X then h may be any function. Property 14. hX 1 , S − X 1 i ◦ hhi = [X 1 6= X 2 ]hh, Si Case 2: T(X)[g] ◦ T0 , |X| > 1, X ⊇ Var(g) In this and in the next case we may assume, without loss of generality, that g is composed of (in-)equalities and T = hf1 , . . . , fm i, where fi =!si X j , ∀i. Consider, for example: hX 2 , !X 2 , X 3 , !2 X 1 i[X 1 6= X 3 ∧ X 1 6= !X 2 ] ◦ hh1 , h2 , h3 i This expression doesn’t match Lc . However, we can transform the guard in between into a filter prefixing the left tuple through an index substitution, i.e., an injective map φ : V ar(T ) → {1 . . . m} associating each X i to the position of any of its occurrences in T . The picture below illustrates the idea. hX 2 , !X 2 , X 3 , !2 X 1 i[X 1 6= X 3 ∧ X 1 6= !X 2 ]. The following rule formalizes the move of a clause of a guard g to a filter 6= 6= prefixing T (X i = !k X j ≡ X j = !−k X i ). 6 if b is any bag, hX 1 , . . . , X 1 i(b) is obtained from [ i:2...m X 1 = X i ]hb, . . . , bi by V th applying the m root to multiplicities of bag elements 146 L. Capra, M. De Pierro, and G. Franceschinis Lemma 3 (transforming the infix predicate into a filter). Let φ(i), φ(j) be any two occurrences of variables X i , X j , i 6= j, in tuple T . φ(i) φ(j) 6= 6= h. . . , !r X i , . . . , !s X j , . . .i[X i = !k X j , . . .] −→ [X φ(i) = !k+r−s X φ(j) ]T [. . .] | {z } T Corollary 1. Let T [g], with T = hf1 , . . . , fm i and g be a set of (in)equalities. If ∀X i ∈ V ar(g) there is fj , fj =!s X i , then ∃p T [g] ≡ [p]T . Therefore, if V ar(T ) ⊇ V ar(g) the reiterated application of Lemma 3 eventually removes the infix guard from T (X)[g] ◦ T 0 . Applying Lemma 3 to the last example,we can proceed with Lemma 2. Lem.3 −→ [X 4 6=!2 X 3 ∧ X 4 6= !2 X 2 ]hX 2 , !X 2 , X 3 , !2 X 1 i ◦ hh1 , h2 , h3 i Lem.2 −→ [X 4 6=!2 X 3 ∧ X 4 6= !2 X 2 ]hhX 1 , !X 1 i ◦ hh2 i, X 1 ◦ hh3 i, !2 X 1 ◦ hh1 ii Case 3: T (X)[g] ◦ T 0 , X ⊂ V ar(g) This situation is the most complex one. The reason is that we must project on X = V ar(T ) the application of the filter g on T 0 , in a symbolic way. We assume that g is no further reducible, the composition to solve matches Definition 5 and none of lemmas presented so far applies (in particular Lemma 1, thus TV0 ar(g) = T 0 ). 6= Let A ⊆ V ar(g): we say gA = {(X i =!r X j ) ∈ g|X i , X j ∈ A} the restriction of g to variables A. A first simplification comes from the fact that we may take out equalities of g. We recall that f r denotes the index-restriction of f . 0 Property 15. Let [g]T 0 meet Definition 5, g= 6= ∅, X = X ∪ V ar(g6= ). Then T (X)[g] ◦ T 0 = (T [g6= ])r ◦ TX 0 0 This nice property stems from the fact that (by Definition 5) T 0 components are equal (modulo successor) and in T only one symbol per equivalence class is used. Here are some examples of application of Property 15. For simplicity, in all the following examples X = {X 1 , . . . , X m } (T = T r ). P rop.15 1) hX 1 , S − X 1 i[X 1 = X 2 , X 1 = !X 3 ] ◦ hS−!X 2 , S−!X 2 , S − X 2 i −→ P rop.14 hX 1 , S − X 1 i ◦ hS−!X 2 i −→ [X 1 6= X 2 ]hS−!X 2 , Si P rop.15 2) hX 1 , !X 2 i[X 1 6= !X 2 , X 2 = X 3 ] ◦ hS−!X 2 , S − X 2 , S − X 2 i −→ Lem.3,Lem.2 hX 1 , !X 2 i[X 1 6= !X 2 ] ◦ hS−!X 2 , S − X 2 i −→ [X 1 6= X 2 ]hS−!X 2 , S−!X 2 i P rop.15 3) hX 2 , X 2 i[X 1 6= X 2 , X 2 6= X 4 , X 1 = X 3 ] ◦ hS1 , S1 , S1 , S1 i −→ (hX 2 , X 2 i[X 1 6= X 2 , X 2 6= X 4 ])r ◦ hS1 , S1 , S1 , S1 i{X 1 ,X 2 ,X 4 } ≡ hX 2 , X 2 i[X 1 6= X 2 , X 2 6= X 3 ] ◦ hS1 , S1 , S1 i (non-reducible with the available rules) Composition of SN arc functions 147 Main sub-case: g = g6= We may therefore assume that g is a non-empty set of inequalities and focus on ΠX ◦ [g]T 0 . In general, we figure out that it holds 0 ΠX ◦ [g]T 0 ⊆ [gX ]r TX (1) Equation 1 says that, disregarding bag multiplicity, the projection of [g]T 0 on V ar(T ) is included in the restriction of [g] to V ar(T ) which applies to the image of V ar(T ) on T 0 . It follows from our assumptions, by which: g ⇒ gX . In the sequel, we characterize particular forms [g]T 0 verifying ΠX ◦ [g]T 0 = k · [gX ]r TX 0 , k∈N (2) showing that (modulo some rewriting) we can always reduce our expression to such a form. An immediate corollary of (2) is: Corollary 2. Let T = T (X), X ⊂ V ar(g). If (2) holds and [g] ◦ T 0 is a simple tuple-prefix (Definition 5). Then: 0 T (X)[g] ◦ T 0 = k · T r [gX ]r ◦ TX 0 , where k = |[g|[g]T r 0 | 0 if |[gX ]r TX |= 6 0, otherwise X ] TX | k=0 Corollary 2 outlines that we bring a composition to a form where the variables of the left tuple are a super-set of those of the infix predicate. Consider this simple but interesting case where T [g] : C 3 → C 2 , T 0 : C → C 3 . hX 1 , X 2 i[X 1 6= X 3 ∧ X 2 6= X 3 ] ◦ hS − X 1 , S − X 1 S − X 1 i |C| > 2 T g T0 In this case condition (2) is not verified: Π{X 1 ,X 2 } ◦ [g]T 0 (c) turns out to be, for any c ∈ C, |C| > 2: X X (|C| − 2) ∗ hc0 , c0 i + (|C| − 3) ∗ hc0 , c00 i c0 ∈C,c0 6=c c0 ,c00 ∈C,c0 6=c,c00 6=c,c0 6=c00 The restriction of g[T 0 ] to X = {X 1 , X 2 } used on the right-hand side of (2), instead, is hS − X 1 , S − X 1 i (in this particular case, gX = {}). As the example suggests, we should distinguish (in g) the case X 1 = X 2 from the case X 1 6= X 2 . Since we are assuming that the requirements of Definition 5 are met, we may conveniently study [g]T 0 as a system of inequalities (in case of ordered classes, the successors are all expressed modulo-|C|) among V ar(g) variables, with the implicit constraints X i ∈ hi (c), ∀X i ∈ V ar(g), hi being the i-th component of T 0 . Thus, [g]T 0 (c) is a type-set bag which corresponds to the system’s solutions, while ΠX ◦ [g]T 0 (c) is a bag representing their projection on subset X. Due to the symmetry of g and to the fact that functions hi are equal (mod- ulo successor), we can abstract from both c and i and consider any hi as a (parametric) set of known size. We put some conditions on g to ensure that the projection of the inequality system’s solutions on X is the parametric multi-set consisting of k instances of 0 the solutions of the sub-system restricted to X, i.e., [gX ]r TX . 148 L. Capra, M. De Pierro, and G. Franceschinis We consider first an unordered color-class C. In that case, hi = h, ∀i, and we may represent g as an undirected simple graph whose vertices are V ar(g) and whose edges connect vertices corresponding to variables that are required to be different by a term of g. Abusing notation, we denote the same way g and the corresponding graph, leaving the context to disambiguate. Thus, we may interpret gX as a (proper) subgraph of g. A few basic results of graph-colouring theory turn out to be useful for our purposes (refer to [10] for all the details). Given a graph G = (VG , EG ), where VG is a non-empty finite set and EG a set of unordered pairs xy, x, y ∈ V (G), x 6= y, and λ ∈ N, we define a λ-colouring of G as a map ϕ : VG → {1, 2, . . . , λ} that assigns adjacent vertices of G different values. We are interested in the number of different λ-colourings of G, denoted P (G, λ). The minimum value of λ such that G admits a λ-colouring is the chromatic number of G, denoted χG . The value |V (G)| is the order of G. We say that G is empty if E(G) = ∅, complete (or clique) if any two vertices are adjacent. A clique of order n is denoted Kn . We use a few operations on graphs: let x, y be two vertices of G, G · xy, xy ∈ / E(G), is the graph obtained from G by merging x and y and leaving one occurrence of possible resulting multiple edges; G − xy, xy ∈ E(G), the graph obtained by removing edge xy; G + xy, xy ∈ / E(G), the graph obtained by adding edge xy. P (G, λ) can be expressed as a polynomial in λ, called chromatic polynomial of G. This is interesting, since it gives us the possibility to express a composition’s result in a parametric way. Computing χG is around O(2n ), and computing P (G, λ) is at least as complex. [10] shows, however, that for large classes of graphs you can compute P (G, λ) very efficiently, e.g., exploiting their modular structure. How to compute the chromatic polynomial is out of the scope of the paper, however, here are a few intuitive properties used in the sequel. – (Fundamental reduction theorem) let x, y be two non-adjacent vertices of G: P (G, λ) = P (G · xy, λ) + P (G + xy, λ). – Let G include Kr and G0 be obtained from G by adding a new vertex x which is (uniquely) linked to all vertices of Kr . Then P (G0 , λ) = P (G, λ)(λ − r) – Some known polynomials: P (Kr , λ) = λ(λ − 1) · · · (λ − r + 1); if G is an empty graph of order n, P (G, λ) = λn ; . . . Any solution of the inequality system [g]T 0 (g, from now on) corresponds in fact to a λ-colouring of g with λ = |h|, therefore, denoting with Sol(g, λ) the number of solutions of the inequality system, P (g, λ) = Sol(g, λ). Lemma 4. Let [g]T 0 be a simple tuple-prefix, X ⊂ V ar(g), and gX be a clique. P (g,λ) Then, equation (2) holds and (Corollary 2) k = P (K ,λ) if λ ≥ |X|, otherwise |X| k = 0, where λ = |hi |, for any hi in T 0 . It is sufficient to observe that for any two distinct λ-colourings of gX there are (obviously) the same number of λ-colourings of g that include them. Moreover, we know that χKr = r and χg ≥ χgX . We are always able to reduce a composition to the condition that meets Lemma 4 by linking non-adjacent vertices of gX . Two such vertices are two un- related variables X i , X j ∈ X, therefore we rewrite T ◦ [g][T 0 ] into the equivalent Composition of SN arc functions 149 sum T ◦[g ∧X i 6= X j ]T 0 +T ◦[g ∧X i = X j ]T 0 . Note that g ∧X i = X j , after sym- bol replacement and removal of redundant inequalities (according to Definition 5) exactly corresponds to g · X i X j . By recursively rewriting and applying variable substitutions accordingly in T we eventually get sub-compositions solvable with the lemmas above. Let us instantiate this simple procedure and Lemma 4 on the last example. hX 1 , X 2 i[X 1 6= X 3 ∧ X 2 6= X 3 ] ◦ hS − X 1 , S − X 1 S, −X 1 i λ = |C| − 1 (> 1) T g T0 ≡ hX , X i[X 6= X ∧ X 6= X ∧ X 6= X ] ◦ T 0 + hX 1 , X 1 i[X 1 6= X 3 ] ◦ T 0 1 2 1 3 2 3 1 2 ≡ hX 1 , X 2 i ◦ (λ − 2)[X 1 6= X 2 ]hS − X 1 , S − X 1 i + hX 1 , X 1 i ◦ (λ − 1)hS − X 1 i ≡ (λ − 2)[X 1 6= X 2 ]hS − X 1 , S − X 1 i + (λ − 1)[X 1 = X 2 ]hS − X 1 , S − X 1 i P (K3 ,λ) where λ − 2 = P (K2 ,λ) and λ − 1 = P (K2 ,λ) P (K1 ,λ) . Dealing with an ordered class C. What if predicate g of the filter prefixing tuple T 0 is defined on an ordered class? In theory, the situation is even simpler because we can always rewrite any inequality into a disjunction of equalities: for example, if |C| = 3: X 1 6=!X 2 ≡ X 1 =!2 X 2 ∨ X 1 = X 2 . So, by expanding T ◦ [g]T 0 accordingly we eventually get a solvable form. This approach, however, may be inefficient and is not parametric. Therefore, we slightly extend the technique based on graph-representation of g to ordered classes. The graph representing g now has as vertices the symbols Symb(g) = {!r X j } occurring in g and as edges, in addition to inequalities in g, those implied by them: for any two symbols !r X j , !s X j ∈ Symb(g), there is a corresponding edge in the graph7 . In this case, a λ-colouring of g doesn’t necessarily match a solution of the inequality system, i.e., P (g, λ) ≥ Sol(g, λ), Due to the circularity of C there are a number of equivalent representations for g. A first result concerns those cases where g may be expressed in a form such that |V ar(g)| = |Symb(g)|, i.e., for each variable there is one corresponding symbol. In this case the previous results, in particular Lemma 4, still hold. When |V ar(g)| < |Symb(g)| instead, an extension of Lemma 4 is needed. Lemma 5. Let [g]T 0 be a simple tuple-prefix and X ⊂ V ar(g). If a) for each X i ∈ V ar(g)\X any two inequalities between X and X i use the same sym- Sol(g,λ) bol !r X i and b) gX is a clique, then equation (2) holds and k = Sol(g if X ,λ) 0 Sol(gX , λ) > 0, otherwise k = 0, where λ = |hi |, for any hi in T . We can always rewrite any predicate g so that it meets condition a) of Lemma 5. Condition a) is redundant if |X| = 1. Observe that for computing Sol(g, λ), for any inequality graph g, we can use similar basic techniques as for the chromatic polynomial. See Fig. 2, step 7 and [8], Appendix A.3 for a few examples of application of the last two lemmas. 7 Let succmin and succmax be the smallest and largest successor index in the formula; we assume that succmax − succmin < |C|, so that for each two symbols !r X j , !s X i , and for each c, !r X j (c) 6=!s X j (c); as a consequence we may have consider different cases, depending on the size of C 150 L. Capra, M. De Pierro, and G. Franceschinis Case 4: T[g] ◦ T0 , Var(T) ∩ Var(g) = ∅. We may reduce this case to one solvable with Lemma 1. Indeed, we can express (modulo a tuple permutation) [g] ◦ T 0 as a Cartesian product h[g]r TV0 ar(g) , T¬V 0 0 ar(g) i, where TV ar(g) is the image 0 r 0 of g on T . If [g] TV ar(g) is simple we can directly use Lemma 1. For instance: hX 1 i[X 2 6= X 3 ] ◦ hS − X 1 , S, Si → hX 1 i ◦ hS − X 1 , [X 1 6= X 2 ]hS, Sii → λ(λ − 1) · hS − X 1 i (λ = |C|) 5 Applications This section presents two application examples: the symbolic verification of in- variants in SN models, and the reduction of nets by agglomeration of transitions, enabling more efficient qualitative analysis (as in behavior preserving reduc- tions [3,11]) and quantitative analysis (e.g. elimination of immediate transitions in Stochastic SN models, extending the technique defined for GSPNs in [1]). Verification of P and T-invariants. P and T-semiflows inducing invariant prop- erties in PNs have been introduced in mid 80s and extended to HLPN in 90s [13]. Algorithms to compute a generating family of P and T-semiflows of PN exist [9] and are implemented in several tools; they can be applied to the unfolding of an HLPN model, while the automatic derivation of high-level (symbolic) P or T- semiflows is still an open problem, unless restrictions are imposed on the HLPN formalism (as in [12]). Often the modeler is aware of which invariant properties should satisfy a given model, thus the ability to automatically check whether a P or T-indexed vector of functions is a P or T-semiflow is interesting. The symbolic calculus implemented in the SNexpression tool [7], extended with the composition presented in this paper, allows to implement such automatic check. Let us illustrate how this can be done on the example net in Fig. 1; for the sake of space only T-invariants are shown, while P-invariants are discussed in [8]. Definition 6 (T-semiflow of HLPN models). Let y be a T-indexed vector of functions with color domain C(y), y[t] : C(y) → Bag[C([t)], t ∈ T ; y is a T-semiflow if C ◦ y = nully . A T-semiflow defines a (parametric) set of transition instances; given a color c ∈ C(y) if all the transition instances in y(c) can fire (in any order) starting from marking m, they bring back the model to the same marking m. Where nully is a P-indexed vector of functions such that nully [p] is a constant function mapping any c ∈ C(y) into a constant empty Bag on C(p). In Table 1 two T-semiflows of the producers-consumers SN are listed. Their interpretation is quite simple8 : In order to reproduce a marking the pointers first and last should be increased by one |C1| times, hence the producers should produce |C1| items and put them into the buffer, and the consumers should get |C1| items from the buffer. In T1 the same producer fills completely the buffer and a consumer with the same id of the producer empties it (it represents |C2| invariants in the unfolded net). In T2 any combination of |C1| producers and |C1| consumers (satisfying the invariant guard g 0 ) is possible. The expressions 8 Initialization transition init cannot belong to any T-invariant, while additional in- variants involving ProduceBurst exist, but are not included for the sake of space. Composition of SN arc functions 151 Transition T1 T2 (Hp: |C1| = 4) (Domain) C2 C28 , C1 [g 0 ] 1 Produce (C2 ) |C1 |hX2 i hX2 i + hX23 i + hX25 i + hX27 i 1 1 P3 1 2i+1 Put (C1 , C2 ) hSC1 , X2 i i=0 h!i X1 , X2 i 2 1 1 P 3 1 2i+1 2(i+1) Get [g](C1 , C2 ) hSC1 , X2 , X2 i i=0 h!i X1 , X2 , X2 i End Process (C2 ) |C1 |hX21 i hX22 i + hX24 i + hX26 i + hX28 i W  2(i+1) p(k) = ki=0 2 2i+1 ∈ C2j ; g = p(0); g 0 = p(|C1 | − 1) V j=1 X2 ∈ C2j ∧ X2 Table 1. Two T-semiflows of the Producers-Consumers SN allowing Pto verify that vectors Tj correspond to parametric T-semiflows are: ∀p ∈ P, t∈T C[p, t] ◦ Tj [t] = C(p) ; the function Tj [t] has domain C(Ti ) and codomain C(t), so that the domains of the functions to be composed are coherent. Observe that T2 represents 625 T-invariants in the unfolded net when |C1 | = 4, |C21 | = 1 and |C22 | = 2. Let’s check whether the transitions in T1 produce a null change on all places. Producing: W + (Put,Producing) ◦ T 1[Put] - W − (Produce, Producing) ◦ T 1[Produce] = hX21 i◦|C1 |hX21 i−hX21 i◦|C1 |hX21 i = C1 ( the equations for Wait to insert, Wait to extract and Processing are very similar). buffer: W + (Put, buffer) ◦ T 1[Put] − W − (Get, buffer) ◦ T 1[Get] = hX11 , X21 i ◦ hSC1 , X21 i − hX11 , X21 i[g] ◦ hSC1 , X21 , X21 i = hSC1 , X21 i − hSC1 , X21 i = C1 ,C2 full: W + (Put, full) ◦ T 1[Put] − W − (Get, full) ◦ T 1[Get] = hSC• i ◦ hX11 , X21 i − hSC• i[g] ◦ hX11 , X21 , X21 i = C• (the equation for empty is very similar) first:W + (Get, first) ◦ T 1[Get] − W − (Get, first) ◦ T 1[Get] = h!X11 i[g] ◦ hSC1 , X21 , X21 i − hX11 i[g] ◦ hSC1 , X21 , X21 i = hSC1 i − hSC1 i = C1 (the equation for last is very similar) T2 has color domain C1 , C28 where 8 = 2|C1 |, completed by guard g 0 (see Table1); and similar formulae as for T1 apply to it, let us consider the expressions for just a few places to illustrate the type of composition to be solved. buffer: W + (Put, buffer) ◦ T 2[Put] − W − (Get, buffer) ◦ T 2[Get] = hX11 , X21 i ◦ (hX11 , X21 i[g 0 ] +h!X11 , X23 i[g 0 ] + h!2 X11 , X25 i[g 0 ] + h!3 X11 , X27 i[g 0 ])− (hX11 , X21 i[g] ◦ (hX11 , X21 , X22 i[g 0 ] + h!X11 , X23 , X24 i[g 0 ] + h!2 X11 , X25 , X26 i[g 0 ] + h!3 X11 , X27 , X28 i[g 0 ]) = C1 ,C2 Wait to insert: W + (Produce, Wait to insert) ◦ T 2[Produce] − W − (Put, Wait to insert) ◦ T 2[Put] = hX21 i◦(hX21 i+hX23 i+hX25 i+hX27 i)[g 0 ]− (hX21 i◦(hX11 , X21 i[g 0 ]+h!X11 , X23 i[g 0 ]+ h!2 X11 , X25 i[g 0 ] + h!3 X11 , X27 i[g 0 ]) = C2 Observe that in all cases where transition Get is involved we have an infix guard g whose terms check which static sublcass X21 and X22 belong to: it is easily handled both in T1 (where the involved elements of the right tuple are equal) and in T2 (where the T-semiflow guard g 0 implies that g is satisfied). Finally, note that depending on the actual binding of the T-psemiflow variables to colors, functions Tj [Produce] and Tj [End Process] map to a Bag + [C2 ] that may have coefficients greater than one. Hence the composition presented in this paper is required to verify the invariant. Reduction of transitions. Another application of multiset composition in coloured PN is structural reduction. For instance, in [11] a symbolic reduction technique (based on the capability to syntactically solve the composition) is applied to models used for software verification. To allow for a symbolic treatment, the authors propose Quasi-well formed Nets, a tight restriction of SNs. Moreover, 152 L. Capra, M. De Pierro, and G. Franceschinis C = {1, 2, 3} r:C C = {1, 2, 3} ordered r :C ⇥C r:C h1, 3i h1, 1i h1, 2i r :C ⇥C h1i hXi hX 1 , X 2 i t t h1, 3i h1, 1i h1, 2i hXi hX 1 , X 2 i h1i hSi hX 1 + X 2 i 2 0 p:C h1i h2i h3i tt p:C tt0 h3i h1i h2i hXi h!Xi h1i h! 1 X 1 i+ t0 h1i h2i h3i t0 h3i h2i 2hSi (|C| 1).hSi hS Xi h! 1 X 2 i hS Xi q:C q:C q:C h3i h1i h2i q:C h1i h2i h3i (a.1) (a.2) (a.3) (b.1) (b.2) (b.3) Fig. 3. Agglomeration: .1 Original SN; .2 Unfolded subnet; .3 Reduced folded net. the syntactical arc function composition requires further restrictions on the shape of manageable arc functions. Transitions agglomeration is a useful reduction: it consists of merging causally connected transitions. The aim is to reduce transition instances interleaving, pre- serving specific system properties. A number of techniques have been proposed, with different properties and applicability conditions. Common to most propos- als is this applicability scenario: a set H of transitions put tokens into a place p, leading to a new marking of p from which it is possible to restore its initial state only through the firing of a newly enabled transition t0 ; in that case, the firing of any transition in H may immediately cause the firing of t0 , without interfering with any other transition firing. In this paper, we do not propose a general agglomeration technique for SN, rather, we illustrate how to perform agglomeration by symbolically deriving the arc functions for the new transition. We also provide an intuitive structural condition on SN arc functions, which ensures the applicability of agglomeration in a limited set of cases. Figure 3(a.1) shows a simple example where the transitions t and t0 can be agglomerated. Figure 3(a.2) depicts a part of the net unfolding connected to the instance h1i of t. It is possible to see that, if p is initially empty, after the firing of instance h1i of t, we can safely fire immediately all the newly enabled instances of t0 restoring the p empty state. This is true for any instance hii of t. Figure 3(a.3) is the reduced colored subnet, where the size of class C is a parameter. The reduced subnet can be obtained without unfolding it: indeed, for this type of agglomeration, the following formula allows to symbolically compute the arc functions of the reduced subnet9 : W − (tt0 , r) = W − (t, r); W + (tt0 , q) = W + (t0 , q) ◦ W − (t0 , p)t ◦ W + (t, p) In W + (tt0 , q) the rightmost composition provides the instances of t0 enabled by the firing of an instance of t, through p. Finally composing W + (t0 , q) with this result (firing t0 for all those instances) we obtain a function providing the multiset of tokens to be added in q. For the example of Fig.3(a) W − (tt0 , r) = hXi, while: |C|=3 W + (tt0 , q) = hS − Xi ◦ hXit ◦ hSi = hS − Xi ◦ hSi = (|C| − 1).hSi = 2.hSi Figure 3(b.1) shows another example of reduction. The formula for the agglom- eration can be also used here. The agglomeration is valid for any |C| ≥ 2: 9 W − (t0 , p)t : C(p) → Bag[C(t)] denotes the transpose of W − (t0 , p); the rules to sym- bolically compute the transpose of an arc function are defined in [4]. Composition of SN arc functions 153 W + (tt0 , q) = hS − Xi ◦ h!Xit ◦ hX 1 + X 2 i = hS − Xi ◦ h!−1 Xi ◦ hX 1 + X 2 i = hS − Xi ◦ h!−1 X 1 +!−1 X 2 i = hS−!−1 X 1 i + hS−!−1 X 2 i = 2.hSi − h!−1 X 1 i − h!−1 X 2 i For these examples where p is the only input place of t0 and is the only output place of t, we can confidently state that if (1) the instances of transition t0 are not in conflict with each other (a situation called auto-conflict, which can be checked symbolically on the net structure) and (2) if all the tokens put into p by t can be completely consumed by (one or more instances of) t0 , then we can aggregate t and t0 . To verify the second condition it is sufficient to check the following equality: W + (t, p) = W − (t0 , p) ◦ W − (t0 , p)t ◦ W + (t, p). The following property characterizes the form for the input function W − (t0 , p) which guarantees the agglomeration conditions(s). Let the identity on D be IdeD (d) = 1 · d, ∀d ∈ D. Property 16. Let C(p)0 = W + (t, p)(C(t)) be the (support of the) image of W + (t, p). W + (t, p) = W − (t0 , p)◦W − (t0 , p)t ◦W + (t, p) ⇔ ∀c ∈ C(p)0 W − (t0 , p)◦W − (t0 , p)t (c) = 1·c (i.e. the restriction of W − (t0 , p) ◦ W − (t0 , p)t to C(p)0 is the identity). Observe that with the assumption that p is the unique intermediate place between t and t0 , this property includes also the condition of no autoconflicts among t0 instances (= W − (t0 , p)t ◦ W − (t0 , p) − Ide, simplified formula from [5]). The condition holds for both the examples discussed above, and this can be checked symbolically exploiting the composition presented in this paper. Finally, let us consider a third example, fully exploiting the composition tech- nique presented in this paper. The subnet schema is the same but for t0 , which has one more output place, q 0 . The arc functions for this example are: W − (t, r) = hXi W + (t, p) = hS−!X, S, S − Xi W + (t0 , q) = h!X 2 , X 2 i[X 1 = X 3 ] W − (t0 , p) = h!X 3 , X 2 , X 1 i W + (t0 , q 0 ) = 2 · hX 1 , X 2 i[X 1 6= X 2 ∧ X 2 6= X 3 ] The arc functions for the agglomerated transition tt0 are (λ = |C| with |C| > 2): W − (tt0 , r) = hXi W + (tt0 , q) = (λ − 1)[X 1 =!X 2 ]hS, Si W + (tt0 , q 0 ) = 2(λ − 1)hS − X, Xi + 2(λ − 2)[X 1 6= X 2 ]hS − X, S − Xi The detailed explanation of the steps leading to the result, involving the ap- plication of Lemmas 1 to 4, is in Appendix A.3 of [8]. Observe that the result requires to extend the SN formalism, to allow arc expressions with filters. 6 Conclusions and future work This paper reaches the goal of completing the symbolic manipulation of SN arc functions defining a procedure for the composition of functions mapping on Bags. This enables a number of applications that couldn’t be treated with the operations defined so far. The implementation of a new version of SNexpression including this kind of composition is ongoing. The approach suggests an exten- sion to the SN formalism itself, to allow filters in arc expressions: this feature is now implemented in the GreatSPN Graphical User Interface. The presented results are often parametric in color class cardinality, possibly with some con- straints on cardinality lower bounds. 154 L. Capra, M. De Pierro, and G. Franceschinis Future work is devoted to extend the possible applications of the results pre- sented in this paper, in particular as concerns a generalization of net reduction methods proposed in literature to a wider class of nets: for instance, we expect that our proposal may allow to relax some restriction posed in [11]. Another interesting topic is the elimination of immediate transitions in Stochastic SNs (in order to apply analysis algorithms which do not work in presence of im- mediate transitions): this is a challenging issue since in general it may involve marking dependent sequences of immediate transition firings triggered by one timed transition, as in the case of the example in Fig. 1. References 1. M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Mod- elling with Generalized Stochastic Petri Nets. John Wiley —& Sons Ltd, 1995. 2. E. G. Amparore, G. Balbo, M. Beccuti, S. Donatelli, and G. Franceschinis. 30 years of greatSPN, pages 227–254. Springer London, 2016. 3. G. Balbo and M. Silva, editors. Performance Models for Discrete Event Systems with Synchronizations: Formalisms and Analysis Techniques. Editorial Kronos, Zaragoza, Spain, 1998. Available online. 4. L. Capra, M. De Pierro, and G. Franceschinis. A high level language for structural relations in Well-Formed Nets. In G. Ciardo and P. Darondeau, editors, Int. Conf. on Applications and Theory of Petri Nets 2005, pages 168–187. Springer, 2005. 5. L. Capra, M. De Pierro, and G. Franceschinis. Computing structural properties of Symmetric Nets. In Proc. of the 15th International Conference on Quantitative Evaluation of Systems, QEST 15, Madrid, ES, 2015. IEEE CS. 6. L. Capra, M. De Pierro, and G. Franceschinis. Deriving symbolic and parametric structural relations in Symmetric Nets: Focus on composition operator. Technical Report TR-INF-2019-03-01-UNIPMN, DiSIT,UPO, Alessandria, Italy, 2019. 7. L. Capra, M. De Pierro, and G. Franceschinis. SNexpression: A symbolic calculator for Symmetric Net expressions. In Proceedings PN2020, volume 12152 of LNCS, pages 381–391, Cham, CH, june 2020. Springer. 8. L. Capra, M. De Pierro, and G. Franceschinis. General composition for sym- metric net arc functions with applications. Technical Report TR-INF-2021-05-01- UNIPMN, Computer Science Inst., DiSIT, Univ. del Piemonte Orientale, 2021. 9. J.M. Colom and M. Silva. Convex geometry and semiflows in P/T nets. a compar- ative study of algorithms for computation of minimal p-semiflows. In Rozenberg G., editor, Advances in Petri Nets 1990. ICATPN 1989, volume 483 of LNCS. Springer, Berlin, Heidelberg, 1991. 10. F M Dong, K M Koh, and K L Teo. Chromatic Polynomials and Chromaticity of Graphs. WORLD SCIENTIFIC, 2005. 11. S. Evangelista, S. Haddad, and J. F. Pradat-Peyre. Syntactical colored Petri nets reductions. In Automated Technology for Verification and Analysis, pages 202–216, Berlin, Heidelberg, 2005. Springer. 12. S. Evangelista, C. Pajault, and J. F. Pradat-Peyre. A simple positive flows com- putation algorithm for a large subclass of colored nets. In FORTE 2007, pages 177–195, Berlin, Heidelberg, 2007. Springer Berlin Heidelberg. 13. K. Jensen. An introduction to the theoretical aspects of coloured Petri nets. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, A Decade of Con- currency, Reflections and Perspectives, REX School/Symposium, The Netherlands, June 1-4, 1993, volume 803 of LNCS, pages 230–272. Springer, 1993.