Labels

Diagrams

skinparam componentStyle rectangle\nscale max 1024*1024\n\ntitle Input\n\ncloud "pnml.com" {\n    database "RelaxNG Schema" \$schema\n    file PNTD\n}\n\nfile "Input.pnml"\n\ncomponent Parser #Yellow {\n    [EzXML]\n    [XMLDict]\n}\n\ncomponent Core {\n    [Sort]\n    [Term]\n    [Declaration]\n    [Lable]\n    [Node]\n    [Expression]\n}\ncomponent Storage {\n    component [DeclDict] {\n        component variabledecls\n        component namedsorts\n        component arbitrarysorts\n        component partitionsorts\n        component namedoperators\n        component arbitraryoperators\n        component partitionops\n        component feconstants\n        component usersorts\n        component useroperators\n    }\n    component [NetKeys] {\n        component page_set\n        component place_set\n        component transition_set\n        component arc_set\n        component reftransition_set\n        component refplace_set\n    }\n    component [NetData] {\n        component place_dict\n        component transition_dict\n        component arc_dict\n        component refplace_dict\n        component reftransition_dict\n    }\n}\n\ncomponent PetriNet {\n    [PnmlNet]\n}\n"Input.pnml" -- PNTD : uri\n"RelaxNG Schema" -- PNTD\n\nInput.pnml -- Parser : xml\nParser -- Core\nCore -- Storage\nPetriNet -- Storage\nPetriNet -- Core

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_mapConstant

Map 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 '_'.

source

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())

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.