vanrein
commented
6 years ago In the interest of automated analysis of the composed Petri Net, a combined PNML file will be output. That is the one to run deadlock and liveness analysis against, if you are so inclined.
Not many of these tools seem to be around, but research exists so this may be a matter of having tools like these to draw attention to Petri Nets for practical applications.
A bad approach would be to sit back and wait for the perfect solution from science; very often, there are fundamental problems (that cannot be solved, hence fundamental) or corner cases that have little bearing on practical systems.
A better approach would be to guide designers towards structures that can be proven to do what they want, or that require human oversight to erradicate or specially-handle corner cases.
The task for Perpetuum is to integrate well with feedback mechanisms, for instance by retaining symbols from the original design, and perhaps include annotations inasfar as PNML will allow them in the composed output.
As an example of what we're open to, my own PhD work on model checking has made it clear that concrete (counter) examples work well for human consumption. This may require simple means, like a list of instance names to make these concrete runs of problem cases more pallatable to end users.
Though not a primary purpose of this project, Perpetuum is likely to welcome extensions that perform analysis as part of the compiler.
A few mechanisms can be thought of for composing Petri Nets:
These can be really helpful in managing complexity. When the models are supplied as a list, the compiler can, wel, er... compile them into a larger one. Since the editor and simulator are likely to not follow this, the emphasis on predictable semantics has been added above.
At the present time, it may be that the only thing we shall consider are the same-named transitions.