Labels
Diagrams
PNTD Maps
Defaut PNTD to Symbol map (URI string to pntd symbol):
"continuous" => :continuous
"highlevelnet" => :hlnet
"hlcore" => :hlcore
"hlnet" => :hlnet
"http://www.pnml.org/version-2009/grammar/highlevelnet" => :hlnet
"http://www.pnml.org/version-2009/grammar/pnmlcore" => :pnmlcore
"http://www.pnml.org/version-2009/grammar/pnmlcoremodel" => :pnmlcore
"http://www.pnml.org/version-2009/grammar/pt-hlpng" => :pt_hlpng
"http://www.pnml.org/version-2009/grammar/ptnet" => :ptnet
"http://www.pnml.org/version-2009/grammar/symmetricnet" => :symmetric
"https://www.pnml.org/version-2009/extensions/inhibitorptnet" => :ptnet
"https://www.pnml.org/version-2009/extensions/resetinhibitorptnet" => :ptnet
"https://www.pnml.org/version-2009/extensions/resetptnet" => :ptnet
"inhibitorptnet" => :ptnet
"nonstandard" => :pnmlcore
"open" => :pnmlcore
"pnmlcore" => :pnmlcore
"pt-hlpng" => :pt_hlpng
"pt_hlpng" => :pt_hlpng
"ptnet" => :ptnet
"resetinhibitorptnet" => :ptnet
"resetptnet" => :ptnet
"symmetric" => :symmetric
"symmetricnet" => :symmetric
PNML.PnmlTypes.pntd_map
— ConstantMap from Petri Net Type Definition (pntd) URI to Symbol. Allows multiple strings to map to the same pntd.
There is a companion map pnmltype_map
that takes the symbol to a type object.
The URI is a string and may be the full URL of a pntd schema, just the schema file name, or a placeholder for a future schema.
For readability, the 'pntd symbol' should match the name used in the URI with inconvinient characters removed or replaced. For example, '-' is replaced by '_'.
PnmlType map (pntd symbol to singleton):
Pair{Symbol, PNML.PnmlTypes.PnmlType}(:pnmlcore, PNML.PnmlTypes.PnmlCoreNet())
Pair{Symbol, PNML.PnmlTypes.PnmlType}(:symmetric, PNML.PnmlTypes.SymmetricNet())
Pair{Symbol, PNML.PnmlTypes.PnmlType}(:ptnet, PNML.PnmlTypes.PTNet())
Pair{Symbol, PNML.PnmlTypes.PnmlType}(:continuous, PNML.PnmlTypes.ContinuousNet())
Pair{Symbol, PNML.PnmlTypes.PnmlType}(:hlnet, PNML.PnmlTypes.HLPNG())
Pair{Symbol, PNML.PnmlTypes.PnmlType}(:hlcore, PNML.PnmlTypes.HLCoreNet())
Pair{Symbol, PNML.PnmlTypes.PnmlType}(:pt_hlpng, PNML.PnmlTypes.PT_HLPNG())
PNML.PnmlTypes.pnmltype_map
— ConstantThe key Symbols are the supported kinds of Petri Nets. Maps to singletons.
Handling Labels
The implementation of Labels supports annotation and attribute format labels.
Annotation Labels
annotation format labels are expected to have either a <text> element, a <structure> element or both. Often the <text> is a human-readable representation of of the <structure> element. Graphics
and ToolInfo
elements may be present.
For PTNet
(and pnmlcore
) only the Name
label with a <text> element (and no <structure> element) is defined by the standard.
Labels defined in High-Level pntds, specifically 'Symmetric Nets', "require" all meaning to reside in the <structure>.
Attribute Labels
attribute format labels are present in the UML model of pnml. They differ from annotation by omitting the Graphics
element, but retain the ToolInfo
element. Unless an optimization is identified, both attribute and annotation will share the same implementation.
A standard-conforming pnml model would not have any Graphics
element so that field would be nothing
.
High-level Petri Net Concepts
Based on a draft version of ISO/IEC 15909-1:2004 High-level Petri nets - Part 1: Concepts, definitions and graphical notation.
Useful for setting the ontology.
Arc inscriptions are expressions that are evaluated.
Place markings are multisets of tokens of a sort/type.
Transition conditions are boolean expressions that are evaluated. Used to determine if transition is enabled.
Expressions in pnml can be many-sorted algebras. Declaration, Term, Sort, Multiset, Variable, are among the concepts used to define expressions.
Terms
Terms have sorts: the sort of the variable or the output sort of the operator.
Terms can be buit from built-in operators and sorts, and user-defined variables. These are defined in variable declarations, a kind of annotation label attached to pages and nets.
A transition can have a condition, a term of sort boolean, which imposes restrictions on when the transition may fire.
Sorts
named sorts are constructed from existing sorts and given a new name.
arbitrary sort is not defined in core, is not allowed in Symmetric Nets. HLPNG adds arbitrary declarations, sorts of lists, strings, integers to Symmetric Nets.
The sort of a term is the sort of the variable or the output sort of the operator.
Operators
An operator can be: built-in constant, built-in operator, multiset operator or tuple operator.
User-defined operators, or named operators are abbreviations, built from existing operators and parameter variables.
There will be arbitrary operator declarations for High-Level Petri Net Graphs, but not for Symmetric Nets.
Operators have a sequence of input sorts and a single output sort.
Variables
TBD
Notes on Petri Nets
Multiset Rewriting Systems
I. Cervesato: Petri Nets as Multiset Rewriting Systems in a Linear Framework
This addresses Place Transition Nets. High-level Petri nets explictily use multisets.
factor out the multiplicity of the elements of the underlying set. This is achieved by first defining the notion of singleton multisets and then by writing arbitrary multisets as linear combination of singleton multisets.
a rewrite rule can be viewed as a singleton multiset
Petri nets are meant to represent evolving systems. To represent this dynamic flavor, we will rely on the notion of multiset rewriting systems.
Continuous, Open and Other Petri Nets
Allow marking, inscription, conditions to be floating point even when standard wants an integer. This allows continuous nets.
See Petri.jl and AlgebraicPetri.jl for some continuous Petri Net use-cases.
TODO: Hybrid nets combining floating point/continuous and integer/discrete inscription/marking.