Stochastic symmetric nets (SSN) represent a high-level Petri net formalism characterized by succinct annotations that encapsulate behavioral symmetries. These symmetries are utilized to enhance the eficiency of analysis, such as the construction of a symbolic reachability graph from which a lumped Markov chain is derived and the execution of symbolic discrete-event simulations. In the last two decades, powerful structural analysis techniques have also been developed for SSN. This article explores how these techniques can improve some performance analysis techniques, highlighting potential uses and recent progress.
1. Introduction
(Stochastic) Symmetric nets [
One distinctive feature of PNs is the possibility to derive some properties directly from their structure
without (or before) building the state space; the eficient extension to Colored PNs, without resorting
to unfolding, is not trivial. In the last 20 years, there has been an advance in the symbolic structural
analysis of SSNs. Theoretical foundations are rooted in [
The software tool SNexpression [
In the next sections, we outline a few potential applications of SSN structural analysis related to performance evaluation: the novel results concern a complete formalization providing the basis for the eficient computation of the transitions enabled in a given marking of an SSN, particularly efective when the transition color domains are very large, and the definition of Symbolic Extended Conflict Sets, required in the assignment of priorities and weights to immediate transitions, taking into account all the mutual dependencies.
The SN formalism has been conceived to obtain a model representation whose intrinsic symmetries could be easily exploited. The Symbolic Structural Calculus goal is to derive symbolic representations of structural relations between net nodes: to this purpose, a language has been defined that resembles and extends the SN arc functions syntax. The SN formalism is presented first, followed by the definition of the language used to express the structural relations.
We assume that the reader is familiar with PN and HLPN, places, transitions, input, output, and inhibitor arcs, and marking. Let us succinctly introduce the color structure of an SN focusing on color classes, place and transition color domains, transition guards, and arc functions.
N = (, , Σ, D, , Φ, , , , , m0) where is the set of places, is the set of transitions, Σ is the set of color classes, D assigns to each place and transition its color domain, , and define the arcs connecting the net nodes, and the associated arc functions, : → N is a function defining the priority of each transition; m0 is the initial marking, assigning to each place ∈ a multiset of colors from its color domain D().
• Color classes in Σ = {, = 1 . . . , } are finite and disjoint sets of elements called colors, each class may be partitioned into static subclasses {, } or a circular order relation can be defined on its elements; • Place ∈ color domain D() is defined as Cartesian products of color classes ⨂︀ , ≥ 0, = 1, . . . , ; (), the marking of place , is a multiset of elements from its color domain D(); • Transition ∈ color domain D() defines the colored instances of : a set of typed variables () = { : = 1 . . . , = 1 . . . } is associated with each transition , where the variable type is the color class in Σ, and a binding assigning colors of appropriate type to ’s variables defines a transition instance (that we denote (, )); • Transition guard Φ() is a Boolean function expressed through a standard predicate (defined below) and evaluated on transition instances: the color domain D() of a transition includes all the instances of satisfying the guard. • A function labeling an arc connecting place and transition has domain D() and codomain [D()], the set of the possible multisets on D(). We use the notation ∙ / ∘ as a shorthand notation for the set of places connected with transition through an input/inhibitor arc. The general form of arc functions syntax is: ∑︀ .[], ∈ N, where is a function-tuple ⟨1, . . . , ⟩, i.e, a Cartesian product of class functions , and is a tuple-guard. Each classfunction is a linear function defined on a subset of variables of () of the same type. Let ,/. ). : D() → [] is defined as follows: () be the subset of () of type , and ̃︁ the set of static subclasses of , then =
∑︁ ∈ () . +
.! + ∑︁ ∈ ()
∑︁ ∈{1,...,|̃︁|} ., + . where , , , ∈ Z. Symbol ! denotes the successor operator mapping the value of to its successor (the type of must be ordered). ,/ is a constant function mapping to the set Boolean expressions (guards) on () may be associated with transitions (Φ()) or individual tuples; their terms are standard predicates checking whether two variables hold the same value (1 = 2), or if a variable "belongs" to a given static subclass ( ∈ , ); if Φ() is false for a given instance of , then that instance is not enabled, if a tuple-guard is false for a given transition instance, the associated tuple evaluates to the empty-multiset. Class-functions must be such that no negative coeficients can result from their evaluation for any color satisfying the guard associated with the corresponding tuple/transition (if the guard is not explicit, then it is A transition instance (, ) is enabled in marking m if the following conditions are satisfied: • Φ()() = true • ∀ ∈ ∙ , (, )() ≤ • ∀ ∈ ∘ , (, )() > m()
m() • there isn’t any transition instance (′, ′) : (′) > () enabled in m.
The enabling degree of an enabled transition instance (, ) is defined as follows: (, ) = ∈ ∙ :(,)()̸=0,∈(,)() (, )()() ︂⌊ m()() ⌋︂ The enabling degree of (, ) is not defined 1 for (, ) if ∀ ∈ , (, )() = 0.
The Stochastic Symmetric Nets (SSN) formalism comprises timed and immediate transitions: the
former have priority level 0 and a random firing time (with negative exponential distribution) that
determines the occurrence time of the transition firing and solves the possible conflicts through a race,
the latter have priority level greater than 0, fire in zero time, and the conflicts between transitions at the
same priority level are solved through probabilities obtained by normalizing the weights of transitions
that are in a (direct or indirect) dependency relation. The appropriate specification of immediate transition
weights and priorities in GSPNs (e.g., in the net obtained by unfolding an SSN) has been studied and
discussed in [
expressions: and let D be any color domain built as Cartesian product of classes in Σ, (D = 11 × 22 × ... × Definition 2 (Language L). Let Σ = {1, 2, . . . , } be the set of finite and disjoint basic color classes, , ∈ N). Let : D → (D′) and [′] and [] be standard predicates in D′ and D, respectively. The set of L = {︁ : = ∑︁ .[′][], ∈ N
+}︁ 1Hereafter we shall consider models where the enabling degree is never undefined, considering such situation as a modeling error which can be easily fixed to either prevent the enabling, or to force a fixed enabling degree in those cases. (, ) − (, ) ∘ (′, ) + ⋃︁
(, ) − (, ) ∘ (′, ) ∈∙ ∩∙ ′ ∈∙ ∩∘ ′ (, ) − 1, where 1 is the identity on D()
⋃︁ (, ) − (, ) ∘ (′, ) + ⋃︁ ∈∙ ∩∙ ′
⋃︁ ∈∙ ∩∘ ′ (, ) ∘ (′, ) +
⋃︁ ∈∘ ∩∙ ′ ∈∙ ∩∘ ′ (, ) ∘ (′, ) (, ) − (, ) ∘ (′, ) is the language used to express SN structural relations, where are function-tuples formed by class functions , defined in turn as intersections of language elementary functions {, !, , − , − !, ∅ } (projection, ℎ successor, constant function corresponding to all elements of basic class , projection/successor complement and the empty function; where represents any class and any variable of type ).
We can observe that, with respect to the arc function syntax, there may be a predicate left-composed with a tuple (that we call filter), the set of allowed elementary class functions is a bit diferent, with the complement − among the elementary functions and the introduction of intersection of elementary functions. Any arc function may be expressed through an equivalent expression of this language. Conventions In the following, we use capital letters , , . . . , to denote basic color classes in Σ (the set of types) and the corresponding lowercase letters (possibly with a subscript) to denote variables of the respective type: for example, if D() = 2 × , then () = {1, 2, }. We use sans-serif lowercase letters to denote the elements (colors) of a class, for instance if = {n1, n2, . . . , n} and = {m1, m2, . . . , m}, then (m3, m7, n4) ∈ 2 × .
Symbolic structural relations A structural relation between the SN nodes , ′ is symbolically expressed as a function R(′, ) : D() → 2D(′) and formalized using the language syntax ℒ. Its semantics is that, given an instance of , R(′, )() results in instances ′ of ′ such that ′ R in the unfolding of the SN. We use the symbol R alone to denote a family of relations of the same type. We say that R is symmetric if and only if R(′, ) ≡ R(, ′) for each pair , ′ on which R is defined. A relation may be made symmetric.
Table 3.1 summarizes a set of useful structural relations commonly used in structural analysis with the formulae for their calculation. The (structural conflict), SCC (structural causal connection) and SME (structural mutual exclusion) are defined on a pair (, ′) ∈ × have domain D(′) and codomain 2D().
An illustrative example of a SSN model and structural relation Consider the SN in Fig. 1. The transitions and places are = {1, 2, 3}, = {0, 1}. There is only one color class , that is, Σ = {}. The color domains and variables of the three transitions are: D(1) = , (1) = {1}, D(2) = D(3) = × , (2) = {1, 2}, (3) = {1, 2}. The color domains of the places are: D(1) = , and D(0) = . Let us describe the function for 2: (2, 1) = ⟨2⟩[1 = 2]. (2, 1) : × → 2[]: transition instances of 2 with identical color components 1 and 2, say a, consume one token of the same color, a, from place 1; the remaining instances do not consume tokens from 1.
As an example of structural relation, consider the conflict of 1 and 2 on the tokens in the shared place 0: (1, 2) : D(2) → 2D(1). According to Table 3.1: (1, 2) = (1, 0) − (1, 0) ∘ (2, 0) = ⟨1⟩ ∘ ⟨ 1⟩[1 ̸= 2] = ⟨1⟩[1 ̸= 2]
The meaning is that if we consider an instance 2 : ⟨, ⟩ of 2 (where ⟨, ⟩ ∈ × , ̸= ) then the conflicting instance of 1 is 1 : ⟨⟩ obtained by applying to ⟨, ⟩: ⟨1⟩[1 ̸= 2](, ) = ⟨⟩; this can also be easily verified on the SN unfolding. If we consider (2, 1) : D(1) → 2D(2) instead, we obtain (⟨1⟩[1 ̸= 2]) ∘ ⟨ 1⟩ = [1 ̸= 2]⟨1, ⟩ ∘ ⟨ 1⟩ = ⟨1, − 1⟩ so that if we take an instance 1 : ⟨⟩ the set of conflicting 2 instances is {2 : ⟨, ⟩, ∈ ∖}. In the same net, we could also derive (3, 3), that is, conflicting instances of the same transition 3 that result in (3, 3) = ⟨ − 1, 2⟩ hence, given an instance 3 : ⟨, ⟩, the set of conflicting instances of the same transition is {3 : ⟨, ⟩, ∈ ∖}. Finally, (3, 2) = ⟨ , 1⟩[1 = 2].
Finding transition instances that can fire in a given marking is the core operation in both state-spacebased approaches and discrete-event simulations. The efectiveness or lack thereof of this operation significantly influences the overall methodology within which it is utilized.
Empirical findings using the package GreatSPN [
Drawing on the concept presented in [
Basic notation and definitions The fundamental operations used for the eficient transition enabling
test are [
Definition 3. The transpose of (, ) : D() → [D()] is the function ′(, ) : D() → [D()], characterized by ∀ ∈ D(), ′ ∈ D() ′(, )()(′) = ′(, )(′)().
For example, when = , its transpose with respect to a given colored token within the domain of yields the multiset of instances of responsible for its withdrawal, where multiplicities correspond to the number of tokens withdrawn. As indicated previously, the transpose is an operator in language L.
Multisets are extended to include the value ∞ in the set of scalars N, thus if [] is the set of multisets built over a set then ∞[] is an extension in which multiset elements may have ∞ multiplicity, for instance multiset 3.a1 + 4.a3 + ∞.a2 ∈ ∞[]; Multiset operations are accordingly extended in a straightforward way according to the scalar Algebra rules.
If m ∈ [], with m = ∑︀ .a, and ∈ N then the division of m by is defined as follows: m = ∑︁ ⌊︁ ⌋︁ .a
Definition 4 (Simple Function). A function ∈ L, : → [′] is said simple if: ∀ ∈ , ′ ∈ ′ : ()(′) ≤ 1 In other words, a simple function always results in multisets where elements are not repeated. Definition 5 (Normal Form). A function ∈ L, : → [′], such that := ∑︀ , is said to be in Normal Form if - ∀ is simple, ∈ N+ and ∃ ∈ N+ : ∀ ∈ , () ̸= 0 =⇒ |()| = - ∀, ̸= =⇒ ∩ = 0 Proposition 1. Any function ∈ L has a Normal Form. The Normal Form of is not unique in L.
The proposition states that an arc function can be rewritten as a weighted sum of pairwise disjoint terms. Each term thus results, when evaluated on the domain values, in multisets that retain identical cardinality , and where all elements possess the same multiplicity of one, except for those arguments rendering the term null. We call the size of the term and use the notation = ||.
Figure 2 illustrates an SN transition that encapsulates a sort of synchronization. Two color classes, and , are used to represent the processing nodes and the messages, respectively. The color domains of the places are explicitly defined, while D() = × corresponds to the variables (projection functions) and present in the incident arcs. The enabling of depends on the marking of the places 1 (input) and 2 (input and inhibitor).
The function (2, ) in Figure 2, left part, can be rewritten in normal form as shown in Figure 2, right part: The two terms (function tuples) have cardinality | | − 1 and 1, respectively.
An intuitive lemma, which follows directly from Proposition 1, establishes the final form of input and inhibitor arc functions.
Corollary 1. Let (, ) ̸≡ 0 and (, ) ̸≡ 0. These functions can be expressed in a Normal Form, ∑︀ and ∑︀ , respectively, such that ≡ ∨ ∩ = 0, ∀, .
We will assume that the input and inhibitor arc functions are written in a normal form and meet the Corollary 1. The function (2, ) in Figure 2, left part, is accordingly rewritten as shown in Figure 2, right part: the two diferent function tuples in (2, ) and (2, ) are disjoint. As discussed earlier, we assume that there cannot be transition instances that make (, ) = 0 for all input places of : in other words, the enabling condition of all instances must involve at least one input place.
The subsequent corollary arises directly from the definition of a transpose.
Corollary 2. Let := ∑︀ be a normal form. Its transpose = ∑︀ is in normal form.
(, 2) = 2.⟨, , ⟩ + ⟨, − , ⟩ (, 2) = 3.⟨, , ⟩ + 3.⟨, , − ⟩ Let 1 = ⟨, − , ⟩, 2 = ⟨, , ⟩, and 3 = ⟨, , − ⟩, thus (, 2) = 1 + 2 · 2 and (, 2) = 3 · 2 + 3 · 3. The sizes of the terms involved are: |1| = − 1, |2| = 1, and |3| = − 1. After transposing them, we obtain the following expression: (, 2) (, 2) = =
1=⟨,− ,⟩ ⏞1.⟨1, ⟩[1 ̸= 2] ⏟ +
2.2=2.⟨,,⟩ ⏞2.⟨1, ⟩[1 = 2]
⏟ 3.2=3.⟨..⟩ ⏞3.⟨1, ⟩[1 = 2] ⏟ +
3.3=3.⟨,,− ⟩ ⏞3.⟨1, − ⏟⟩[1 = 2] The normal form of the result allows us to write the enabling conditions locally to place 2 and inferable from the transposes: [1, ∞) ⟨1, ⟩[1 ̸= 2], [2, 3) ⟨1, ⟩[1 = 2], [0, 3) ⟨1, − ⟩[1 = 2]
⏟ 1⏞ ⏟ 2⏞ ⏟ 3⏞ class = {n1, . . . , n4} class = {m1, . . . , m } ∪ {ack} vars : :
D(1) = D(3) = × D(2) = × × The above expression conveys most of the information needed for the enabling test: for example, let c ∈ m(2) and its multiplicity, then [2, 3)2(c) = 2(c) if 2 ≤ < 3, otherwise [2, 3)2(c) = 0. [2, 3)2(c) constitutes a superset of the enabled instances of when the color c is in the current marking of 2. Obviously, for a given c, the terms 1(c), 2(c), and 3(c) are disjoint sets of instances. Definition 6 (Enabled Super-Set Fragment). Assume (, ) and (, ) to be in normal form and term . to be in (, ) or term . to be in (, ), where , ∈ N. Then:
[, ) is a function [D()] → [D()] so defined:
= , and = ∞ if = 0 otheriwise = and: ∀d ∈ m(), [, ) (d) =
∅ ︂{ (d) if ≤ m()(d) <
ℎ [, ) (m()) =
∑︁ [, ) (d) d∈m()
Intersecting all the Enabled Superset Fragments applied to marking m(2) further refines the resulting superset of the enabled instances of locally to 2: Definition 7 (Enabled Super-Set). Given the Enabled Superset Fragments {︀ [ , )}︀ for pair (, ), the function (, ), which applies to a marking, is defined: ⋂︁[ , )(m(2)) (, ) = ⋂︁[ , )
(, 2) = [1, ∞) ⟨1, ⟩[1 ̸= 2] ∩[2, 3) ⟨1, ⟩[1 = 2] ∩[0, 3) ⟨1, − ⟩[1 = 2] ⏟ 1⏞ ⏟ 2⏞ ⏟ 3⏞ and similarly, but less complex:
(, 1) = [1, ∞)⟨, ⟩
In Def. 6 looking for tokens that in current marking m satisfy the constraint ≤ m() < , when = 0, is not practicable because it will lead us to evaluate also for tokens that are not in the marking (they have multiplicity 0 in m). Thus, when = 0 for some we will compute the superset of the enabled instances for that via the complement of the disabled instances:
[0, )] = ([, ∞) )∁
When ̸= 0, (, ) is in general a proper superset of the enabled instances. We will use the information conveyed by the cardinality of to calculate the actual set of enabled instances, as well as their enabling degree: If, due to the application of term [, ) to the current marking of , (, c) is in (, )(m()) then we know that this instance will require from a sub-multiset2 with | | distinct colors. We can compute how many of the tokens required by (, c) are actually in applying [, ) (m()) and counting the scalar multiplicity of (, c), we will call this value the Connection Degree of (, c) with regard to [, ) , and in the current marking.
For example, consider a very simple net with a transition and place with D() = = {a, b, c, d} and (, ) = ⟨ − ⟩. Then, (, ) = ⟨ − ⟩, and the unique Enabled Super-Set Fragment is [1, ∞)⟨ − ⟩, thus
(, ) = [1, ∞)⟨ − ⟩ Assume first that m1() = 2.a + 2.b + 2.c + d. In this marking, it is straightforward to see that all instances of are enabled, moreover the one of color = d has the enabling degree 2, while all the others have the enabling degree 1. By Def. 6:
(, )(m()) = 3.a + 3.b + 3.c + 3.d Thus, the obtained Enabled Super-Set matches the actually enabled instances. Observe that in the above expression, the scalar 3 points out that each instance will withdraw by marking m() 3 tokens with a distinct color (for example, instance (, a) will withdraw a multiset b + c + d). Now let us consider a diferent marking: m2() = a + b + c; in this case only instance (, d) is enabled, however (, )(m()) = 2.a + 2.b + 2.c + 3.d In this case, the Enabled Super-Set is a proper superset of the actually enabled instances because instances (, a), (, b), and (, c) are not enabled. However, the multiplicity 2 indicates that these instances were derived from only two distinct colors in m(), while three are actually required; instead, instance (, d) is derived from 3 = || − 1 = | − | distinct colors in m(). We shall call this multiplicity Connection Degree because, in a certain sense, it represents the number of connections from a given instance to distinct token colors in m(). We will see later how to use this information to refine the Enabled Super-Set function, but first let us formalize the above concepts.
Definition 8 (Connection Degree). Given the pair (, ), let [, ) be an Enabled Superset Fragment of (, ), and m() the marking of . Let b ∈ [D()] such that (, )(m()) = b. Let the value ∈ N be the multiplicity of the color instance c ∈ D() in multiset b. Then, is said Connection Degree of instance (, c) in m locally to place and Super-set [, ) .
The Connection Degree provides us with how many distinct tokens, of those needed by a given instance (, c) belonging to [, ) (m()), are actually in m(). If = | |, then instance (, c) is enabled locally to place and Superset Fragment[, ) . When this holds, let be the minimum multiplicity of the distinct tokens required by (, c) actually in m():
= d∈ (){m()(d)}
then ⌊/ ⌋ is the Enabling Degree of the instance (, c), relative to Fragment [, ) . Referring to the marking m1 of the previous example, it holds = 1 for all instances of except (, d) , due to the single token of color d in place ; instead, for example (, d) it holds = 2 because each needed token has multiplicity 2.
Again, if for all the Connection Degree is equal to = ||, then we can say that instance (, c) is actually enabled in m(). The actual enabling degree is {⌊/ ⌋}.
Definition 9 (Enabling Degree). Given (, ), and a term appearing in the normal form of (, ), then (, ) for marking m is a function mapping to a multiset of colors of so defined: (, )(m) =
∑︁ c∈(,)(m()) d∈(){m()(d)} .c and (, ) is a function so defined:
(, )(m) = {(, , m)} Definition 10. Given pair (, ), and (, ) the Super-set function of the enabled instances. Then, the actually enabled instances of locally to are given by the following function: (, ) =
⋂︁ ∀: ̸=0 [ , )
⋂︁ ∀: =0 ∞︀( [ , ∞))︀ ∁ where = ||.
We observe that in Def. 10 the division by puts to 0 the multiplicities of the instances in [ , ) such that the Connection Degree is less than . The instances remaining in (, ) will have multiplicity 1.
The actual enabled instances are finally computed by intersecting the locally enabled instances in all places.
Definition 11 (Enabled instances). Let () ∈ [D()] represent the instances of enabled in a marking m. Then, (, m) =
(, )(m()) ⋂︁ ∈∙ ∪∘ () = ⋂︁ (, )
and the Enabling Degree function is:
For example, consider the following marking of the SN shown in Figure 2 (right part), where = {n1, . . . , n4}, = {m1, . . . , m } ∪ {ack}, > 1: m(1) = 2⟨n1, m1⟩ + ⟨n2, m2⟩ m(2) = 4⟨n1, n2, m1⟩ + 2⟨n1, n3, m1⟩ + 3⟨n1, n4, m1⟩ + 2⟨n1, n1, m1⟩ + 3⟨n2, n2, m1⟩ + 2⟨n2, n1, m2⟩ + 2⟨n2, n3, m2⟩ + 2⟨n2, n4, m2⟩ + 3⟨n3, n1, m2⟩ + 2⟨n3, n2, m2⟩ Let us compute (, 2)(m(2)), the enabling function locally to place 2. Thus, we first compute the Enabled Super-set Fragments [1, ∞)1(m(2)),[2, 3)2(m(2)), and [0, 3)3(m(2)) (Def. 6). Let us look at the term associated to 3: [0, 3) ⟨1, − ⟩[1 = 2], with 1, 2 ∈ , ∈
⏟ 3⏞ The transition instances belonging to this parametric set have no input from 2 but only inhibition. Since 3 = 0 we will compute these instances using the complemented formula:
[3, ∞)3(m(2))∁ By applying the function [3, ∞)3 to marking m, we obtain ⟨n2, − m1⟩, the result is due to the only token ⟨n2, n2, m1⟩ ∈ m(2) such that the first and second components are equal (guard 1 = 2) and whose multiplicity is at least 3 in m(2). This tuple identifies the instances of inhibited in the current marking and therefore excluded from (, 2). Complementing it provides the superset of the instances we are looking for:
[3, ∞)3(m(2))∁ = ∞⟨ − n2, ⟩ + ∞⟨n2, m1⟩ As second Fragment to evaluate in m(2), let us consider the term associated with 1: [1, ∞) ⟨1, ⟩[1 ̸= 2] with 1 ∈ , 2 ∈ , ∈
⏟ 1⏞ This parametric set represents a group of instances of consuming tokens from 2 but not inhibited (upper range ∞). All of these instances need at least one instance of the consumed colors. The evaluation in the current marking results in (see Def. 10):
[1, ∞)⟨1, ⟩[1 ̸= 2](m(2)) = ⟨n1, m1⟩ + ⟨n2, m2⟩ In detail follows the calculus that leads to this result. The representation below highlights in the underbrace the instances of each color in m2 maps to, consistently with the multiplicity of the color in the marking: m(2) = 4⟨n1, n2, m1⟩ + 2⟨n1, n3, m1⟩ + 3⟨n1, n4, m1⟩ ⏟since 4≥ ⏞1 then ⏟since 2≥ ⏞1 then ⏟since 3≥ ⏞1 then [1,∞)1(n1,n2,m1)=⟨n1,m1⟩ [1,∞)1(n1,n3,m1)=⟨n1,m1⟩ [1,∞)1(n1,n4,m1)=⟨n1,m1⟩ ⏟ ⏞ [1,∞)1(︀ ⟨n1,n2,m1⟩+⟨n1,n3,m1⟩+⟨n1,n4,m1⟩)︀ =3⟨n1,m1⟩ + + 2⟨n1, n1, m1⟩ + 3⟨n2, n2, m1⟩ + ⏟ since 1=⏞2 then [1,∞)1(⟨n1,n1,m1⟩+⟨n2,n2,m1⟩)=0 + 2⟨n2, n1, m2⟩ + 2⟨n2, n3, m2⟩ + 2⟨n2, n4, m2⟩ + 3⟨n3, n1, m2⟩ + 2⟨n3, n2, m2⟩
⏟ 3⟨n2,m⏞2⟩ ⏟ 2⟨n3,m⏞2⟩
There exist two instances, namely ⟨n1, m1⟩ and ⟨n2, m2⟩, whose Connection Degree is |1| = 3; both instances have enabling degree 2, since those are the minimal multiplicities common to the involved tokens present in m(2): respectively to the first three tokens in m(2) above, 1(, 2)(⟨n1, m1⟩) = {4, 2, 3}, and respectively to the tokens from 6th to 8th in m(2) above, 1(, 2)(⟨n2, m2⟩) = {2, 2, 2}. There are instead only 2 tokens in m(2) (the last two), resulting in instance ⟨n3, m2⟩, thus its Connection Degree is lower than |1|. Consequently, this term of (, 2) leads to the result ⟨n1, m1⟩ + ⟨n2, m2⟩.
The last Fragmentto evaluate is the one associated with 2, namely
[2, 3)⟨1, ⟩[1 = 2](m(2)) Let us show below only the tokens in m(2) that do not map to the empty multiset: m(2) =
2⟨n1, n1, m1⟩ + 3⟨n2, n2, m1⟩ [2,3)2(⟨n1,n1⏟,m1⟩)=⟨n⏞1,m1⟩ since 2≤ 2< 2 [2,3)2(⟨⏟n2,n2,m1⏞⟩)=0 since 3≥ 2
Thus, [2, 3)2(m(2)) = ⟨n1, m1⟩ and 2(, 1)(⟨n1, m1⟩) = 2/ 2 = 1.
Intersecting the three Fragments (Def. 10) yields the final result:
(, 2)(m(2)) = ⟨n1, m1⟩ with (, 2)(⟨n1, m1⟩) = {2, 1, ∞} = 1.
Similarly, it can be computed that (, 1)(m(2)) = 2⟨n1, m1⟩ + 1⟨n2, m2⟩ with the respective enabling degree equal to 2 and 1. In conclusion, (, m) = ⟨n1, m1⟩ with enabling degree 1.
Throughout various stages of computation, we have implicitly applied certain operators of structural calculus, including composition, diference, and intersection. These operators enable us to manipulate symbolic representations eficiently. 3.1. Eficient state space generation The approach just described may be integrated using a traditional method based on a proficient update of the set of enabled transition instances. Structural relations inherently encapsulate all potential dependencies that are locally induced by the firing of a transition instance. Such an instance has the capability to disable instances with which it is in (structural) conflict and to enable those to which it is (structurally) causally connected. Hence, exploiting the transpose of structural conflicts and causal connections (see Table ) computed on the net structure it is possible to incrementally update the set of enabled instances after the state change due to enabled transition instances.
The most recent version of SNexpression [
In conjunction with the established symbols representing matrices for net adjacency lists and
fundamental relationships, namely Structural Conflict, Structural Causal Connection, and Structural Mutual
Exclusion, a novel symbol is introduced to denote a more comprehensive and intricate form of
dependency between transitions, termed Structural Dependency (SD). SD was first introduced for GSPN in
[
An immediate application of the SD relation is in the calculation of the well-known ECS (Extended
Conflict Sets) [
The algorithm for computing the ECS in SN, as equivalence classes of the SD* relationship, has been
presented in [
SCS enables the consistent assignment of probabilistic weights to immediate transition instances.
Furthermore, it may be leveraged to construct the ordinary or symbolic reachability graph of an SSN
with enhanced eficiency and eficacy by minimizing the interleaving of immediate transitions, since
instances pertaining to two independent sets can be executed in arbitrary sequence.
Computing ECS in SSN: an application example We illustrate the derivation of the Symbolic ECS
(SCS) by applying the method to an SSN inspired by a model of the Model Checking Contest3. This SSN
models a Utility Control Room [
SD* for this net is a block matrix (see Tab. 3) composed of three blocks, 1,2 and 3, since there are three priority levels. Transitions in diferent priority groups are in diferent SCS. The derivation of SCS for the groups 1 and 2 is easier because they are both composed by a single colored transition. Let us illustrate the computation of the SCS for transition instances in the three groups.
SCS for transitions in 1: matrix block 1 is composed of transition assignSameZone only, instances of this transition can still be partitioned in several SCS. To compute them, consider the parametric instance assignSameZone(, 1), where {, 1} = (assignSameZone) and start checking which other instances of the same transition are in the same class using the dependency relation in 1. Thus, symbolically instantiating SD*(assignSameZone, assignSameZone) = ⟨ , 1⟩ on such a color parameter ⟨ , 1⟩(, 1) allows obtaining the requested dependent instances, thus belonging to the same SCS: ⟨ , 1⟩(, 1) = ⟨, 1⟩. SECS is updated as follows:
SCS(, 1) = {assignSameZone(, 1), assignSameZone(, 1) : ∈ , 1 ∈ } and after simplification (in fact SD * is reflexive then the first instance is contained in the second group of instances)
SCS(1) = {assignSameZone(, 1), 1 ∈ } This symbolic expression for the SCS covers all the instances of assignSameZone, that is all instances are assigned to one SCS. To check this condition, we can apply again the symbolic calculus: ∑︁ ⟨, 1⟩ → ⟨ , 1⟩ ∘ ⟨ ⟩ = ⟨ , ⟩ → ⟨, ⟩ 1∈ ⏟ equivalent⏞calculus
performed in functional form
SCS for the transition assignNearZone in 2: as for 1, one can compute SCS instantiating the function in 2 on the colors of the parametric instance assignNearZone(, 1, 2), which results in two SCSs due to mutually exclusive guards [1] and [2]: and
SCS(, 1, 2) = {assignNearZone(⟨, 2, 2⟩), ∈ , 1 ∈ 2, 2 ∈ 3} SCS(2) = {assignNearZone(⟨, 2, 2⟩), 2 ∈ 3} SCS(, 1, 2) = {assignNearZone(⟨, 3, 2⟩), ∈ , 1 ∈ 3, 2 ∈ 2} SCS(2) = {assignNearZone(⟨, 3, 2⟩), 2 ∈ 2} it simplifies
→− it simplifies →−
SCS for the transitions in 3: 3 is made up of transitions {assignFar, assignMunicipality}.
The method first categorizes all the instances of assignFar iterating on the functions in the first
column of 3; we obtain the instances respectively of assignFar and assignMunicipality in
some SCS with assignFar(, 1, 2). Due to the guard [3] on the function in 3[
SCS(, 1, 2) = {assignFar(, 1, 2), assignFar(⟨, 4, 1⟩ + ⟨, 1, 4⟩),
assignMunicipality(⟨, ⟩), ∈ , } and after some simplification:
SCS = {assignFar(⟨, 4, 1⟩ + ⟨, 1, 4⟩), assignMunicipality(⟨, ⟩)} Each remaining instance of assignFar(, 1, 2), whose color does not satisfy 3, is in its own separate SCS. It remains to classify the instances of assignMunicipality not classified in the previous step, and in relation only with itself, because due to the symmetric nature of 3 assignFar instances in some SCS with assignMunicipality were considered in the previous step. However, in this particular case all the instances of assignMunicipality have already been classified because the previous calculated assignMunicipality(⟨, ⟩) contain all.
The symbolic structural relation calculus for (Stochastic) Symmetric Nets developed in the last two decades and implemented in the SNexpression tool is the basis for enabling several tasks that can be useful when analyzing an SSN model. In this paper, we have presented a novel method exploiting the operators of the structural calculus to derive the transition instances enabled in a given marking, applying functions derived from the structure directly to the marking, instead of enumerating all possible color instances and testing their enabling conditions: this is a useful feature which is common to state space construction and discrete event simulation of SSN. We have also illustrated the operators recently introduced in SNexpression and operating on matrices of functions derived from the model that, in particular, can express in a symbolic form the dependency relations between transitions, useful to support the definition of the probabilities to be used for conflict resolution between immediate transitions. Among the other features implemented in SNexpression and not discussed in this paper, we recall the automatic generation of a system of Symbolic Ordinary Diferential Equations (SODE), which can provide approximate average results in systems that have very large state spaces. Using the symmetry of the model, a reduced number of equations is generated, usually much smaller than the total number of place instances. The adaptation of the method to the parametric size of color classes is ongoing. Another useful feature is the ability to verify that a given P-invariant holds, which is also required to verify the applicability of a SODE-based solution.
Future work will integrate additional features into the tool to improve it in several directions: (1) expanding the calculus to include general composition (of functions mapping on multisets), (2) improving the rules for the simplification of the resulting formulas, and (3) achieving a seamless integration with other tools, in particular with GreatSPN.
The SNexpression tool can be downloaded from http://www.di.unito.it/~depierro/SNexpression/. Two releases are currently available: the latest, integrating the calculation of structural properties on a whole SN using a matrix calculus, and the previous one, implementing the structural properties computation for specific pairs of nodes in the net, specified by the user. Several example models illustrated in the publications are also available online. A translator from the GreatSPN net description format (.PNPRO) (https://github.com/greatspn) to the SNexpression format (.sn) can be downloaded from the home page.
The Utility Control Room model used in Section 4 is depicted in Figure 3: the SCS computation concerns the subnet of immediate transitions in the frame.