This paper presents a set of strategies to solve global behavioral properties of Petri nets. We introduce eficient methods to compute structural invariants and bounds, and to decide presence of stable places for both PT nets and colored nets. Our focus is on proposing strategies that scale to very large nets, even if precision is degraded or the test is only a semi-decision (e.g. a suficient condition). These strategies form the decision procedures of ITS-Tools, that has won the annual model-checking competition MCC in these categories in both 2021 and 2022.
The structure of the paper is the following, we first set the basic definitions and notations used in the paper Then for each property of interest, we present in detail a series of structural or low complexity suficient or necessary condition that can be tested. If these preliminary strategies cannot conclude, we use a more complete model-checker but we limit as much as possible the number of queries that we pose to the model-checker. We discuss computation of invariants in section 3, then computation of bounds on place markings in section 4. This leads to decision procedures for the one safe property in section 5. Finally we present strategies to decide the stable marking property, i.e. are some place marking constant, in section 6.
We first recall the definitions of a Petri net, then we informally introduce the notion of colored net (also called "High Level Petri Net") with its unfolding and skeleton.
Definition 1. Structure. A Petri net = ⟨P, T , W−, W+, 0⟩ is a tuple where P is the set of places, T is the set of transitions, W− : P × T ↦→ N and W+ : P × T ↦→ N represent the pre and post incidence matrices, and 0 : P ↦→ N is the initial marking.
Notation: We use (resp. ) to designate a place (resp. transition) or its index dependent on the context. We let markings be manipulated as vectors of natural numbers with |P | entries. We let W− () and W+ () for any given transition represent vectors with |P | entries. W−⊤, W+⊤ are the transposed flow matrices, where an entry W−⊤ ( ) is a vector of |T | entries. We denote W = W+ − W− the integer matrix representing transition efects .
In vector spaces, we use ≥ ′ to denote ∀, () ≥ ′ (), and ofer sum + ′ and multiplication of a vector by a scalar · for scalar with usual element-wise definitions.
We denote • (resp. •) the pre set (resp. post set) of a node (place or transition). E.g. for a transition its pre set is • = { ∈ P | W− ( , ) > 0}. A marking is said to enable a transition if and only if ≥ W− (). A transition is said to read from place if W− ( , ) > 0 ∧ W ( , ) = 0. Definition 2. Semantics. The semantics of a Petri net are given by the firing rule →− that relates pairs of markings: in any marking ∈ N| P |, if ∈ T satisfies ≥ W− (), then →− ′ with ′ = + W+ () − W− (). The reachable set R is inductively defined as the smallest subset of N| P | satisfying 0 ∈ R, and ∀ ∈ T , ∀ ∈ R, →− ′ ⇒ ′ ∈ R.
A colored or high-level Petri net is similar to a Petri net structurally, but each place now has a domain ( ) and place markings are a multiset (or bag) over this domain. Similarly, an arc touching a place will bear a color function that itself resolves to a multiset over the domain of the place. Finally, transitions come equipped with a guard that can forbid or enable the transition depending on the type of tokens present in the connected places.
We avoid providing a formal definition of a colored net here, we recommend [
This operation has a very low complexity, but yields a net whose behaviors are a strict superset of the behaviors of the original colored net : the skeleton net can do anything that the original net could do, and more. Hence if the skeleton net is unable to reach a certain behavior, the original net cannot reach it either.
The process of calculating the structural invariants of a Petri net, also known as flows, is based on
an analysis of the incidence matrix (efects) of a net. The strategy is well known, it essentially
consists in applying Farkas’s lemma to an extended matrix [
This section presents the precise variant of this algorithm used within ITS-Tools. Our
implementation is in plain Java, and is based on source-code we took and adapted from the
APT [
To store a vector we use a sparse array data structure, containing two integer arrays indexes
and values both of size the number of non zero entries in . Indexes are maintained
sorted, values can never be 0. For instance vector = [
To store matrices we use a dynamically allocated array (ArrayList in Java) of sparse arrays representing the columns of the matrix. So this structure is "semi sparse", each column has an entry in the matrix even if it is empty. Transposition is possible with complexity proportional to the number of non zero entries (exploiting the fact that appending to a sparse array is (1)).
We initialize the algorithm by computing the matrix W′ : • Let W designate the efects matrix where columns are transitions and places are rows • We first build a set from the normalized columns of W; a set so elements are unique, and normalized by dividing all entries in the vector by the greatest common divisor of its entries. These operations will discard transitions identical up to a multiplicative factor on arc inscriptions, as well as fuse any two transitions that difer only by "read" arcs, i.e. that have the same efect but diferent enabling conditions. Applying this normalization step is a new idea to the best of our knowledge. • We then rebuild a matrix from this set (column order being unimportant), and finally transpose it to obtain the input W′ of the next step where rows are transitions and columns are places. • We then compute for each row of the W′ matrix the set of indexes that correspond to strictly positive and strictly negative entries. This data structure is stored in a variable and updated during the computation. This structure is important to stay in complexity related to non zero entries when working with a row index, so that we can directly find the columns that contain non zero values in this row.
Our goal in the next step is to empty the matrix W′, by replacing columns in the matrix by linear combinations of other columns until we converge to a matrix only containing zeroes. Basically we choose a row with some non zero entries in it, we then pick a column where the row has a non zero entry [ ], and replace all other columns that have a non zero entry in the row with a linear combination of columns and with coeficients chosen so that [ ] is set to 0. We then discard column .
After each such step, another row in the matrix is nullified, so that convergence is ensured in a polynomial number of steps. Progress is tracked by applying the same operations to an identity matrix, from which invariants (if any) can be read directly at the end of the procedure. This setting is classical, but we focus on only using sparse operations.
Let designate the identity matrix with dimension equal to the number of columns in W′ (i.e. the number of places in the net). We initialize a square matrix = .
We then iterate the following procedure until the W′ matrix is empty : • Find a row in the matrix such that exactly one entry is strictly negative or positive. We use to test this. If such a row exists : – Let designate the index of the single strictly positive (resp. negative) entry in .
Then for all , ≠ , such that [ ] < 0 (resp. strictly positive), ∗ First compute = ( | [ ] |, | [ ] |), then the coeficients = | [ ] |/ and = | [ ] |/. We then replace column of W′ by column = · W′ [ ] + · W′ [ ]. While computing , we can compute indexes of rows ′ where W′ ( ) [ ′] ≠ [ ′], and use this information to (sparsely) update . ∗ We then also replace the column ( ) of index in by ( ) = ·( ) + · ( ). – Finally we clear the column of W′, updating (sparsely, based on non zero values of W′ ( )), and clear column of . Note we use the term "clear" deliberately here, it is much preferable to set all entries to zero in a sparse data structure than actually removing a column (and requiring to reindex elements with greater indices non sparsely in ). Note that empty columns are irrelevant with respect to our algorithm, and induce almost no extra cost with sparse data structures. • If no such "exactly one entry is strictly negative or positive" row exists in W′, we look for a row in W′ such that there exists an index such that [ ] ≠ 0.
– While technically any such entry is appropriate, heuristically we want to choose a position that minimizes subsequent iterations of the algorithm. We currently orient this choice by looking for the column with index in W′ that has the least non zero entries (reducing the number of subsequent operations, and fast to test with sparse structures ), and in case of equality by taking the column with smallest summed absolute value ∑︁ |W′ ( ) | (reducing the risk of coeficient blowup). – Given , we let designate a row of W′ such that [ ]! = 0. We can choose any such row without impacting performance of the algorithm, so we simply take the first non zero entry in column of index . – Using to identify them we then iterate over all other non zero entries of : let designate such an entry ( ≠ , [ ] ≠ 0), and = ( [ ], [ ]) designate the greatest common divisor of these entries.
∗ Let = | [ ] |/. Let = [ ]/ if [ ] and [ ] have opposite sign, or = − [ ]/ otherwise. We then replace column of W′ by a new column = · W′ ( ) + · W′ ( ). During this product, and similarly to above we should (sparsely) update the data structure.
∗ We then replace the column ( ) of index in by ( ) = ·( ) + ·( ). – Finally we clear column from both W′ and (and update ). • Note that we must iterate the procedure to a fixpoint. We end the procedure when W′ is empty hence none of the two above rules apply. We always iterate the search for an appropriate row for the first test by iterating the rows in starting from the last row index where a rule applied rather than starting from row 0, as this avoids repeating redundant tests in most cases (and iterating elements in is not sparse).
At this stage, the W′ matrix has been entirely emptied, and we can find the invariants in the matrix. We can post process the columns of by dropping empty columns, normalizing columns (by dividing by the gcd of its entries, and possibly multiplying the column by −1 if all entries are negative), and filtering any duplicate columns.
This algorithm produces a generative basis of the P-flows of the net, but can be applied to W⊤
if we wish to compute T-flows. This basis of flows can further be used to compute semi-flows [
Notes: The idea of first looking for rows with a single positive/negative entry comes from
PIPE [
In this section we evaluate the performance of our implementation of this algorithm. We chose as
comparison the tool Tina [
The following performance evaluation 1 was performed on a Linux machine intel Core 7. We used the full set of 1384 PT models from the 2022 edition of the model-checking contest and computed P flows and T flows with both tools. The following table as well as Figure 3 summarize the results. The column "Overflow" corresponds to integer overflowing in the representation of the coeficients in the matrix. "Timeout" corresponds to exceeding the 120 seconds time limit, and "Memory" is runs exceeding 16GB of RAM.
Tool Success Overflow Timeout Memory ITS-Tools 1355 20 9 0 Tina 4ti2 1215 1 157 7
Tina 948 145 289 1
While in a few cases (16 overall) we meet integer overflow when Tina can produce a solution
(particularly with 4ti2), problems ITS-Tools can’t solve within one second are mostly unsolvable
by Tina, and our implementation is extremely memory eficient (peaking at 3GB) despite being
pure Java. Our implementation thus outperforms Tina [
Run time to compute PFlow+TFlow as reported by tools Resident shared size to compute PFlow+TFlow as reported by time
The goal of this task is to compute the maximum number of tokens in a place or group of places that can actually be reached. Our approach consists in computing both a lower bound Maxseen that represents the highest number of tokens actually confirmed to have been seen in this place or group of places and an upper bound Maxstruct that represents a structural maximum that the marking cannot exceed. When both values are equal, we can conclude, this value is the bound on this place marking.
For instance, suppose we must compute the bounds on expression 0 + 1. Suppose that in the initial marking, 0 = 1 and 1 = 0, so that Maxseen is 1. If we can compute an invariant that states 0 + 1 + 2 = 1, we can deduce that Maxstruct is also 1, so that the bound of 0 + 1 is 1.
For the lower bound Maxseen, we can simply explore (parts of) the state space, remembering the highest value encountered. For the upper bound Maxstruct, we seek to compute structural bounds if we can, rather than relying on an exhaustive exploration of the state space.
As a first step, we compute rough upper bounds on reachable markings using P flows. We first compute the P-flows, using the algorithm presented in section 3.
The solution can naturally contain some positive invariants (semi-flows) that we integrate first. Such an invariant is of the form : 0 0 + 1 1 + . . . = with alpha coeficients and being natural integers in N. Since at best all variables are 0 except one of them, we can compute an approximate upper bound on each place marking with a non zero coeficient in the invariant as / where / designates Euclidean division. For instance, suppose we have the invariant 2 ·0 + 3 = 5, we can deduce that 0 ≤ 2 and 3 ≤ 5.
Now that at least some variables have an upper bound, we can look at generalized flows with both positive and negative coeficients. We write them under the form (0 0 + 1 1 + . . .) − ( 0 0 + 1 1 + ...) = where and coeficients are natural integers, and for any given place , one of or at least is zero, and is a relative integer. This presentation highlights a positive term () and a negative term (). If either of these two terms is bounded, we can now bound the other one. For instance, suppose we have the invariant 0 − 1 = 2, and that we have the bound 1 ≤ 1 already, we can deduce that 0 − 1 ≤ 2 hence 0 ≤ 3. The same invariant 0 − 1 = 2 can also be written 1 = 0 − 2, so if we know that 0 ≤ 5 we can deduce that 1 ≤ 3. We iterate the procedure on generalized flows until no new bounds are detected since results might otherwise depend on the order in which the invariants are inspected.
If for instance all the places of the net are covered by simple semi-flows 0 + 1 + 2 = 1, 3 + 4 + 5 = 1 . . . this "rough" strategy is still enough to conclude correctly that the net is one safe. Note however that the computations are very rough, for instance suppose we have invariants 0 + 1 = 1 and 0 + 1 − 2 = 0. The first invariant gives us the bounds 0 ≤ 1 and 1 ≤ 1, the second invariant however will give 2 ≤ 2 because we approximate both 0 and 1 using their current bound (despite having a tighter bound on 0 + 1). Of course a more powerful approach, e.g. an ILP or SMT solver would be able to better exploit this kind of tight bounds, however this "rough" strategy is extremely fast and scales just as well as invariant computation does (so it scales much better than delegating problems to an ILP/SMT solver or doing any kind of actual model-checking).
As described in [
In this process, the SMT solver works with an over-approximation of the state space so that states unreachable according to SMT are definitely unreachable, but SMT may believe some states are reachable when it is is not the case.
When we query the SMT solver, we ask it to exhibit a "reachable" marking satisfying a given
predicate . We thus either get a trusted "UNSAT" answer, that means such a situation is not
possible, or we get a "SAT" answer that cannot be fully trusted (but that we can try to replay,
see [
The strategy to define "reachable" consists in successive approximations that are progressively
more constraining. We start with reals (where the complexity of any linear algebra is much lower)
and only try natural solutions in a second step. We introduce constraints and additional variables
to support those constraints incrementally, starting with flows, then the state equation, then trap
constraints. . . as explained in [
Suppose we have computed a lower bound Maxseen on the marking of a place or group of places. We ask the SMT solver to test whether a state with strictly more tokens than Maxseen in those places is "reachable". If we get "UNSAT", we can conclude, this maximum seen bound cannot be exceeded, it is the bound on this expression.
When we get "SAT", we can try to replay the solution provided by the solver to confirm it. In this process, we exploit the fact that Z3 has an optimizing component, so that we ask the solver to maximize the value of the target expression when it reaches a SAT verdict. This lets the example exhibited by the solver (if we can replay it) be potentially a run that exhibits the true bound, so that in the next iteration when Maxseen has this value and we ask the solver to produce a state with a larger value, we actually get UNSAT and can conclude.
Our full strategy to compute upper bounds thus consists in the following steps : • For colored nets, we can start by computing Maxstruct using the skeleton net and the rough approximation of section 4.1 and/or the more refined one provided by SMT in section 4.2. This is correct since the behavior of the skeleton net is an over-approximation of the behavior of the net. We then unfold the net and proceed with the same algorithm as for PT nets. • For any kind of net, we initialize Maxseen with the value of expressions in the initial marking.
We also compute the P flows of the net and initialize Maxstruct using the rough structural
bounds of section 4.1.
• We then iterate the following steps until a solution is reached (or we time out) :
– If Maxstruct = Maxseen conclude
– Try to increase Maxseen by exploring (parts of) the state space. We can use
pseudorandom or directed walks for instance. We do not need to be exhaustive, Maxseen is
always an under-approximation of the bound we are looking for. So any state space
exploration is fine, ITS-Tools typically runs a decision diagram engine, the LTSMin
engine with partial-order reduction [
The "UpperBounds" category of the MCC consists precisely in this examination. Figure 6) is a
performance comparison taken from the latest 2022 edition of the contest. It compares ITS-Tools
that obtained the gold medal in the category with a total of 23388 points against second place
ifnisher Tapaal that gathered 21687 points (roughly 8% less points). The third place finisher
GreatSPN using only exhaustive methods with advanced decision diagram technology [
While we can observe a large blob of relatively easy answers computed within 10 seconds by Tapaal and that ITS-Tools can take up to two minutes to solve, there is also significant number of points against the right border, corresponding to timeouts of Tapaal when ITS-Tools could answer within a few minutes.
While our algorithm is very efective in most cases, our decision procedure cannot conclude when dealing with unbounded expressions where we should answer +∞ (since Maxseen will never reach this bound with the mechanism we propose to increase it). While they were exceedingly rare originally, the number of unbounded models in the MCC benchmark has been growing steadily, so that dealing with such models is clearly a direction for improvement.
The goal of this examination is to prove that a net is one safe, i.e. in all reachable markings, all place markings are bounded by one. For colored nets the definition is the same, at most one token (all colors confused) per place is allowed.
First we check if the initial state satisfies the property. If not, we can conclude.
Note that this test is conclusive for many models, particularly colored ones where the requirement of having a single token in a colored place is pretty extreme (there is some debate on the definition that was adopted in the MCC, the "color safe" property where there are never more than one token of each color in a given place is perhaps more interesting), and ones with large initial markings (e.g. scaleable models).
The next test consists simply in checking whether the input file contains a relevant NUPN
section [
A basic approach given a decision procedure that can prove an invariant is to simply place one assert on each place of the net and try to prove this as one single big invariant ⋁︁∈P ≤ 1 or as a set of invariant queries ∀ ∈ P, ≤ 1. However this approach can scale poorly when the number of places in the net grows due to the excessive size of the query for the "one big invariant" approach or to the number of queries in the set of queries approach.
In the spirit of gradually treating the problem, we do think of the problem as a set of invariants that we need to prove. Hence each one we can treat reduces the amount of work remaining for downstream procedures.
Our next step consists in reusing the algorithm proposed to compute upper bounds of section 4.1. We try to prove that Maxstruct = 1 for as many places as we can. Even if this bound is not reachable (i.e. we have not computed Maxseen) we can still conclude the place is one safe. Places thus proved to be one safe can be removed from the remaining queries. This strategy is particularly efective on many nets whose places are covered by simple P semi flows.
Still in the spirit of reducing the amount of queries, we can look for places that cannot be fed (and are initially one safe). Such a place can only allow output transitions to fire a single time. Hence if these transitions are the single input of some place, that place is also one safe. More formally, let ⊆ P designate an initially empty set of places, and ⊆ T designate an initially empty set of transitions. We iterate to a fix point the following procedure : • For any place such that • = ∅, or • = {} a single transition and ∈ and W+ ( , ) = 1, then we add to : ← ∪ { } and add all output transitions of to : ← ∪ •. At the end of the procedure, all places in are known to be one safe.
Correctness comes from the fact that transitions in the set can be fired at most once in any execution of the net, hence their output places can receive at most one token in any execution.
This is a low complexity exploration of the structure of the net, that bypasses actual state space exploration. It works particularly well for models of workflows that do not have loops. Any place we deduce is one safe reduces the number of subsequent queries to a reachability engine.
Our full strategy to compute whether a net is one safe thus consists in the following steps : • Test initial conditions and the elementary conditions of section 5.1. • Use the rules of section 5.2 to reduce the amount of queries • If we have not yet concluded, delegate remaining queries to a reachability/invariant decision procedure, as a set of invariants to prove.
These cheap structural tests ahead of a more complete model-checking approach thus help our solution scale to larger models.
The "OneSafe" category of the MCC consists precisely in this examination. Figure 4) is a
performance comparison taken from the latest 2022 edition of the contest. It compares ITS-Tools
that won the category with a total of 25922 points against second place finisher Tapaal that
gathered 24707 points, GreatSPN [
The goal of the "Stable Marking" examination is to prove that there are no places whose marking is constant in all reachable states. This typically could indicate "dead code" or that parts of the net cannot be activated. It sufices to find a single "stable place" whose marking is a constant to answer the query.
For colored nets and prior to unfolding we try to detect that all outgoing arcs of a colored place to a transition have a symmetric incoming arc from inscribed with the same color function. This criterion for constant places in the net reflects a usage pattern in colored models of using complex place markings to encode discretized functions, that are "queried" but never actually updated. This can also be exploited during unfolding to reduce the size of the unfolded net. In any case such a place is stable letting us answer the query.
Still prior to unfolding, we can check if the skeleton net contains stable places (recursively using the same procedure, but it is much smaller). Since its behavior is a super set of the behaviors of the real unfolding, if a place is stable in the skeleton, it must also be stable in the unfolding. The reverse is not true, even if all places of the skeleton can be updated this does not imply that the unfolding satisfies the property.
Failing these two first tests we proceed to unfold the colored net.
The first test on PT nets is to look for an empty row in the incidence matrix W. More precisely we look for an empty column in W⊤ given the sparse data structures we use to store matrices. This indicates a constant place, hence the net has "stable markings".
We then look for unmarked syphons (see [
The next step consists in building a graph representing "free" token flow. We let places be the vertices of the graph, and add an edge from place to place ′ if. there exists a transition with • = { }, • = { ′} and arc weights one. Such "transfer" transitions could be an artifact resulting from model generation, but they also occur naturally in many manually built models. This graph is relatively simple, but we can exploit it to remove the burden of proving for many places that they are not constant.
We use two strategies, both based on computing sufixes in this graph.
Firstly, all places in the sufix of a place that is initially marked, as well as the place itself are not stable. Indeed, the tokens in the place can flow freely to any place "downstream".
Next we can take all remaining places that are not currently proved to be unstable but are connected in this graph, and compute a minimal set of places such that all nodes in the graph are reachable from a node in . This requires a small prefix search and computing the SCC of the graph, but the complexity of these operations is quite incomparable to any downstream model-checking treatment to prove invariants. More precisely, we look for a vertex that has no predecessor, add it to and discard all places in its sufix (i.e. we assert that we have proven they are not stable). When all nodes have a predecessor, only SCC and their sufix remain; we simply pick an arbitrary vertex belonging to an SCC, add it to and discard all places in its sufix. The procedure is iterated until there are no more connected nodes in the graph.
We retain only places in in the subsequent proof burden, and (optimistically) suppose that all places in their sufix (in the free token flow graph) have already been proved non stable. If one of the places in is indeed stable, we will conclude instantly anyway, otherwise all places downstream can indeed be updated, hence the optimistic view we took is justified.
Our full strategy to compute whether a net satisfies the stable marking property thus consists in the following steps : • If the net is colored, check for constant colored places and try to prove the property using the skeleton prior to a full unfolding. • Use the rules of section 6.2 to conclude if possible or at least reduce the amount of queries • If we have not yet concluded, delegate remaining queries to a reachability/invariant decision procedure, as a set of invariants to prove of the form ( ) ≠ 0 ( ) for all remaining places.
The structural tests help the solution scale, by reducing the burden of proof on subsequent steps. By eliminating the burden of proof for some places we also help the decision procedures in the reachability solver to bootstrap more efectively, particularly when they are sensitive to the alphabet of the property. For instance, places whose marking is used in a property cannot be reduced by structural reduction rules and typically neither can neighboring transitions be agglomerated.
The "StableMarking" category of the MCC consists precisely in this examination. Figure 5) is a
performance comparison taken from the latest 2022 edition of the contest. It compares ITS-Tools
that won the category with a total of 24405 points against second place finisher Tapaal that
gathered 21560 points, GreatSPN [
The results on Figure 5 overall advantage ITS-Tools particularly on harder models. There is a dense blob of points above the diagonal corresponding to Tapaal solving within one second while ITS-Tools takes as much as ten seconds. However as models become more dificult to solve, most points end up below the diagonal (and far from it, particularly in a log/log scale), and the relatively dense border to the right indicates many timeouts of Tapaal when ITS-Tools could conclude.
While part of these results come from the good performances of our reachability engine
described in [
In this section mostly consisting of figures we regroup performance plots taken from the website of the Model Checking Contest in its 2022 edition, see https://mcc.lip6.fr/2022/results.php.
These log/log scatter plots compare ITS-Tools that won each of these categories to Tapaal that obtained second place. Each point is a model, with horizontally time consumption for ITS-Tools, and vertically consumption by Tapaal. Points below the diagonal advantage ITS-Tools while points above it advantage Tapaal.
Timeout was 30 minutes on all examinations except upper bounds that is granted one hour. In total, 1617 model instances coming from 150 model families are represented. For upper bounds, each query additionally contains 16 bounds to compute on a given model, for the other plots a single answer is expected.
ITS-Tools is clearly more eficient than the runner up Tapaal on all plots, with OneSafe being the most blatant and Upper Bounds being the least clear cut.
Structural approaches to analyze Petri nets can allow to bypass the state space explosion that is the main enemy of model-checking in many cases. In this paper we have presented eficient strategies designed to answer some of the queries of the model-checking contest as well as computing invariants of a net.
These strategies are used by the state of the art verification engine ITS-Tools and are partly responsible for its success in the competition. While some "strategies" are seemingly trivial, this paper is a precise if informal description of otherwise unpublished algorithms that have been refined and tested over the huge benchmark of the MCC.
ITS-Tools is free open source under GPL, so please do feel free to look directly at the implementations. It is distributed from its home page https://ddd.lip6.fr and hosted on GitHub https: //github.com/lip6/ITSTools.
We would like to thank Amine Benslimane and Sofiane Braneci who helped to integrate support for global properties into ITS-Tools during an internship in 2021.