Profile contract
petri.basic@1
ISO/IEC 15909 Petri net notation: places (circles) with token counts, transitions (bars), weighted arcs, inhibitor arcs (open-circle end), test/read arcs (dashed), markings via records. Bipartite graph enforced: places connect only to transitions and vice versa.
graph projectionPetri net
Open this profile in the gallery
Primary palette
Relationship roles
Legal endpoints
| Relation | Source roles | Target roles | Self relation |
|---|---|---|---|
petri.arc | petri.place, petri.transition | petri.place, petri.transition | Not allowed |
petri.inhibitor | petri.place | petri.transition | Not allowed |
petri.testarc | petri.place, petri.transition | petri.place, petri.transition | Not allowed |
Profile verification
- Arcs are bipartite between place and transition; each registered arc role retains its direction.
- Token counts are integers >=0; explicit arc weights are integers >=1, not zero.
- Draw place markings and transition bars; inhibitor and test arcs remain separate verbs.
- Weight metadata applies to petri.arc and petri.testarc; inhibitor arcs do not accept a weight field. Tokens metadata belongs only to petri.place.
Profile defaults
Explicit file settings override eligible CSS, then these profile defaults and the common standard apply. Unspecified semantic facts remain unspecified.
{
"projection.kind": "graph",
"projection.profile": "petri.basic@1",
"petri.tokens": 0,
"petri.weight": 1
}Projection properties
kind, profile, inputs, analysis_budget, traces, iso, depth
Design operations
- Create place/transition; edit supplied token count or positive arc weight; connect ordinary/inhibitor/test arc.
Bounded analysis
Structural verification and display only; no execution or implied process engine.
Outside this profile
- reachability/coverability analysis
- PNML interchange
- net execution/simulation