<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Petri Sport: A Sport for Petri Netters</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Stefan Klikovits</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Alban Linard</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Dimitri Racordon</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Didier Buchs ?</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Software Modeling and Verification (SMV) Group, Faculty of Science University of Geneva Geneva</institution>
          ,
          <country country="CH">Switzerland</country>
        </aff>
      </contrib-group>
      <fpage>35</fpage>
      <lpage>56</lpage>
      <abstract>
        <p>Petri nets are a family of formalisms dedicated to the representation of concurrent systems. Their strength is the compact modeling of complex behaviors using very simple rules. Despite this simplicity, many teachers observe that students often require a lot of exposure and numerous exercises to truly understand the semantics of Petri nets. In order to speed up this learning process and provide a different attack angle, we propose Petri sport, a fun game based upon the Petri net formalism. In Petri sport, players aim to gather points by moving across a Petri net-shaped playing field and “firing” transitions. A clock-based play style supports a structured game advance while at the same time it encourages players to move fast. As the playing field is shaped like a Petri net, it is possible to challenge a player's movement speed, intellectual capabilities, as well as team coordination and communication. The difficulty level of Petri sport is based on the choice of playing field. This allows for adaptation in order to best fit the competitors' age, experience and/or physical fitness level.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>-</title>
      <p>A significant part of the system and software engineering community embraces
Petri nets for their capability to model and simulate complex behaviors, such as
concurrent systems. The adoption of Petri nets can be explained by their clear
and elegant semantics, as well as their simple graphical notation. Since their
introduction [Pet62], there have been many efforts to extend, adapt and modify
the formalism. Such efforts materialized for instance in the addition of inhibitor
arcs [Zai14], which provide Turing completeness, or Colored Petri nets [Jen14],
which enable for more compact representations, by adding the possibility to use
distinguishable types of tokens.</p>
      <p>These concepts are useful and make the Petri net formalism (family)
powerful and versatile, albeit difficult to learn. In the course of our teaching activities,
we regularly observe that a significant part of our students struggle to fully
understand the Petri net semantics. As a result, confusion and misunderstandings
slow down the learning process and hinder the understanding of advanced Petri
net variants and tooling.</p>
      <p>This motivated us to tackle the problem with a different approach, which
led us to the design of Petri sport. Petri sport is a game based on the Petri
net formalism. The sport borrows from the graphical syntax of the formalism to
design playing fields, and from its semantics to establish the playing rules. The
game’s concept originated as a means for students unfamiliar with Petri nets to
observe its semantics by actively “being part of it”. Through further gamification
[Kap12], and in particular the introduction of a competitive aspect, Petri sport
became a canvas which can be used to teach advanced Petri net concepts through
the lens of an entertaining activity.</p>
      <p>We designed a handful of different Petri sport variants so that the game’s
difficulty is adaptable to the player’s theoretic knowledge, experience and
physical fitness. While in its most basic form the game underlines coordination, quick
thinking and stamina, we also developed puzzle modes and similar variants,
which aim at challenging players’ intellects in a less physical way. Based on our
observations of Petri sport’s entertainment potential, we are certain that even
senior researchers will enjoy this “academic” sports discipline1. The rest of the
paper is structured as follows: Section 2 outlines the rules of Petri sport and
explains the playing field, the teams and the game play. Section 3 discusses
the formal basis which underlies Petri sport. Section 4 discusses different game
variants and adaptations that can be incorporated. Section 5 elaborates on the
constraints of the playing fields and properties that should be satisfied in order to
guarantee entertaining game rounds. Section 6 provides details about the
experiments we performed. Section 7 discusses related work and similar approaches.
Section 8 concludes.
2</p>
    </sec>
    <sec id="sec-2">
      <title>Rules</title>
      <p>Petri sport is a team-based game, played on a field whose shape resembles a Petri
net. Each team consists of several players who act as the tokens of the Petri net.
At the beginning of the game, players are either within places, in which case they
are called bound players, or alongside the playing field, in which case they are
called free players. Similarly to Petri nets, we use the term marking to refer to an
assignment of players (i.e. tokens) to places. To advance the game, players must
fire transitions, according to a set of rules describing how tokens are consumed
and produced.</p>
      <p>In order to fire a particular transition, bound players must move from
precondition places to the transition, following the arcs of the laid out Petri net.
Once they reach the transition, they meet free players who then carry on the
firing process by moving to the postcondition places. Bound players satisfying the
preconditions become free only after the transition firing completed, i.e. when
the formerly free players reached their respective postcondition places. On the
1 We believe that Petri sport might even bring sustainable health benefits to the Petri
net community.
other hand, free players satisfying the postconditions become bound upon
completion of a transition firing. Hence, the total number of bound and free players
involved depends on the weight of the input and output arcs of the transition,
respectively. As in a classic Petri net, a transition can only be fired when it is
enabled. This requires that the number of players in the preconditions at least
matches the weight annotation of the arc coming out of these preconditions. In
addition, the number of free players available should be at least the sum of the
postcondition weights. Figure 2 shows examples of the enable semantics.</p>
      <p>Conceptually, the firing semantics can be represented as a classic Petri net
where each transition is connected to a special free place by pre- and
postcondition. free is the virtual place where free players are positioned before/after
they are bound. The weight of the arc from free to the transition is the sum of
postcondition weights, while the weight of arc from the transition to free is the
sum of the precondition weights. An example is depicted in Figure 3.</p>
      <p>This behavior helps avoiding the common misconception that tokens are
passing from preconditions to postconditions. Our semantics clearly shows that
players who are freed from preconditions are not the same as the players who
get bound to postconditions.</p>
      <p>Petri sport rules revolve around the concept of correctly firing transitions.
The overall goal is to fire certain point-awarding transitions as often as possible
within limited time. Depending on the “game flavor”, rules may be added or
modified in order to make the game more entertaining and/or challenging. A
discussion of such variants is given in Section 4.
2.1</p>
      <sec id="sec-2-1">
        <title>Field</title>
        <p>A typical Petri sport field (a sport Petri net, SpPN ) consists of places and
transitions which are distributed and connected via arcs. Places are traditionally
1
1
1
1</p>
        <p>X
1
1
1
1
1
1
1
1</p>
        <p>X
X
1
1
1
1
(a) Precondition violation</p>
        <p>(b) Not enough free players
