Ready.
On copycat82's page 143, there is only the "Fig.6.2." which shows the internals of the "producer" and "consumer" as referred to, in "Fig.6.1." (on
The macro/"component" "Produce" has "xor-input" entrance-macro at its start. This means it deadlocks, if p1 and p9 each have a token, at the same time.
In such cases where timing is important, for a subnet to behave appropriately, only specifying an initial marking would not suffice - very especially if re-entry is possible, while the macro is still running.
copycat82 does not discuss any such thing. It does not list the VD78 criteria for well-formed subnets, either. In fact, as this example shows, its own examples, exactly within the Ph.D. dissertation, have such problems. Although the "Producer" in fig.6.2. (which contains the "produce"), is a macro referred from the Fig.6.1. on page 141, it appears, it makes assumptions that the container net would not send any more tokens. Even this assumption is not expressed, though, as copycat82 ignores all such. Instead, I point it out, here, that such scenarios are needed, if external-state (at the environment) may interfere with the internal-sate of the subnet/macro/"component" which is being verified.
The other side of the story is vague, too. How may the container guess that the particular subnet may deadlock, it is not proper, not conservative? These are possible when no restriction is declared, but they are not captured in any way, with copycat82, at all.
In contrast, VD78 has its restrictions that impose the expected well-formedness on a subnet, and NN73 suggest all macros to be expanded within the full net - transparent to the verifier. i.e: Both VD78, and NN73 cover their cases appropriately. It is copycat82 which is mixing, but not matching, between the two.
copycat82 also uses the words "well-formedness" but it begs the question, because it assumes the entrance/exit gate macros to be a sufficient/correct set of specification-rules/options. Then, as we state here, the question is: What specification-option(s) inform about such internal problems, within a macro/subnet, and how would a Petri net verifier make sense of it?