Ready.
A review of the research paper:
VD78 introduces a methodology to model, and seamlessly verify,
VD78 does not introduce new graph types. It orchestrates the prior art, to found a feasible methodology.
VD78 keeps Petri nets as it is, for the first level, although avoids some patterns of the regular Petri net use. Instead, VD78 suggests the data-graph (after LOGOS), to represent unbounded variables, and whatever pertains to data. The Petri net is used for control of (the structure of) events. The (internal) computations are in its data-graph.
At the second level, VD78 lets associate a label with any Petri net transition, through a label to point at its data-graph. A label lists the related data-operator and/or the data-predicate - to avoid, non-determinacy (race-conditions), and/or non-determinism, respectively.
The third level is not published in VD78, but it is available in Va76, the Ph.D. of Valette (in French). VD78 reasons that, the interest of the method is the ease, provided by the first two levels, to the third - by pre-verifying the system structure.
With VD78, to model, is together, at every turn, with the verifier. This contrasts, for example, with a strategy to model the net first, whether module-by-module or as a single piece, only next, to verify all of it, together (such as with SARA). For this ready-modularity,
That "idle" place represents the rest of the net, as referrable by the well-formed subnet. To use Petri net terms, the net and the well-formed subnet, are represented to each other, as a Petri net place vs. a Petri net transition, respectively.
Some readers may question whether the well-formedness restrictions of VD78 are "too restrictive." i.e: May it not be defined in some other way? Maybe. But you should first appreciate the elegance of VD78, before you "challenge" it, or else, you may be only to commit to a worse than trivial junk, such as copycat82, which claims to "let" arbitrary dissections of a net, but it is not verifiable, any more, although it attempts to! That is, copycat82 is fault-prone, in its ignorance.
copycat82, is a subset of VD78, as copycat82 commits plagiarism, and its sheer ignorance, and/or immense neglect, provides a lot of un-exemplar examples, to avoid, when working with net-formalisms.