Standards families
Petri net
Places, transitions, tokens: the producer/consumer net with the marking drawn, firing rules implicit in the topology.
petri.basic@1New DDN source
Why use it?
Concurrency questions (can this deadlock? can this starve?) have a formal home — and it draws small.
When it helps
Reasoning about concurrent resource flow: pipelines, buffers, locks, work queues.
How to read it
- Circles are places (holding tokens), bars are transitions (firing), dots are the current marking.
- A transition fires when every input place holds a token — trace one firing by hand.
What you need
- The places
- The transitions and their arcs
- The initial marking
Things to check
- Do not draw an arc transition-to-transition — flow alternates place/transition.
- An empty net proves nothing; declare the marking you are analysing.
Scope of this diagram
Declared net with structural validation; reachability and liveness are reading aids here, not a model-checker run.
Work with the converted example
- Open the viewer and select
net. Inspect the rendered view and its source. - Open the designer. Keep the selected profile and inspect its legal palette and property controls.
- Change one displayed title or an appropriate data value. Apply the edit and check the resulting diagram.
- Run the verifier and review its diagnostics before moving complete content into review.
- Download your edited DDN source to retain the change.
The example uses the indentation-based ddn-next-1 dialect. The language guide explains reusable definitions, dotted data rows and explicit property blocks.