Ready.
Petri nets are verifiable with the reachability-test. The vagueness of copycat82, loses that ability, though. The (implicit, unstated) assumption of "verifiable-macros", is FALSE. The "verifiability" is degenerate, because an ordinary Petri net verifier, would not work with those vague, unproperly-prepared nets.
In other words, it attempts to claim Macro E-nets (NN73) as its own, with a change of names. That is copycat82's plagiarism. Next, it cuts-and-pastes bits-and-pieces, imitative of published papers of yet others. But when such sources have differences, the vagueness piles up. At the end, the faultiness is a given of copycat82 - although even the attempted would have been trivial, any way.
The malicious situation is that, the non-method of copycat82 is chronically ignorant. As such, copycat82, the un-credible Ph.D., is a generator of faultiness, with its fake claims - if you buy them.
copycat82 is buried in its faulty examples, throughout its pages. Even that alone could tip about its lack of achievement, especially as it claims to be a Ph.D. study in the field of software-methodologies, to build and verify, with Petri nets. What sort of "verified examples" would contain such an immense amount of errors? Is there any such method, at all?
VD78 had published its own proofs, for reduced, separately-verifiable subnets. If copycat82 claims to introduce anything new about verifiability, where is the proof about it? There are no attempted proofs-of-correct-operation in copycat82, whatsoever.
copycat82 vagueness, leaves it unverifiable by a Petri net verifier. This page presents examples of it. Another page, points out the exponentially-explosive complexity - beyond Petri nets. That is, even if we write a new kind of verifier to verify that sort of vagueness, it may not be feasible to run, at all.
In many cases, the published examples of copycat82 turn out to be false. Such faults point out many failures of copycat82's attempted method, too. Has nobody cared to reflect about them? Neither the author(s), nor the jury(ies)? If only those trivial examples had been verified, it would be clear that the "missing" proofs, in fact, cannot exist because the method-crashing examples, the standard faults, already exist in copycat82 itself, at some very unexpectably central figures (which were published with those faults, also in copycat83-the-associated-paper, the next year).
copycat82 confuses macros with properly-reduced subnets. How would a Petri net verifier make sense of it?
copycat82 sells laxness. If we would buy its fake claims, we would start with a full net, or a single node, and proceed with chops. But even the schematic figures, in its section four ought to warn us that, there is no such free lunch. Although copycat82 does not specify any rules, those rules that VD78 had listed are necessary, for verifiability. As such, most of those "intermediate" figures, in fact, lose equivalence to the full net, if it means anything, at all. At most, immediately, they must be expanded as NN73 suggests for macros.
In other words, such a vague "component" in copycat82, is only a mixture. We must identify the reduceable parts with VD78 rules, and we must expand the rest, as NN73 had suggested for macros. The SARA software system, had already implemented such a combined strategy, with the strong-reduction algorithm, that compresses a net, after SARA SL modules are expanded.
The VD78 and SARA strategies start at the opposite ends, although for the same overall strategy. VD78 rules/restrictions for a well-formed subnet, lets prepare off-the-shelf subnets, after they are verified. The UCLA/SARA algoritm identifies reduceable patterns. i.e.: VD78 comcentrates on the pieces, whereas SARA concentrates on successive improvements in an existing net. Both SARA and VD78, may fruitfully work together, but copycat82 mentions neither as a source. They only pass in the literature-overview sections, briefly.
The ignorance with the structure persists, beyond those macro-chops. The examples, imitative of SARA SL, contain what SARA people would name "socket calls." i.e: A module invokes another module, while it has not terminated itself, yet. It is what a SARA SL module lets, but a SARA control-node would not. SL is SARA's macro package, with software-system support, whereas the control-nodes are the representative net-elements. The vagueness of copycat82, confuses the two, but the naive programmers, sooner or later, must find out a requirements-list, such as VD78, if they are to verify their nets, at all.
If a subnet, imitative of SARA socket-calls, contains intermediate exit/entrance places, it violates the single-entrance-single-exit rule of Petri net non-primitive transitions. Thereby, it violates even the first rule of a subnet-to-transition reduceability. It would be improper, too, because it assumes an internal state, within that subnet. The entrance, versus the return-from-socket-call must find different internal states. This is not proper.
The existence of multiple phases of entrance/exit(s) to any macro/"component" increases the vagueness of data-rectangles, even as a commentary, too. In many cases, data-name is unknowable to be associated, with which path(s) in/out of that macro. e.g: When two macros communicate, over many phases, but the data-items may be associated with only some of the phases, and furthermore, some of the phases may refer to the same item, whereas others may refer to the different versions of the same item, as captured in a frame that visited that node, at an older time. Nothing is mentioned about such data-access semantics in copycat82, although its figures do contain such varieties, in its full-ignorance. (e.g: see the article Is it supposed to be a similarity-semantics?)
The vagueness is noticeable, when we contrast it with the prior art, published before copycat82. E-nets identify resources with the tokens (the token-attributes). Therefore, no possible confusion, even with paths in/out of macros. If the resource is not a captured-value, and/or if it is globally-modifiable, an environment-variable would fit it, in E-nets. SARA formally identifies the data within the sockets. At each socket-call, we know the list of data-items of relevance. VD78 is not about macros, and no phase-dependent information is relevant. None of these researchers merge/expand the data-graph, within the net, to spread out data, around macros. It is the copycat82 vagueness. The others do identify where the data coheres, with exact referrals, encoded in their formal structures. i.e: copycat82 associates data with some macro(s), not with any of the places/paths, although it is in the paths where the intricacies of control, are represented. For example, a return from a "socket call" is not the same as a new-entry. They have different data-relevance, too.
copycat82 does not even attempt to verify with data. i.e: Neither the Da80 strategy, nor the (second and third levels of the) VD78 strategy. Data is never employed. This leaves copycat82 equivalent to only-the-first-level of VD78. That is, a subset of VD78. The Petri net part gets verified all by itself. That leaves the question open, as to why the data was included at all. NN73, and VD78 had employed data for determinism. In fact, copycat82 also tells the same, at the introductory part, but probably did not care to implement, at the end. (May have thought, an advertisement of it was enough?)
Data-name rectangles turn out to be, as such, patently useless. Only tedious commentary. It is only a tedious, verbose cut-and-paste of E-net formal,listings, into the net-figure itself. (Or equivalently, when the VD78 graphs are one-to-one everywhere, the merged control- and data-graphs would be the cluttered, unnormalized graph which copycat82 paints. The anomalies appear in copycat82 though, when the elements may not be necessarily one-to-one.)
Data, shown but lost. Still non-deterministic (and explicitly states that, when specifying the behavior of or/xor-output macros. Furthermore, inhibitor arcs]
What I refer to as the partial-flow of tokens (or, as "partially fired" transitions, if that were possible), is to expect a transition/subnet to fire, without all of its inbound paths enabled (whether ordinary, or inhibitory arcs), and/or to possibly output tokens to only some of its output places. This is certainly not a Petri net transition behavior, but it is a possible case with macros. A Petri net verifer cannot make sense of such a structure.
For example, Da80 studies interface machines. An interface-macro may connect two sides, over multiple phases. If there are twelve phases, that means twelve input paths, and twelve output paths to that interface machine, to represent different phases, with two sides. (If within a phase, full-duplex communication is available, this would double the paths.)
Petri net verifiers would not verify it. Period. In fact, such a vagueness, an attempt to verify macros, is extremely-expensive for any verifier. When that macro is not expanded/replaced, the verifier would have to check out, every possible permutation. That is exponential explosion. After all, not every macro would have only a single path enabled at all times. Therefore, the verifier cannot assume it. Any number of paths may be activated, for whatever purpose, at any time.
copycat82 attempts to verify subnets separately, with a loop that only recursively, but separately, verifies every subnet. Such a naive, primitive loop, does not count as a real multi-level verifier.
To make it work, the subnets must be equivalent to the net primitives - either to transitions, or to places. For example, VD78 studies abstraction of well-formed subnets to ordinary transitions.
Even without any loops, token-output, in multiple steps, is not verifiable as a Petri net. A Petri net transition, either fires, or not. It never drags its feet, after start. Even Petri subnets, as non-primitive transitions, at least, require that there is a single-entrance, and a single-exit, so that when the activity is over, this occurs in atomic-time.
copycat82 does not implement the "superscript" (repeated output) operator. Although we could do it ourselves, it may not be so trivial to isolate it from the rest of the code within a procedure. i.e: Only the macro-replacement figure would not suffice. The rest of the resolution- and transition-procedures must also be transformed to the net primitives, at least to a point, where every element inputs/outputs a single token through a single arc, when it fires. (This issue is not about arc-weights. A weighted-arc, in Petri nets, is atomic, too. Acts in a single-step.)
It is especially problematic with copycat82, because although multiple-output leans on data, copycat82 does not use data, when the net is to be verified. Thereby, any macro, with multiple-steps of output, per macro, lose sense. A verifier, must either falsely assume such a subnet as with a single-token-per-arc rule, and/or may expect any number of tokens, from any transition/subnet which was ever enabled, once upon a time.
Da80 studies net-compression with data, but copycat82 is not capable of what Da80 does, when copycat82's data gets jettisoned by the verifier. Only a vague subset of Da80.
When there are loops, the multi-step-token-output means that macro is runnable again, with its own output, before it finishes the current job. For Petri nets, it is not representable, until that macro is replaced with the equivalent subnet. Such a subnet is not isolated from its "previous" activations.
A Petri net transition, either fires, or not. It never drags its feet, after start. Even Petri subnets, as non-primitive transitions, at least, require that there is a single-entrance, and a single-exit, so that when the activity is over, this occurs in atomic-time. Multiple-step-token-output necessitates multiple-scenarios management, with intricate-timings. A single "initial marking," or two, would not suffice. Their interdependence is important. e.g: Even copycat82 itself contains examples, that would deadlock, if a token would enter, when the subnet is at a particular state (page72, page143.) Such a trivality stays there, with all of the problems, because copycat82 ignores it. Many other naive people, if they use the copycat82, would commit such errors.
When a subnet is not proper, that is, if it preserves its internal-state is changed through successive runs, then it is false to asume it as if it were a subnet with a constant behavior. e.g: A queue-macro that may hold at most five tokens. The different states of it (0, 5, or other) would present different input and/or output patterns of behavior. Such a subnet, is not primitive-compatible. As NN73 had suggested, we must expand them as macros, as long as, the verifier does not know its internal structure - especially so, when copycat82 jettisons data.
Such a subnet may get arbitrarily complex. If it also contains deadlock-potentials, nothing less than an exhaustive set of scenarios that consider multiple-token entries at a variety of internal states, are needed. i.e: It would not suffice to verify it only once, with a single initial-marking. Although VD78 subnets are able to verify with a single marking, the stickiness in copycat82 subnets would not let it.
If there are n different input configurations possible, the verifier must run every combination-set over and over again, in combinations with each other, until some previous internal-state is met again. To verify a subnet as if it were a stand-alone net without stickiness, ignores a lot of possibilities, when stickiness may exist i.e.: side-effects, like static data, or global data, shared among functions around the system, or like a flip-flop, but with ill-defined set of states, atleast, in the examples of copycat82. Even its input-macros "or-in", "++-priority-in" and also "xor-in" contain such stickiness. Any net which uses those problematic input/output macros would inherit the problems.
For example, the producer-consumer example in copycat82/83 is such a problematic case with stickiness. Although the deadlockable subnet "producer," within the example circuit, may not deadlock, when there is only a single start, the same submacro would deadlock, if that container-net, were included in a circuit that may send another token. This means, although the second pile upon it still works, yet another layer may introduce a deadlock. That is not any true "layers of abstraction."
copycat82 neither represents, nor avoids such behavior, about a subnet. We have to read the macro/subnet itself to find out whether it may deadlock within a given circuit. This means, we have to expand all of them as macros, or we have to verify subnets with multiple scenarios, to list such weaknesses. None of this exists in copycat82, at all. As such, copycat82 is extremely fault-prone.
The ADTs are not the only. We find that copycat82 is totally-chaotic with net-nodes, too. In copycat82, a node/"component" does not have any such requirement that a fixed number of tokens should enter/exit. After the first time it is enabled, that node may release any number of tokens, any time, forever. In fact, the ADTs only make this even more chaotic, because, with ADTs, possibly, a node does not even need to be enabled first, before releasing any tokens. There are no examples for this, in copycat82, but when we imagine the proposed multiple-step-token-release-when-enabled (on pages 53-54, the "superscript"), with the ADTs exception-management, anything may occur, anytime.
How would that be verifiable, especially when all the data (with their "data-types") are neglected for the reachability-test of the Petri nets? The model lets arbitrary behavior, but the Petri net verifier expects a fit to special restrictions, in abstraction.
VD78 was already a prior-art paper with multiple-levels of analysis. The first-level of VD78 is the Petri net reachability test, neglecting the data. But to make it workable, VD78 pay special attention to ensure the subnets to be well-formed (such that, it is assumable as a primitive transition, for a Peri net verifier's purposes). But to arrive the VD78, any violations that do not follow the VD78 restrictions must be expanded as macros - as NN73 do with their macros for E-nets, and as SARA people must do so with SARA SL modules, before verifying with SARA CFA, as a Petri net.
Now, the problem is a double-edged sword: It cuts either way. If those ADTs are confined to individual subnets/nodes, expanding them as macros could be easier, but that would not be anything different than what we already had. Or otherwise, if those ADTs have their separate interconnection logic, behind the scenes, as a duality, with its own intricacies, that would need a very involved macro-processor to transform/expand those macros to make such a net correctly verifiable, as a Petri net. Please, keep in mind that, no algorithm, not even any examples exist in copycat82, for such ADT-to-net transformations.
As a prior art, see NN73 examples with queues (p.722), and alternatives-in-representation (p.724). Da80 discusses these, but an X-transition always fires as a single-token-in-single-token-out. Da80 does not suggest a separate ADT, to go with E-nets, either. In fact, I would interpret Da80's inclusion of a discussion, in section "IV.F Programming Languages" about hybrid models, right after the section "IV.E" where the E-nets are mapped to a two-level FSA, as a suggestion that E-net, in itself, is a hybrid that is sufficiently formal.
Although copycat82 never cites Da80, at all, some very similar patterns do suggest even a plagiarism in copycat82, and here, in the case of ADTs, the reason why copycat82 introduces yet another hybrid, might be a misinterpretation that "something yet further may need to go with E-nets." But when we look carefully, there is no further substance about it, in copycat82. That is, in fact, where, copycat82, at first appears a bit different, is only its false (unsubstantiated) advertisement.
copycat82's fake claims to represent and verify software, evaporate, when we notice its faultiness. Still
Even minor errata, may crash real world projects, e.g: the necessary parantheses do not exist in a switch/case macro, where the adjacent paths exclude each other, but the others may occur together. The second and the third may not occur together, but the first and the third may occur together. What sort of "switch/case" is that? How was that verified, if at all?
Although a verification system should have ways to verify any such errors, we concentrate here only on the persistent, systematic faultiness. Most of the input/output transfer macros contain faults and/or quirks (as implemented on its pages 129, and 130), although being used throughout copycat82. Any net which uses those problematic input/output macros would inherit the problems.
If we keep in mind that, one of the main reasons for using Petri nets is the strength at verification, the problematic nature of the problems becomes clearer. (If a PhD recipient with Petri nets cannot write correct Petri nets, who is supposed to?)
Petri nets had already been modified, by other researchers. E-net is an example. VD78, and SARA
employ Petri net research, too. The suggested "method," in copycat82, is a duplication attempt,
as copycat82 cuts-and-pastes from other research papers,
although it cannot keep even the rewards of those changes that had already existed.
copycat82 is not verifiable, at all. It loses Petri net'ness - vagueness leaves it very much fault-prone. It is only a very cluttered way of vague commentary, and it has not helped even the examples in copycat82 itself, given its immensely-faulty examples. This shows that, even the Ph.D.-grantee cannot avoid such gotchas, as found in its examples. As such, the necessity of an explicitly-stated list of restrictions, such as published by VD78, is certain. Even the basic advantages of the ordinary Petri nets are lost. And such an ignorance, essentially, totally disqualifies the copycat82 as a Ph.D. recipient.
copycat82 is problematic in other ways, too. The representational assumptions it lists, are not those verified by a Petri net verifier. The model, and the verifier talk different languages. The latter would generate a lot of absurd messages, totally meaningless to the modeler. This does not occur with VD78. It is copycat82's confusion. e.g: zero-wait transitions are not enforced by Petri net verifiers. Those assumptions, e.g. "as soon as"ness is not part of Petri nets.