(c) Enabled transition
(d) State after firing Figure 2c
represented as circles, while transitions are marked as rectangles. We found that
hula hoops and small fitness carpets nicely lend themselves to represent places
and transitions, but any other means is thinkable, as long as places and
transitions are easy to see and distinguishable from each other. Arc connections are
drawn lines or strings (tent pegs are useful to tie them to the ground). It is
important to annotate arcs with their respective weight (if greater than 1). In our
experience sheets of paper with large, bold, well-legible numbers usually suffice.</p>
        <p>Petri sport can be played on any flat terrain both indoors and outdoors,
provided there is enough space and the risk of injury is reasonably low. The
field’s size is not fixed and can vary depending on the teams’ sizes, players’
familiarity with both Petri nets and Petri sport, and players’ physical fitness.</p>
        <p>Most of the above descriptions are suggestions and should be adapted by the
game hosts. The authors appeal to the game organizers’ creativity to find the
best means possible to establish a playing field. For example, if playing on a
pool of free players
concrete surface it is quick, easy and cheap to simply draw a field using chalk,
instead of using hoops, mats and strings as on a grass pitch.
2.2</p>
      </sec>
      <sec id="sec-2-2">
        <title>Example sport Petri net</title>
        <p>An example of Sport Petri net (SpPN) is given in Figure 4. The SpPN consists
of six places (p0 – p5) and eight transitions (t0 – t7). Players aim to fire the
point-winning transition t2 as often as possible.</p>
        <p>The initial marking displayed in Figure 4, prescribes two players to be placed
in p5. From there, there are two main strategies to follow in order to reach t2.
Players can follow the sequence t5 ! t6 ! t3 ! t4 ! t2 which leads to scoring
two points and resetting the net to its initial state. Alternatively, a player can
reach t2 by firing t7 ! t1 ! t2. Assuming all tokens produced by t1 advance to
fire t2 immediately, this sequence awards five points but involves much longer
transitions (in terms of distance). Further, after this transition there are five
tokens bound within the SpPN.</p>
        <p>This SpPN also features a sink transition t0 which frees two tokens bound
within p0 and p1, respectively. Deadlocks can occur when too many players are
in places p0 and p1, as there can be not enough free tokens for the postcondition
of t1. t0 can then be used to provide these free players. Its firing requires
coordination between players in p0 and p1. However, it is important to understand
that this can easily lead to deadlock situation, such as when firing the sequence
t7 ! t0 ! t7 ! t0 since there are no more bound tokens on the field.
2.3</p>
      </sec>
      <sec id="sec-2-3">
        <title>Teams</title>
        <p>Petri sport is a team-sport. The minimum number of teams is one, but in our
experience a competitive play between at least two even-sized teams increases
the enjoyment of the game. At any given moment only one team is actually
playing. This means that the teams alternate between rounds and try to score
a maximum of points in their respective round – there is no direct engagement
between the teams.</p>
        <p>The size of a team heavily depends on the playing field. While theoretically
the number of players is unlimited, a too large number of players often leads
to too large number of enabled transitions, confusing situations and unclear
decisions. From our experience, a team size of around 8-12 players is ideal, as
this provides many situations where trade-offs have to be taken into consideration
and a strategy has to be devised in order to avoid reaching deadlocks.
2.4</p>
      </sec>
      <sec id="sec-2-4">
        <title>Game setup</title>
        <p>During the setup phase players can get an overview of the playing field and briefly
discuss strategies. Subsequently, the players spread across the field according
to the initial marking, that is the players-to-places assignment that has to be
upheld at the start of the game. It must be provided by the game host and
defined together with the playing field.</p>
        <p>Players that are not assigned to any places become free and position
themselves around the playing field. It is important that free players leave the
immediate playing field (it should be easy to see when a player is inside or outside
the pitch), in order to clearly distinguish them from bound ones.</p>
        <p>This setup phase takes, depending on the field’s complexity, between one and
two minutes. Immediately at the end of this timespan the main phase is started
without any pause in between.
2.5</p>
      </sec>
      <sec id="sec-2-5">
        <title>Main phase</title>
        <p>The main game phase is dictated by a clock providing a constant pace. In regular
intervals (e.g. every 30 seconds) the clock emits a loud signal (a beep). Transition
firings have to start clearly after one beep and finish before the next one. The
completion of a firing brings the marking to a “normal” state. This means that
the players that were freed leave the immediate playing area (i.e. outside of the
field) and the newly bound players are positioned clearly within their new places.
Teams are awarded points for successfully firing certain predefined transitions.
In the example in Figure 4 transition t2 is the only point-scoring transition, but
in general there might be more than one.</p>
        <p>Sequential firings Following the firing of one transition, and thereby the
freeing of bound and production of newly bound players, it is possible for players
to be involved in another transition before the end of the clock interval (i.e.
before the next beep). Requirement for the firing of another transition is that
the previous firing is completed and all players involved in the new transition
have reached their final positions of the previous one (free tokens outside the
field, bound tokens reached their post-places). It is thus possible for a team to
fire multiple transitions in sequence before a beep occurs.</p>
        <p>Parallel firings In addition players are also allowed to fire several transitions
in parallel. Instead of chaining transitions, parallel firing is performed by firing
several transitions concurrently. It requires enough free players for the
postconditions of all the transitions, and is thus less likely to happen than sequential
firings.</p>
        <p>Transaction All transitions that are fired during one clock period are
collectively referred to as a transaction. Figure 5 shows a transaction with two parallel
sequences S1 = t5 ! t6 ! t4 and S2 = t7 ! t1. The transition firings within
those sequences can be started at any point between two beeps, but have to
finish before the next beep. Transition t1 in this example would not finish firing
before the end of the interval and thus infringe the rules of Petri sport. Such a
rule infringement is penalized by a rollback, as explained below.
S1
S2
t5
t7
t6
t4
t1
Fig. 5: A transaction consisting of two sequences S1, S2 and five transitions
t5, t6, t4, t7 and t1. The attempt to fire t1 does not complete before the end
of the interval and thereby triggers a rollback. The interval limits (beeps) are
represented by the thick lines.
Rollback Transition firings have to finish before the end of the current clock
interval. If any transition firing does not finish before the next beep, the entire
transaction has to be reset and no points are awarded for the entire transaction.
In Figure 5 this means that a firing of t1 will result in all transitions of both
sequences to be rolled back, and the marking at the beginning of the transaction
is established.</p>
        <p>Thus, this rule prevents “opportunistic” transition firings with low chance of
