Checks declarations' id attribute existence

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.