VD78 forms hierarchies with well-formed subnets. We may represent any well-formed subnet, as an ordinary transition, for inclusion in any net.
Next, four years later, copycat82 attempts to build hierarchies, too. Although, copycat82 also mentions the term "well-formed," most examples of copycat82, cannot even pass as valid Petri net. Therefore, we may infer that, either
In either case, any attempt to verify such a vagueness, as it is, would only explode complexity. For a verifier to understand the (Petri) net, out of such vague macro-hierarchies, either
copycat82 ignores any problems. It neither expands all macros, nor is to provide any such algorithm to find VD78-ready subnets, within a (free-form) NN73 macro hierarchy. Another work, SARA, does find a few patterns, and reduces them, but even SARA requires, first, to expand the full net, only next to reduce. VD78 and copycat82, verify each subnet separately.
To verify a VD78 well-formed subnet, only for the case of a single token, is enough, for any run-time. The reduction (of a subnet, as a transition) remains equivalent (to the original net), with any amount of tokens.
copycat82 is chaotical, with its un-proper (sticky) subnets. To verify with a particular marking would never suffice - unless, by chance, that subnet fits VD78 restrictions.
copycat82 must verify each subnet with an exhaustive list of token-entry scenarios. e.g: In two (or more) of its examples, a subnet which works with a single token, could still be deadlocked, if a second token enters that net, while the first token is at a particular place (at an "xor" gate), within the subnet. That needs very intricate timing. Such a subnet must be only used, with previously (exhaustively) tested token-scenarios.
In other words, an "otherwise-tested" subnet may carry a deadlock-potential, if enabled with multiple tokens. i.e: From n to n+1 tokens, a deeadlock may be introduced, because of the inhibitor arc(s). Not to mention possible token entries, from different input-places. An entry from p1, may invoke something else, or if p1 and p2 may resemble each other, p3 need not be. Every single permutation must be tracked. But, copycat82 does not tell it, either.
If proper (VD78 well-formed) reductions are avoided, the prospective-container net would need to know about the quirks of that subnet/macro. NN73 suggests the full expansion of those macros. SARA CFA reduces nets after the macro-expansions (of SARA SL modules). To report what a subnet does, would need a very complex, and probably costly, vertical-specification language, which expands as macros. A trivial idea is to reduce any macro with SARA/UCLA algorithm, and expand that, instead of the full macro. This needs a reduction, after expansion, too, because at joints, the macros may form reduceable patterns, again.
An insistence to avoid any expansion, as copycat82 does with ignorance, explodes complexity Although copycat82 attempts to expand the input/output macros (similar to a SARA CFA strategy, to translate SARA/UCLA logic, to Petri nets), even that brings increased quirkiness, instead of avoid. Those macros, being not proper, and deadlockable themselves, even if expanded within a subnet, they would increase the problematic cases which need to be captured - to inform the readers/modelers/verifiers.
It is aversive (and/or needs real research), to insist to represent any subnet as if it were a reduced-transition, with only some adaptor-macros to stand at its entrance and/or exit. That not only may explode the complexity (marking space) of the verification process (instead of reduction, because the re-expression through the limited set of macros may be more complex than the subnet itself), but to exhaustively-list, all the possible scenarios, with intricate timings, may be very tedious to do manually - whether it is theoretically possible, at all.
e.g: To express "when a single token enters, the tokens may be released in any permutation of the output-paths" is a tedious (and very expensive) way of expressing a simple parallelism, if that. (It maps the internal logic to other terms, any way.)
Next, also to tell that "when two tokens enter, the subnet "possibly" may deadlock" is either" difficult or impossible. Notice that, the two tokens need not even enter together, the problem may occur when they meet somewhere within the subnet. Those mythical adaptor-macros must cover all these possibilities, and the user must exhaustively list these, with all the scenarios, one by one.
copycat82 provides no software tools, and even it may not be possible. Is that progress, at all? This only points out that, copycat82 may have never ever attempted to verify its own examples. Otherwise, it would suggest something else.