success, but also adds a suspense factor for “close transactions”. This behavior
forces the players to assess the risk of firing several transitions versus the safety
of firing only one. It also gives more value to parallel firings, that are difficult to
coordinate.</p>
        <p>Sudden death Additionally to the rollback an additional sudden death penalty
is introduced. Sudden death dictates that if a transaction has been executed in
a faulty manner (e.g. not enough/too many players are involved in a transition),
the transition is reset and the transaction stops, but additionally one free player
is excluded from the game round and can no longer participate during the whole
round. The whole transaction is not rolled back, as there is already a penalty for
the fault, but all other transitions that were being fired in parallel are canceled.
2.6</p>
      </sec>
      <sec id="sec-2-6">
        <title>Winning conditions</title>
        <p>A round of Petri sport ends if either of the following conditions are met:
Timeout The game time is over and a predefined number of beeps is reached.
Deadlock No further transitions are enabled, naturally (being trapped due to
game design), or due to sudden death (i.e. loss of free players making it
impossible to satisfy postconditions).</p>
        <p>Livelock While it is possible to fire transitions, it is not possible to reach a state
where the team can still score points i.e. only (cycles of) non-point-scoring
transitions are enabled.</p>
        <p>In either case, the game ends, and the team’s score (i.e. the total number of
transitions that were fired) is announced. In a competitive settings, the second
condition does not trigger the end of the game for the other team(s), but excludes
the one that reached a deadlock from remaining rounds. It is then only at the
end of the game time that the team with the highest number of fired transitions
is declared victorious.
2.7</p>
      </sec>
      <sec id="sec-2-7">
        <title>Refereeing</title>
        <p>In most games and sports there are situations where even the fairest players may
not reach consensus. In Petri sport, disputes over point counts or proper
completion of a transition firing can arise easily – in particular near the end of a game.
One or several impartial referees shall be appointed to settle these disputes. Such
referee(s) are also responsible for sanctioning illegal moves, usually resulting in
a rollback or sudden death. In case several referees are appointed, only one shall
have the right to dispense additional penalties, such as point and/or time
deductions, or rollback without timer suspension (i.e. time passes as the players
run back to last valid marking before the foul play), if deemed necessary. As in
any other sport, the ruling of a referee shall not be contested.
3</p>
      </sec>
    </sec>
    <sec id="sec-3">
      <title>Formal Definition</title>
      <p>Petri sport is played on a special kind of Petri nets, called sport Petri nets
(SpPN). Their definition has been carefully designed in order to keep the Petri
sport field as simple as possible, while still allowing complex behaviors.
3.1</p>
      <sec id="sec-3-1">
        <title>Sport Petri nets</title>
        <p>Sport Petri nets are a variant of classical Petri nets. Their most distinguishing
feature is that the global number of tokens is bounded. At the beginning of the
game a finite number of tokens is split into bound tokens (the initial marking)
and free tokens. When a transition is fired, bound tokens become free and free
tokens are bound according to preconditions and postconditions. The total
number (free + bound) of tokens within the system cannot increase. Every SpPN
can be converted into an equivalent place-transition net by adding a place for
free tokens and additional pre- and postconditions for each transition, as shown
in Figure 3. The following section will elaborate on the formal aspect of sport
Petri nets.</p>
        <p>We denote S as the set of all SpPN and define that each sport Petri net s 2 S
is composed of s = hP; T; pre; post ; f; ii.</p>
        <p>P
pre : P
post : T</p>
        <p>T ! N
P ! N
set of places
preconditions
postconditions</p>
        <p>T
f : N
i : P ! N
set of transitions</p>
        <p>free tokens
initial marking</p>
        <p>As typical for Petri nets, SpPN make use of two kinds of arcs: pre and post ,
defining the pre- and postconditions of transitions. Arcs are labeled with their
weight, i.e. a natural number defining the amount of tokens taken from a place
or put into it when firing a transition. Arcs with weight = 0 do not influence a
transition and are hence treated as non-existent.</p>
        <p>Markings A SpPN’s marking defines the number of tokens within each state
