A Schematron mini-schema for PNML Symmetric Nets constraints specification
This schema provides Schematron rules you may use to further check the validity of a Symmetric
Net Document, in addition to the original PNML Schema in RELAX NG. This schema reuses the rules
designed to check PNML Core Model Documents, since Symmetric Nets are built upon the Core Model.
File name : SNetconstraints.sch
Requires : CMConstraints.sch
Version : 2010
Copyright notice : Copyright 2010 Lom Hillah (AFNOR)
License : GNU GPL v3 (See http://www.gnu.org/licenses/)
Revisions - (Number/Date/Author/[Comment]) : 1/April 25, 2010/L.H./Inception
: 2/April 27, 2010/L.H./New semantic rules
: 3/June 16, 2010/L.H./Rules for operators arity
In this schema we provide a phase for Symmetric nets. Since the Core Model schema is
included, its phase will be activated as well during validation. If you extends this schema
with another phase, you may set a default phase for the validation in the @defaultPhase
attribute of the iso:schema element.
Checks declarations' id attribute existence
Checks that no arc connects two nodes of the same kind
The arc '' must connect two different kinds of nodes.
Checks every user sort actually references an existing named sort. Normally, even dot and
bool should be explicitly declared, to preserve the completeness and consistency of ID/IDREF
pairs between usersort and namedsort.
The referenced sort from whose @declaration is ''
must be an actual named sort or a partition.
Checks every user operator actually references an existing named
operator or feconstant.
The referenced operator from whose @declaration is '' must be
an actual named operator (namedoperator), a finite enumeration constant (feconsant) or
a partition element (partitionelement).
Checks named sorts do not contain a multiset sort declaration
The ''
should not contain a multiset sort declaration.
Checks variables used in expressions actually reference declared variables
Attribute @refvariable '' of element should
reference an actual declared variable.
Checks every cartesian product involves at least two sorts
Product sort named '' must involve at least two sorts.
Checks finite int range constants belong to their range and that
their arity is zero.
Finite int range constant whose value is '', must belong to the
declared range ''..''
As an operator, the arity of the finite int range constant whose value is ''
must be equal to 0.
Checks naturals, and positives belong to their range.
Numeric values in XPath are integer, decimal and double...
Number constant whose value is '' must belong to the declared
range ()
Checks every Symmetric net has at least a declarative part;
there should not be sort declarations using infinite types such as natural, positive and integer.
Symmetric Net '' must have a declarative part
(element structure required and non-empty).
Infinite types such as Natural, Positive and Integer must not be used in
sort declarations in Symmetric nets (in net '').
Checks every place is typed
Place '' must be typed (or have a domain) by a sort.
Checks every specified initial marking is non-empty
Initial marking of place '' must be structured by
a term (element structure required and non-empty).
Checks every specified condition is non-empty; variables in a condition are of the same
named sort; any variable referenced in a condition must appear at least once either in the input or
output arcs of the transition ; any value compared to a variable is valid in the sort of the variable.
Condition of transition '' must be
structured by a term (element structure required and non-empty).
Variables in the condition of transition ''
must be of the same (and declared) named sort.
In the condition of transition '', any variable referenced in
the condition must appear at least once either in the input or output arcs of the transition.
In the condition of transition '', any value compared to
a variable must be valid in the referenced sort of the variable.
Checks every specified inscription is non-empty;
any value in a valuation must be valid in the sort of the place connected to the arc (input or output);
any variable in a valuation must be valid in the sort or domain (one sort of the cartesian product)
of the place connected to the arc;
Note : the last two rules do not take reference places into account!
Inscription of arc '' must be
structured by a term (element structure required and non-empty).
In the inscription of arc '', any value must be valid in
the sort of the place connected to this arc (input or output).
Note: this rule does not catch reference places.
Checks every partitionelementof references an existing partition
Referenced partition '' from 'partitionelementof' must be
an actual declared partition.
The arity of the '' operator must be equal to 1.
Checks the sort of every contained partitionelementconstant is the
sort referenced by the containing partition.
The referenced sort by every contained useroperator of partitionelement ''
must be the same as the sort referenced by the usersort sibling of this partitionelement.
Checks the multiset all operator arity is zero; it is applied only on
single sort declarations, not product sorts; its sort is the same as the sort of
the place or arc (or place connected to that arc) it appears on.
The arity of the '' operator in the subtree of element ''
must be equal to zero.
The '' operator in the subtree of element ''
must be applied only on single sort declarations, not product sorts.
The '' operator in the subtree of element '' must be
applied on the same sort as the sort (of the place) associated to that element.
Checks the successor and predecessor operators are not used in initial markings,
their arity is 1 and they are applied on variables whose declarations reference single sorts,
not product sort.
Note : we may have successor(successor($var)) or any arbitrary-long imbricated sequence.
The '' operator must not be used in the initial marking of place ''.
The arity of the '' operator in the subtree of element ''
must be equal to 1.
The '' operator in the subtree of element ''
must be applied only on variables whose declarations reference single sort declarations, not product sorts.
Checks the arity of multisets operators, except all which is already
checked above.
The arity of the multiset '' operator must be equal to 2.
The arity of the multiset '' operator must be greater or equal to 2.
The arity of the multiset '' operator must be equal to 1.
Checks the arity of booleans operators.
The arity of the boolean '' operator must be equal to 2.
The arity of the booolean '' operator must be equal to 1.
The arity of the boolean '' operator must be equal to 0.
Checks the arity of finite int ranges operators,
except finiteintrangeconstant which is already checked above.
The arity of the finite int range '' operator must be equal to 2.
Checks the arity of partitions operators,
except partitionelementof already checked above.
The arity of the partition '' operator must be equal to 2.
Integers are indirectly used in Symmetric nets.
Therefore, we need to also check their operators
The arity of the integer '' operator must be equal to 2.
The arity of the '' operator must be equal to 0.
In a Symmetric net, an arc may connect a place to a
transition or vice versa. It may also connect a place to a referenceTransition (or vice versa)
or a transition to a referencePlace (or vice versa). It may also connect a referencePlace to a
referenceTransition (or vice versa).
In a Symmetric net, a place must be typed, i.e., have a domain.
That domain must refer to an existing built-in sort (e.g., dot, bool) or a named sort,
declared by the user in the declarative part of the net. The corresponding 'type' element,
child of 'place' element, must have a non-empty 'structure' element.
A Symmetric net must have a declarative part. In the case your net doesn't, you must therefore
declare it as a P/T net in high-level notation, where only built-in sorts Dot and Bool are
used, and not required to be declared beforehand. In that case, you may just use elements
'numberconstant', 'dotconstant' and 'booleanconstant' in the terms of the places' initial
marking and arcs' inscriptions.