and the number of free tokens available. It is thus a function from places (and
the free tokens counter) to natural numbers: m : P [ ffreeg ! N. The marking
of a particular place is m(p) (for p 2 P ), and the number of free tokens is given
by m(free). The set M of all possible markings of an SpPN s is defined by M =
fm j m : P [ ffreeg ! Ng. The initial marking of the SpPN adds the number of
free tokens to m0. It is thus given by m0(free) = f ^ 8p 2 P; m0(p) = i(p).</p>
        <p>A few convenience functions render the below definitions more readable:
pre( ; t) and post (t; ) return the marking corresponding to the precondition
(respectively postcondition) of transition t, that includes the free tokens. + and
are addition and subtraction of markings. A special case of using the
operator is to remove a token from the set of free tokens: m ffree 7! 1g performs
this operation.</p>
        <p>8t 2 T; pre( ; t) =
8t 2 T; post (t; ) =
8p
&lt;
:
8p
&lt;
:
8p 2 P [ ffreeg; ml + mr = ml(p) + mr(p)
8p 2 P [ ffreeg; ml
mr = ml(p)</p>
        <p>(p
m
ffree 7! ng =</p>
        <p>7! m(p); 8p 2 P
free 7! m(free) n
3.2</p>
      </sec>
      <sec id="sec-3-2">
        <title>Operational Semantics</title>
        <p>SpPN’s semantics are provided in the remainder of this subsection. It is given
using inference rules written as follows, where the semantic domain is split into
three parts: input parameter output .
name:
h: : : i 2 input
rule( 2parameter)</p>
        <p>! h: : : i 2 output
The semantic rules and their domains are:</p>
        <p>transition : M
transaction : M</p>
        <p>T
T
(M
M
All rules take a marking as input and return a marking. The transition rule
is parameterized by the transition to fire, and returns a marker (&gt; or ?) of
validity of the firing. The transaction rule is parameterized by a sequence of
transitions to fire, T denotes a sequence of T .</p>
        <p>transition-correct and transition-incorrect are the firing rules for
individual transitions. They are parameterized by the transition t to fire, take
as input a marking (containing also the free tokens), and return the resulting
marking together with a marker (&gt;; ?) stating if the firing is correct.
transition-incorrect:
pre( ; t)
m; m0 = m</p>
        <p>pre( ; t) + post(t; )
hmi
pre( ; t) &gt; m _ m0 6= m
transition(t)
! hm0; &gt;i</p>
        <p>pre( ; t) + post(t; )
hmi
transition(t)
! hm0; ?i</p>
        <p>The transition-incorrect rule differs from most of the semantics given
for Petri nets, because it explicitly states to what constitutes an invalid firing
of a transition. There can be thus an infinity of markings m0 as output of this
rule. They correspond to all the firings of the transition where players do not
follow the firing rules of the Petri net, for instance by using less or more tokens
than expected, or tokens from or to wrong places. The failure marking m0 is not
reused in other semantic rules, the only important part of the result being the
? marker.</p>
        <p>transaction-empty, transaction-correct and transaction-incorrect
are the rules for transactions (sequences of transitions). A sequence is denoted
as t::s where t is the transaction’s first transition, and s the rest of the sequence.
[] denotes an empty sequence (i.e. no transitions).</p>
        <p>The transitions within a transaction are fired in sequence, the marking being
updated one by one. When the firing of a transition within a transaction fails
(returns ?), the remainder of the transaction is not performed. Instead, one free
token is removed, and the state remains in the last valid marking.
transaction-empty:
transaction-correct: hmi
transaction-incorrect:
hmi
transaction([])</p>
        <p>! hmi
transition(!t) hm0; &gt;i; hm0i transaction(s!) hm00i
hmi
hmi
transition(t)</p>
        <p>! hm0; ?i
transaction(t::s)</p>
        <p>! hm00i
hmi
transaction(t::s)
! hm
ff 7! 1gi</p>
        <p>This semantics is very abstract and close to the one for common Petri nets,
except for the handling of erroneous firings. It cannot express the parallel firing
of transitions, as it only allows sequences of firings. Additional rules are provided
in Section 3.3 to describe the detail of the SpPN evolution and in particular the
ability to fire simultaneously transitions.
3.3</p>
      </sec>
      <sec id="sec-3-3">
        <title>Concurrency, sudden-death and failures</title>
        <p>When playing Petri sport, several transitions can be fired in parallel during a
transaction. To describe the semantics of such firings, we do not provide the
usual parallel composition operator (jj), but instead decompose each transition
into two phases: 1. its resource acquisition phase, where the preconditions are
met and free tokens are reserved for the postconditions, 2. its resource release
phase where the actual firing happens. Parallel transitions are a sequence of
resource acquisition and release phases.</p>
        <p>The corresponding semantics thus works on traces, that explicitly list the
actions performed by the players and the environment. A trace is a sequence of
actions, each action can be one of the following:
– begin(t; m) representing the gathering of preconditions of the transition,
– end (t; m) representing the release of postconditions of the transition,
– beep for a beep from the timer, i.e. the end of one clock interval and start of
another.</p>
        <p>The semantics consider all possible traces, not only correct ones. I.e. there
are no guaranteed begin-end pairs, or there can be a beep before other actions.</p>
        <p>The relations and their domains are given as follows. All take at least one
marking as input and return at least one marking. The action subrule takes as
input and output a multiset of transitions, that have begun but not ended. It also
uses the action to perform, and returns a marker of success. The transaction
subrule takes as input the state in which the system is at the beginning of the
transaction. It is used for canceling the transaction. It also takes the multiset
of begun transitions. The rollback subrule is used to perform rollbacks, when
a part of a transaction is canceled, mainly because of sudden death. It takes as
parameter the multiset of begun transitions to rollback.</p>
        <p>A = fbegin(t; m) j t 2 T; m 2 M g
[ fend (t; m) j t 2 T; m 2 M g
[ fbeepg
action : (M
transaction : (M
rollback : M</p>
        <p>M(T ))
M
M(T )</p>
        <p>M(T ))</p>
        <p>M</p>
        <p>A
(M
A</p>
        <p>M(T )
Ms
f&gt;; ?g)
The multiset of values within a set S is written M(S). Operations defined on
sets are extended on multisets. For instance x n fyg only removes one occurrence
of y in x if x is a multiset.</p>
        <p>The following rules define the behavior of individual steps begin and end .
They are parameterized by the action to perform, take as input a marking and
the multiset of transitions that have only begun (those that have seen a begin but
no end ), and return the updated marking, the updated list of begun transitions,
and a success marker.
pre-correct:
post-correct:
m0</p>
        <p>m; m0 = pre( ; t)
hm; tsi
action(begin(t;m0))</p>
        <p>! hm m0; ts [ ftg; &gt;i
t 2 ts; m0 = post ( ; t)
hm; tsi
action(end(t;m0))</p>
        <p>! hm + m0; ts n ftg; &gt;i</p>
        <p>The following rules are similar, but define the behavior in case of incorrect
firing. Several problems are handled: the transition to fire can be disabled, the
firing can be incorrect because not enough or too many tokens are used, or a
transition is ended without having been begun.
pre-incorrect:
post-incorrect:</p>
        <p>m0 &gt; m _ m0 6= pre( ; t)</p>
        <p>When a transaction comes to its end (there are no more actions to perform),
it is validated by looking at the transitions that are still not ended. If one such
transition remains, there is an incorrect behavior, leading to a sudden death.
This rule does not handle the case where a beep occurs, but instead the case
where players have forgotten to perform the postcondition.
empty-correct:
empty-incorrect:
hmi ; m; tsi</p>
        <p>ts = ?
ts 6= ?; hmi
transaction([])
! hmi
rollback(ts)</p>
        <p>! m0
hmi ; m; tsi
transaction([])
! hm0
ffs 7! 1gi</p>
        <p>The firing of a transaction performs actions one by one. If one action fails,
the marking is restored to its value before this transition, all currently begun
transitions are rolled back, and a sudden death occurs after the rollback. This
information about when the sudden death occurs is important as the free players
may change between the rollback. Note that in these semantics the sequence
consists of actions rather than transitions (as in the one above).
transaction-correct:
transaction-incorrect:</p>
        <p>action(x!) hm0; ts0; &gt;i; hmi ; m0; ts0i transaction(s!) hm00i
rollback is used to rollback all transitions that have begun but not ended.
rollback-empty:
hmi
rollback-nonempty:
hm + pre( ; t)i
rollback(ts)</p>
        <p>! hm0i
hmi
rollback(ftg[ts)</p>
        <p>! hm0i</p>
        <p>At the beginning of each transaction, the set of transaction relation is used
with hmi; m; tsi = hm; m; ?i, where m is the state of the sport Petri net at the
beginning of the transaction. When starting the game, this state is m0.</p>
        <p>All transactions that are correct while playing Petri sport are also correct
within the sequential semantics and the parallel one. The only difference
between the two semantics is that the sequential one transforms parallel firings
into sequences. Similarly, all transactions that are incorrect while playing Petri
sport are also incorrect within the two semantics (except for beep which is not
represented in the sequential semantics). Erroneous firings explicitly represented
in the parallel semantics are handled by the transition-incorrect rule of the
sequential semantics.</p>
        <p>According to the semantics, the marking graph of a sport Petri net can be
computed, but may be infinite when using the simple semantics without
concurrency, or when dealing with infinite transactions. In all other cases, assuming
that the number of free tokens acts as a bound, the marking graph is guaranteed
to be finite. In addition, the bound of the SpPN is lower than the sum of the
initially bound tokens and the initially free tokens.
4</p>
      </sec>
    </sec>
    <sec id="sec-4">
      <title>Game Variants</title>
      <p>There are two ways in which the rules of Petri sport can be modified, so as
to suit more experienced players or provide interesting, alternative play styles.
The first focuses on the semantics of the underlying Petri net formalism. In the
previous sections, we presented a semantics based on classic (black token) Petri
nets. But Petri sport can very well be adapted to borrow concepts from Petri net
extensions, such as colored tokens, inhibitor arcs and similar. Evidently, the rules
of a particular flavor of Petri net that would include these extensions must be
changed accordingly. For instance, one could imagine assigning colors to players,
and designing postconditions so that the number and/or color of the free players
that could satisfy them would depend on the number and/or color of the players
who satisfied the precondition.</p>
      <p>For spatial reasons, we cannot delve deeper into that direction, and therefore
will not provide a precise semantical specification of these concepts. Instead, the
remainder of this section will focus on a second way of modification: the rules of
the game itself. In particular, we will show how minor modifications can create
interesting variants to accommodate different play styles.
4.1</p>
      <sec id="sec-4-1">
        <title>No sudden death</title>
        <p>As described above, the sudden death rule changes Petri sport’s semantics with
regards to the Petri net formalism. We noticed that novice players still unfamiliar
with the formalism, often find it difficult to adapt their strategy in function
of a variable number of free players. Our experiences have shown that it may
sometimes be advantageous to remove the sudden death rule, replacing it with
other kind of penalties, such as deductions to the available time or awarding
of negative points. This allows players to become familiar with the formalism,
before having to process more elaborate considerations, such as a potential loss
of available players.
4.2</p>
      </sec>
      <sec id="sec-4-2">
        <title>Exponential points</title>
        <p>According to the rules presented above, teams are rewarded if they successfully
fire several transitions in a given time span. Unfortunately, in complex SpPN
designs which require elaborate team coordination, teams might be tempted to
play safely and avoid firing long sequences. Indeed, the risk of losing free players
under sudden death might discourage teams to try more difficult moves.</p>
        <p>This problem can sometimes be overcome without resorting to a complete
game redesign. By simply awarding a number of points exponential to the
number of fired transitions during a single clock phase the reward for risk becomes
higher. For instance, one could imagine awarding a single point for the first fired
transition, but then multiplying this number for each subsequent transition (e.g.
two points for the next one, four points for the following, etc.) Such a
rewarding scheme encourages more risky behavior and creates games with a higher
“gambling” character.
4.3</p>
      </sec>
      <sec id="sec-4-3">
        <title>Multi-point transitions</title>
        <p>In a usual game, the number of points grows quickly. A standard 5-minute game
with a 15 second base clock provides 20 intervals. Considering that in each
interval multiple transitions may be fired in parallel and/or in sequence, it is
easy to see how scores can quickly reach high numbers. By itself, this is not
necessarily bad game design, but can make it harder for teams to properly think
out their strategy. Moreover, counting fired transition can prove quite difficult
with respect to refereeing, in particular remembering that transitions may be
fired in parallel.</p>
        <p>So as to ease these aspects, one possible adjustment is to assign a
particular value to each transition, or a subset thereof. For instance, this could mean
awarding points only if one or several specific transitions are fired, while firing
other transitions would not impact the score. An indirect advantage of this
variant is that it enables the design of play fields that feature a complex sequence of
transition, requiring higher efforts (e.g. long running distances), but whose firing
is extremely rewarding. This can also encourage teams to find the quickest ways
to repeatedly reach valued transitions.</p>
        <p>We also introduce multi- and high-value transitions. By firing these special
transitions teams are rewarded with a point multiplier (i.e. doubles the amount
of points scored in the current clock interval). Typically such transitions require
an elaborate team coordination. Game designers are encouraged to make it hard
to enable such transitions and/or repeatedly execute them.
4.4</p>
      </sec>
      <sec id="sec-4-4">
        <title>Colors</title>
        <p>While the variants above represent small modifications of the game, we also
looked into teaching more complex flavors of Petri nets. In particular, we
extended Petri sports to include colors. In color Petri sports, tokens and free players
have access to colored shirts/bibs. Wearing a shirt identifies the player as token
of a certain color. Each bound player is associated with one specific color which
cannot change until freed. Free tokens are color-less and can choose to become
any one of the game colors when they participate in a transition. In each game
round the game organizers can decide for each color whether it is bounded, i.e.
there is maximum number of tokens in a certain color (and hence shirts/bibs),
or unbounded (there should be as many bibs of that color as number of players.
This game variant significantly changes the original Petri sport semantics. For
spatial reasons we cannot provide the semantics of this modification.
Puzzle mode is a modification of Petri sport that reduces the physical aspect of
the game. We consider games of this style to be a kind of intellectual exercise.
In puzzle mode, the field provides a difficult problem and requires players to
find a sequence of transitions that will allow the reaching of a certain goal.
This goal can be the enabling and firing of a certain transition, or the reaching
of a predefined marking. The teams participating will find themselves directly
competing against each other. This means that a before unknown playing field
and/or winning condition will be presented to all teams at the same time. The
teams can attempt to solve the puzzle on a first-come-first-served basis. The first
team to find the solution wins the round. If a team attempts and fails, it is not
allowed to try again in the same round. A positive trait of this game variant is
that it can also be played by a single team individually. In this case the goal can
be to check if the reaching of the goal is possible in the first place, rather than
finding the solution fast.
5</p>
      </sec>
    </sec>
    <sec id="sec-5">
      <title>Quality metrics</title>
      <p>In order to assert the quality of Petri sport we developed guidelines to help the
design of sport Petri nets. Below, we elaborate on some quality aspects of SpPN.
The suggestions however do not guarantee good SpPN design. It is possible
to create an entertaining SpPN that violates some of these rules or create an
adhering SpPN that is not playable.</p>
      <p>Formally expressed, a SpPN should allow users to fire transitions without
reaching deadlock situations. This means that there should be a sequence of
transitions (a path) whose execution takes longer than the predefined playing
time. It has to be taken into account that transitions are only fired between
beeps, but that it is possible to fire multiple transitions at once. It should further
be considered that the duration of a transition firing depends on its complexity,
i.e. how many players from how many places are involved, and the physical length
of the arcs. Usually the firing of two to three transitions within one beep-interval
supports entertaining games.</p>
      <p>For the overall entertainment we expect that variety is asserted by making
it possible to reach many different game states (markings). In practical terms
we recommend that in most game states there should be at least two transitions
enabled that lead to different new markings.</p>
      <p>Obviously, the presence of deadlocks increases the excitement potential. They
should however be sparsely used, in order to keep a good game flow [HSR+16].</p>
      <p>In terms of team size, game organizers should keep in mind that the sudden
death penalties might easily remove some players for the current game round.
This means that team sizes should be chosen so that the playability is kept up
even during the loss of players.</p>
      <p>Playability We define that playability is the set of metrics that give information
about the suitability of a SpPN for Petri sport. Examples of unsuitable SpPN
include nets that do not have enough free tokens to fire any transition, or do
not contain cycles in their state space. These measures are mostly related to
standard Petri net key figures such as path length, size of state space, etc.
Entertainment potential Entertainment potential is a measure of how interesting
it should be to play a SpPN. In order to standardize this rather subjective
figure, we try to provide objective characteristics for evaluation. We propose the
following metrics to assess the entertainment potential of a SpPN. All properties
are decidable on a finite marking graph.</p>
      <p>Number of states A SpPN with only a few reachable states is not interesting,
because players will repeat the same actions over and over.</p>
      <p>How many deadlock states? A SpPN should contain the risk of being trapped
in a deadlock in order to keep the players focused on the game.</p>
      <sec id="sec-5-1">
        <title>Number of states leading only to deadlocks States leading only to dead</title>
        <p>locks are not of interest since players cannot escape. The number of such
states should thus remain low, compared to the total number of states.</p>
      </sec>
      <sec id="sec-5-2">
        <title>Number of enabled transitions per state Having more than two enabled</title>
        <p>transitions allows the players to choose which one to fire. They have to make
a decision and coordinate, which makes the game more fun.</p>
      </sec>
      <sec id="sec-5-3">
        <title>Number of parallel transitions per state Firing several transitions in par</title>
        <p>allel is a risk in the SpPN, because it allows players to gain more points, but
at the increased risk of sudden death, because coordination is more difficult.
Thus, allowing parallel transitions in most of the states is a good practice.</p>
        <p>The petrisport tool2 is provided to game organizers to help the analysis of
the game and hence provide indicators for playability and entertainment
poten2 https://github.com/cui-unige/petrisport
tial. The tool calculates these characteristics based on a sport Petri net provided
in the PNML format.</p>
        <p>Evaluation of the example Figure 6 shows some characteristics of the SpPN in
Figure 4 as computed by the petrisport tool. The histograms show the ratio
between the number of states that have a property and the total number of states
in the marking graph. In total three characteristics are displayed as histograms:
1. choice ratio expresses the fraction of system states that offer at least two
enabled transitions, 2. parallel ratio considers the states that can fire at least
two transitions in parallel, 3. deadlock ratio shows the states that can only lead to
deadlocks. Line plots show the mean number of enabled transitions and parallel
firings in each state.</p>
        <p>The analysis of the SpPN of the example shows that it can be fun starting
from 6 free tokens (thus 8 players in total). As sudden death may occur during
the game, we recommend to start the game with 10 or 12 players, in order to
avoid reaching the less entertaining token numbers too soon.</p>
        <p>0
1
2
3
4</p>
        <p>5
choice ratio
parallel ratio
deadlock ratio
6</p>
        <p>7 8
Free players
9</p>
      </sec>
    </sec>
    <sec id="sec-6">
      <title>Experimental Evaluation</title>
      <p>Petri sport has been successfully played at the University of Geneva. In this
section we present initial experiment results and participant reactions after playing.
Note, that these results are preliminary: the feedback has been captured using
a simple, anonymous questionnaire and represents the participants’ opinions of
the game. So far, there was no controlled experiment that formally attempts to
measure the impact Petri sports has on students’ knowledge or academic success.
100
o
ita 50
R
0
4
2
0
n
a
e
M
Methodology We played the game with undergraduate (Bachelor’s degree) and
graduate (Master’s degree) students who learned about, and used Petri nets in
previous academic courses before playing the game.3</p>
      <p>Participants were taught the rules of the game gradually, by introducing the
different notions one by one. The introduction was played on the “introductory”
SpPN (Figure 7), which while simple exposes all interesting concepts, such as
source and sink transitions, split, merge and synchronization. Each notion was
introduced by a short theoretical information followed by some practice. We
proceeded in the following steps:
1. We introduced the basic concepts (i.e. movements along the arcs, firing
transitions, consumption and production of tokens).
2. We introduced the synchronization mechanisms for transitions involving
multiple preconditions.
3. We invited the students to do trial play without timing.
4. We introduced the clock-based system (i.e. transition have to finish before
interval end).
5. We introduced the penalty system (i.e. the reset rule and sudden death
rules).
6. We invited the students to a practice round with all rules in full-force.
7. We carried out a competitive round.</p>
      <p>Since the team sizes were held minimal to allow multiple competitive teams, the
experiments were played using the no-sudden-death variant, where faulty firing
leads to a reset of the transition.</p>
      <p>After an initial round on the “introductory” SpPN, the participants were
given a picture of a second, more complex SpPN (depicted in Figure 4, above).
Following a few minutes of study, and one minute of setup, the teams were left
to play the game in two rounds. In the former, students were left to play without
additional instructions, while in the latter they were encouraged to target the
outer transition with the longer running paths and try to score higher than
before. The complete session lasted about 90 minutes.</p>
      <p>Evaluation Following the experiment, the students answered a short survey
where they answered questions using a five-valued scale from 0 (disagree) to
5 (agree) and open answers. While a full discussion would exceed the scope of
this publication, we will summarize the most important feedback.</p>
      <p>Most students enjoyed playing Petri sports, independent of their familiarity
with the formalism. Additionally, despite having already completed at least one
course, almost all students responded to having learned “a bit” more about Petri
nets while playing the game. About half of the students felt that playing Petri
sports would have strongly helped them understand Petri nets when they first
came in contact with the formalism. When asked whether Petri sports should be
included into the undergraduate course that first introduces Petri nets, students
provided mixed answers. About half of the participants were interested in using
the game as a means to learn about Petri nets.
3 We have yet to experiment with complete novices.
Discussion The results we obtained encourage us to continue using Petri sports
as a means of teaching. Petri sports positions itself as a fun addition to classical
lectures and allows us the playful introduction of Petri net concepts. We do see
however, that the students’ learning types and opinions on alternative teaching
methods differ largely and traditional classroom methods cannot be replaced.
t0
p0
t1
t2
p1
p2
2
t3
t4
p3
Fig. 7: Introductory sport Petri net that can be used as a tutorial. Teams of
at least five players can learn about source/sink transitions, synchronization,
splitting and merging.
7</p>
    </sec>
    <sec id="sec-7">
      <title>Related Work</title>
      <p>The use of games for education purposes is a hot topic in the didactics domain
[EGCN+11,SPS05]. In particular, approaches based on games met remarkable
success in the context of teaching activities, in the form of classroom games.
Also interesting to note is the surge of toys, games and other applications that
aim at teaching algorithmic thinking – or similar concepts – to young
students [Sqi05,RMMH+09,Boe17]. The use of (digital) games for other purposes
than pure entertainment (e.g. education, training, activism, health awareness,
etc.) is referred to as serious gaming [MC05]. This relatively new domain
explores how to best design games so that the learning experience is as natural
and efficient as possible, while maximizing the entertainment aspect to make
solutions attractive to young audiences [EN11].</p>
      <p>The omnipresence of personal computers, gaming consoles and smartphones
also pushes people of all demographic groups to disrupt traditional learning
approaches. The number of mobile applications and online platforms seeking to
teach about subjects like (spoken) languages, geography or biology is growing
by the day. Despite the reluctance of some professionals at first, their relevance
has became undeniable [VG12].</p>
      <p>For nearly a decade now, our group has embraced such untraditional
approaches for its teaching activities, and in the context of campaigns promoting
university studies. We conducted projects with LEGO robots to introduce
formal verification concepts [LRC+14], illustrated formalisms and algorithms with
more common and familiar concepts such as cooking [LR16], and used 3D printed
devices to concretize otherwise abstract notions such as memory or
communication [RB18].
8</p>
    </sec>
    <sec id="sec-8">
      <title>Conclusion and Future Works</title>
      <p>This paper presents Petri sports, a novel approach to teaching the Petri net
formalism to domain novices. Petri sports is motivated by the experience that
classroom Petri net teaching often leads to misunderstandings and an increased
need for practice and exercise with the formalism. Through gamification, we
created Petri sports which allows students to “act as” Petri net tokens and thereby
access an additional learning method. Petri sports uses the standard Petri net
syntax to design playing fields and its semantics to prescribe movement of
players across the pitch. Additional rules bound the number of tokens, and ensure
intellectual challenges through sudden death and rollback penalty rules. All Petri
sports rules are based on the formalization provided and allow for programmatic
analysis of game characteristics (such as detection of deadlock reachability, etc.)
as shown in this paper. Petri sports is extensible and adaptable to best serve the
participants’ knowledge, physical abilities and preferences. The paper presents
several game variants to classical Petri sports and briefly introduces colored Petri
sports, puzzle mode and other variations to the game.</p>
      <p>The experimental results presented in this paper show that , our While our
basic work shows good results in the classroom, we plan to extend Petri sports
in several ways:
1. We use numerous game variants to explain various advanced Petri net
concepts (inhibitor arcs, colored Petri nets, etc.). We are in the process of
creating a catalog thereof, categorically documenting specific rules, semantics
and educational success.
2. As we observe good results, we would like to spread Petri sports to other
institutions and learn from their experiences as well.
3. Petri sports shows the success of gamification concepts in Petri net teaching.</p>
      <p>We are currently evaluating whether other gaming styles (such as mobile
or browser games) can be used to teach Petri nets. An early stage mobile
application project can be found on our group’s blog4.
4. In parallel to the above extension of Petri net teaching, we also evaluate
whether other formal methods domains can be taught more easily using
such alternative forms of teaching.
5. We are planning to perform evaluations together with experts in the
didactic domain, in order to evaluate the teaching success of Petri sports more
formally.
4 https://cui-unige.github.io/blog-smv/2018/03/26/petri-ios/</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          <string-name>
            <given-names>Boe17. Benjamin</given-names>
            <surname>Boettner</surname>
          </string-name>
          .
          <article-title>Harvards wyss institute launches root robotics, an educational startup to get anyone coding</article-title>
          ,
          <year>Aug 2017</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          <source>EGCN+11</source>
          .
          <string-name>
            <surname>Alejandro</surname>
            <given-names>Echeverria</given-names>
          </string-name>
          , Cristian Garcia-Campo, Miguel Nussbaum, Francisca Gil, Marco Villalta, Matias Améstica, and
          <string-name>
            <given-names>Sebastian</given-names>
            <surname>Echeverria</surname>
          </string-name>
          .
          <article-title>A framework for the design and integration of collaborative classroom games</article-title>
          .
          <source>Computers &amp; Education</source>
          ,
          <volume>57</volume>
          (
          <issue>1</issue>
          ):
          <fpage>1127</fpage>
          -
          <lpage>1136</lpage>
          ,
          <year>2011</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          <string-name>
            <surname>EN11. Simon</surname>
          </string-name>
          Egenfeldt-Nielsen.
          <article-title>What makes a good learning game?: Going beyond edutainment</article-title>
          . eLearn,
          <year>2011</year>
          (2),
          <year>February 2011</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          <source>HSR+16</source>
          .
          <string-name>
            <surname>Juho</surname>
            <given-names>Hamari</given-names>
          </string-name>
          , David J Shernoff, Elizabeth Rowe, Brianno Coller, Jodi Asbell-Clarke, and
          <string-name>
            <given-names>Teon</given-names>
            <surname>Edwards</surname>
          </string-name>
          .
          <article-title>Challenging games help students learn: An empirical study on engagement, flow and immersion in game-based learning</article-title>
          .
          <source>Computers in Human Behavior</source>
          ,
          <volume>54</volume>
          :
          <fpage>170</fpage>
          -
          <lpage>179</lpage>
          ,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          <string-name>
            <surname>Jen14. K. Jensen</surname>
          </string-name>
          .
          <source>Coloured Petri Nets: Basic Concepts</source>
          ,
          <source>Analysis Methods and Practical Use</source>
          .
          <article-title>Number v. 1 in Monographs in Theoretical Computer Science</article-title>
          .
          <source>An EATCS Series</source>
          . Springer Berlin Heidelberg,
          <year>2014</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          <string-name>
            <surname>Kap12. Karl M Kapp.</surname>
          </string-name>
          <article-title>The gamification of learning and instruction: game-based methods and strategies for training and education</article-title>
          . John Wiley &amp; Sons,
          <year>2012</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref7">
        <mixed-citation>
          <string-name>
            <given-names>LR16. David P.Y.</given-names>
            <surname>Lawrence</surname>
          </string-name>
          and
          <string-name>
            <given-names>Dimitri</given-names>
            <surname>Racordon</surname>
          </string-name>
          .
          <article-title>Cooking with algorithms</article-title>
          . https://www.youtube.com/watch?v=aDtq_bLXKvI,
          <year>2016</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref8">
        <mixed-citation>
          <source>LRC+14</source>
          . David Lawrence, Dimitri Racordon, Maximilien Colange, Steve Hostettler, Alban Linard, Edmundo Lepez Bobeda, Alexis Marechal, Matteo Risoldi, Nicolas Sedlmajer, and
          <string-name>
            <given-names>Didier</given-names>
            <surname>Buchs</surname>
          </string-name>
          .
          <article-title>Introducing formal verication with lego</article-title>
          .
          <source>In 2nd workshop on Fun With Formal Methods</source>
          , Vienna, Austria, July
          <volume>13</volume>
          ,
          <year>2014</year>
          , Proceedings,
          <year>2014</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref9">
        <mixed-citation>
          <string-name>
            <given-names>MC05. David R.</given-names>
            <surname>Michael</surname>
          </string-name>
          and
          <string-name>
            <surname>Sandra L. Chen</surname>
          </string-name>
          . Serious Games: Games That Educate, Train, and
          <string-name>
            <surname>Inform</surname>
          </string-name>
          . Muska &amp; Lipman/Premier-Trade,
          <year>2005</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref10">
        <mixed-citation>
          <string-name>
            <surname>Pet62. Carl Adam</surname>
          </string-name>
          <article-title>Petri</article-title>
          . Kommunikation mit Automaten.
          <source>PhD thesis</source>
          , Universität Hamburg,
          <year>1962</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref11">
        <mixed-citation>
          <string-name>
            <given-names>RB18. Dimitri</given-names>
            <surname>Racordon</surname>
          </string-name>
          and
          <string-name>
            <given-names>Didier</given-names>
            <surname>Buchs</surname>
          </string-name>
          .
          <article-title>Démystifier les concepts informatiques par l'éxpérimentation</article-title>
          . In Didapro 7 - DidaSTIC, De 0 à 1 ou l'heure de l'informatique à l'école, Lausanne, Switzerland, February 7-
          <issue>9</issue>
          ,
          <year>2018</year>
          , Proceedings,
          <year>2018</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref12">
        <mixed-citation>
          <source>RMMH+09</source>
          .
          <string-name>
            <surname>Mitchel</surname>
            <given-names>Resnick</given-names>
          </string-name>
          , John Maloney, Andrés Monroy-Hernández, Natalie Rusk, Evelyn Eastmond, Karen Brennan, Amon Millner, Eric Rosenbaum, Jay Silver, Brian Silverman, and
          <string-name>
            <given-names>Yasmin</given-names>
            <surname>Kafai</surname>
          </string-name>
          .
          <article-title>Scratch: Programming for all</article-title>
          .
          <source>Commun. ACM</source>
          ,
          <volume>52</volume>
          (
          <issue>11</issue>
          ):
          <fpage>60</fpage>
          -
          <lpage>67</lpage>
          ,
          <year>November 2009</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref13">
        <mixed-citation>
          <string-name>
            <surname>SPS05. Julia Shaftel</surname>
          </string-name>
          , Lisa Pass, and Shawn Schnabel.
          <article-title>Math games for adolescents</article-title>
          .
          <source>TEACHING Exceptional Children</source>
          ,
          <volume>37</volume>
          (
          <issue>3</issue>
          ):
          <fpage>25</fpage>
          -
          <lpage>30</lpage>
          ,
          <year>2005</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref14">
        <mixed-citation>
          <string-name>
            <given-names>Sqi05. Kurt</given-names>
            <surname>Sqire</surname>
          </string-name>
          .
          <article-title>Changing the game: What happens when video games enter the classroom? Innovate: Journal of online education, 1(6</article-title>
          ):
          <fpage>5</fpage>
          ,
          <year>2005</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref15">
        <mixed-citation>
          <string-name>
            <given-names>VG12. Roumen</given-names>
            <surname>Vesselinov</surname>
          </string-name>
          and John Grego.
          <article-title>Duolingo effectiveness study</article-title>
          . City University of New York, USA,
          <year>2012</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref16">
        <mixed-citation>
          <string-name>
            <surname>Zai14. D.</surname>
          </string-name>
          <article-title>A. Zaitsev. Toward the minimal universal petri net</article-title>
          .
          <source>IEEE Transactions on Systems, Man, and Cybernetics: Systems</source>
          ,
          <volume>44</volume>
          (
          <issue>1</issue>
          ):
          <fpage>47</fpage>
          -
          <lpage>58</lpage>
          ,
          <year>Jan 2014</year>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>