{\rtf1\ansi\ansicpg1252\uc1 \deff5\deflang1033\deflangfe1033{\fonttbl{\f0\froman\fcharset0\fprq2{\*\panose 02020603050405020304}Times New Roman;}{\f5\fswiss\fcharset0\fprq2{\*\panose 00000000000000000000}Helvetica;}
{\f7\fswiss\fcharset0\fprq2{\*\panose 00000000000000000000}Geneva{\*\falt Arial};}{\f234\froman\fcharset238\fprq2 Times New Roman CE;}{\f235\froman\fcharset204\fprq2 Times New Roman Cyr;}{\f237\froman\fcharset161\fprq2 Times New Roman Greek;}
{\f238\froman\fcharset162\fprq2 Times New Roman Tur;}{\f239\froman\fcharset177\fprq2 Times New Roman (Hebrew);}{\f240\froman\fcharset178\fprq2 Times New Roman (Arabic);}{\f241\froman\fcharset186\fprq2 Times New Roman Baltic;}}
{\colortbl;\red0\green0\blue0;\red0\green0\blue255;\red0\green255\blue255;\red0\green255\blue0;\red255\green0\blue255;\red255\green0\blue0;\red255\green255\blue0;\red255\green255\blue255;\red0\green0\blue128;\red0\green128\blue128;\red0\green128\blue0;
\red128\green0\blue128;\red128\green0\blue0;\red128\green128\blue0;\red128\green128\blue128;\red192\green192\blue192;}{\stylesheet{\ql \li0\ri0\nowidctlpar\faauto\rin0\lin0\itap0 \f5\fs24\lang1033\langfe1033\cgrid\langnp1033\langfenp1033 \snext0 Normal;}
{\*\cs10 \additive Default Paragraph Font;}}{\info{\title Summary and Disposition of Comments for FCD15909}{\author University of South Australia}{\operator University of South Australia}{\creatim\yr2002\mo11\dy22\hr9\min16}
{\revtim\yr2002\mo11\dy22\hr9\min16}{\version2}{\edmins4}{\nofpages31}{\nofwords10127}{\nofchars57725}{\*\company University of South Australia}{\nofcharsws70890}{\vern8269}}\paperw11900\paperh16820\margl640\margr640\margt640\margb640
\widowctrl\ftnbj\aenddoc\ftnrestart\noxlattoyen\expshrtn\noultrlspc\dntblnsbdb\nospaceforul\hyphcaps0\horzdoc\dghspace120\dgvspace120\dghorigin1701\dgvorigin1984\dghshow0\dgvshow3\jcompress\viewkind4\viewscale100\nolnhtadjtbl \fet0\sectd
\pgnrestart\linex0\colsx0\sectdefaultcl {\*\pnseclvl1\pnucrm\pnstart1\pnindent720\pnhang{\pntxta .}}{\*\pnseclvl2\pnucltr\pnstart1\pnindent720\pnhang{\pntxta .}}{\*\pnseclvl3\pndec\pnstart1\pnindent720\pnhang{\pntxta .}}{\*\pnseclvl4
\pnlcltr\pnstart1\pnindent720\pnhang{\pntxta )}}{\*\pnseclvl5\pndec\pnstart1\pnindent720\pnhang{\pntxtb (}{\pntxta )}}{\*\pnseclvl6\pnlcltr\pnstart1\pnindent720\pnhang{\pntxtb (}{\pntxta )}}{\*\pnseclvl7\pnlcrm\pnstart1\pnindent720\pnhang{\pntxtb (}
{\pntxta )}}{\*\pnseclvl8\pnlcltr\pnstart1\pnindent720\pnhang{\pntxtb (}{\pntxta )}}{\*\pnseclvl9\pnlcrm\pnstart1\pnindent720\pnhang{\pntxtb (}{\pntxta )}}\pard\plain \qc \li0\ri0\widctlpar\faauto\rin0\lin0\itap0
\f5\fs24\lang1033\langfe1033\cgrid\langnp1033\langfenp1033 {\b\f7\cf1 Summary and Disposition of Comments for FCD15909
\par }\pard \ql \li0\ri0\widctlpar\faauto\rin0\lin0\itap0 {\f7\cf1
\par }{\b\f7\cf1 Date:}{\f7\cf1 17 May 2001
\par
\par }{\b\f7\cf1 From:}{\f7\cf1 Editor of Project 7.19.3
\par
\par }{\b\f7\cf1 Subject:}{\f7\cf1 Disposition Report for FCD15909
\par
\par }{\b\f7\cf1 Work Item:}{\f7\cf1 7.19.3 Petri net techniques
\par
\par }{\b\f7\cf1 Document: }{\f7\cf1 KMJ-013R4
\par
\par }{\b\f7\cf1 Input Documents:}{\f7\cf1
\par
\par 1. SC7/N1947, FCD15909 Ballot, 26/6/1998
\par 2. SC7/N2003 Letter Ballot Summary of FCD15909 Software Engineering - High Level Petri Net Standard, 29/10/1998 (Note: Incorrect UK comments included in this document)
\par 3. KMJ-100 Hugh Davis Email, with Prof Dan Simpson's (UK) comments.
\par 4. KMJ-101 Email from Prof Tad Murata (USA)
\par 5. KMJ-013R1 Draft Summary and Disposition of Comments for FCD15909, 3 November 1998 (Editor)
\par 6. KMJ103 Email from Dan Simpson (UK), 4/11/98.
\par 7. KMJ104 Email from Kurt Jensen (Denmark), 5/11/98.
\par 8. KMJ105 Re: Draft Disposition Report, FCD15909, 18/11/98 (Ekkart Kindler)
\par 9. KMJ106 Re: Draft Disposition Report, FCD15909, 25/4/99 (Editor)
\par 10. KMJ107 Re: Draft Disposition Report, FCD15909, 10 May 1999 (Ekkart Kindler)
\par 11. Karsten Schmidt, 'Parameterized Reachability Trees for Algebraic Reachability Trees', LNCS Vol 935, 1995, Springer, pp 392-411.
\par
\par
\par }{\b\f7\cf1 General}{\f7\cf1
\par
\par In N2003, of the 21 P-members who voted, 17 approved (4 with comments), one disapproved (Germany) with comments, and three abstained (without comments). Thus the FCD has been approved. This means that the final text from the editing meeting will be the te
xt of the standard, so long as it passes the FDIS Yes/No ballot.
\par
\par There were a total of 84 comments received by the editor. The editor has processed comments that were meant to be input by National Bodies, even if they have not been included in N2003 (ie do
cuments 3 and 4 above) as agreed at the Curitiba meeting of SC7/WG11 i May 1999.
\par
\par The editing meeting was officially commenced after all the ballot responses had been received. Some preliminary discussions occurred during the WG11 meeting in Kumomoto, Japa
n, October 1998 via email, as the editor and several other NBs could not be present. A draft disposition of comments document was circulated by email to all representatives of NBs and WG11 experts on 3 November 1998. The editing meeting was left open till
the Curitiba meeting of WG11 as part of the SC7 Plenary in Brazil, in order to finalise the disposition of comments. The UK and Denmark responded positively to the draft disposition accepting all recommendations (see inputs 8 and 9 above). The USA noted t
h
at all its comments had been accepted (see WG11 minutes - SC7 N2036). Australia confirmed it agreed with the disposition. A detailed response from Germany was received on 18 November 1998, and responded to by the editor on 25 April 1999. Comments were res
o
lved (except for the implementation of including symbolic markings) in Germany's response of 10 May 1999. No other responses by NBs were received during this period. The disposition of Japanese comments was agreed to at the Curitiba meeting. Because no re
p
resentative from the German NB was present at the meeting, the editing meeting was kept open, to allow further discussion on symbolic markings. After several rounds of discussions a final circulation of the revised FCD occurred in October 2000. Comments f
rom that circulation have now been incorporated. The disposition is therefore final.
\par
\par Taking each country in turn from N2003, the disposition of comments is as follows:
\par
\par }{\b\f7\cf1 AUSTRALIA (Approve with comments)}{\f7\cf1
\par
\par AUS01 G
\par
\par Australia considers the FCD to be at a mature stage, and ready for progression to FDIS, with a few minor changes (see below).
\par
\par Noted
\par
\par AUS02 E
\par
\par The full title of the FCD should be:
\par
\par FCD15909 Software Engineering - High-level Petri Nets - Concepts, Definitions and Graphical Notation
\par
\par (The secretariat is still using an old title for the cover pages, but the new title is given on page 1)
\par
\par Accept
\par
\par Note: The editor advised the secretariat of this problem on 30 October 1998.
\par
\par AUS03: E Clause 0 Introduction: assemly --> assembly
\par accept
\par
\par AUS04: E Clause 3, 3.1.8 instatiated ---> instantiated
\par accept
\par
\par AUS05: E check all clauses for consistent use of bolding for \'d4note\'d5.
\par accept Need to comply with directives (see JPN006E)
\par
\par AUS06: TL Clause 5, 5.1 Definition, third fly dot replace
\par
\par \'d4D is a non-empty finite set of domains where ...\'d5 with
\par
\par \'d4D is a finite set of non-empty domains, where ...\'d5
\par
\par Partially Accept (see DAN1TH) if modified to retain that D is non-empty.
\par Ed. This is because function Type is not defined if D is empty, except in the speci
al case of both T and P being empty, where we would have the empty function for Type. Hence for all interesting cases where there is at least a transition or a place, D must not be empty.
\par
\par AUS07: E Clause 5, 5.1 Definition
\par
\par At the end of this clause add the following explanatory note:
\par
\par \'d4Note: \\mu PLACE is the set of multisets over the set, PLACE (see Annex A, section A.2).\'d5
\par
\par Accept
\par
\par AUS08: E Clause 5, 5.4 Transition rule
\par
\par Remove the full stop at the end of the equation.
\par
\par Accept
\par
\par }{\b\f7\cf1 DENMARK (Approve with Comments)}{\f7\cf1
\par
\par DAN1 (TH)
\par In section 5.1, the definition of D should be changed from
\par D is a non-empty finite set of domains,.....
\par to
\par D is a finite set of non-empty domains,......
\par Motivation: This is consistent with the usual definitions of Coloured Petri
\par Nets and Predicate/Transition Nets. It is also consistent with the
\par description of Place Types in the beginning of section 6.2.
\par
\par Partially Accept.
\par See AUS06. So long as P union T is not empty, D must not be empty for Type to be defined.
\par
\par DAN2 (TH)
\par In section 6.4 the notation used for multi-sets should be
\par modified. As an example the marking of place A in Figure 1 should be
\par changed from
\par 1 + 2(3)
\par to
\par 1'1 + 2'3
\par Motivation: The use of an infixed operator ' (or *) in multi-sets are more
\par common than the use of parenthesis. Omission of 1-coefficients introduces
\par problems for languages that are strongly typed, since these distinguishes
\par between a token value (such as 34) and a multi-set with one token (such as
\par 1'34).
\par
\par Accept
\par Ed: See discussion on DIN23.
\par
\par DAN3 (TH)
\par Similar changes should of course be made in all those parts of the document where the notation is used (e.g., A.2.1 and Annex C)
\par
\par Accept
\par
\par }{\b\f7\cf1 GERMANY (Disapprove with Comments)}{\f7\cf1
\par
\par DIN ballot vote on FCD 15909, V. 4.0, June 19, 1998
\par
\par DIN agrees with the FCD, provided the following comments are appropriately
\par integrated into the document (in particular Comments #1, #2, and #43):
\par
\par DIN1. Type: Major technical
\par Location: Clause 6, Clause 7
\par
\par Proposal: The definition of High-level Petri Net Graphs (HLPNG) should be
\par defined on a more syntactical level! Up to now, syntactical
\par concepts and semantical concepts are mixed in HLPNG.
\par
\par DIN would be willing to make a technical proposal provided this
\par direction is agreed on. An outline can be found in the appendix
\par of this vote.
\par
\par Rational: The standard claims that HLPNG are syntactical and High-level
\par Petri Nets (HLPN, cf. Clause 5) are semantical. Still, HLPNG
\par uses concepts which are not syntactical such as sets (types) and
\par markings. Therefore, HLPNG are at most semi-syntactical.
\par
\par If HLPNG had syntactical representations of types as sorts and
\par of markings, the concept of parameterized HLPNG would become
\par technically more precise and would fit to a concept called Net
\par Scheme.
\par
\par See also Comment #25
\par **
\par Partially accept.
\par This comment has been discussed at length via email (see inputs 5, 8,9 and 10 above). The outcome is as follows:
\par 1. The main definition will continue to be in the same form as it was - ie places are typed (by sets) rather than sorted.
\par 2. To cater for some analysis techniques, it is desirable to include the notion of symbolic markings as ground terms, as well as the present concrete marking via values from the algebra.
\par 3. Implementation of 2, is probably cleanest if a net scheme is defined (in a similar way to the HLPNG) in a normative annex (favoured by the editor), or else some mention of the sche
me, as well as the definition of symbolic marking via ground terms (favoured by Germany).
\par 4. A compromise has been to include the schema definition in an informative annex.
\par 5. Replace the word 'syntactical' in the last sentence of the first paragraph of clause 6.1, by 'semi-syntactical'.
\par Ed: I believe it would be confusing to include both symbolic markings and concrete markings (from the algebra) in the same definition. Those new to algebraic nets (most of industry) would not know which to use, or why the s
ymbolic marking was there. Therefore it is necessary to separate these concerns. The rationale to include symbolic markings is based on the needs of analysis. However, I dont see why a HLPNG cant be analysed using algebraic net techniques, without symboli
c
markings being in the standard. Since the signature and variables are defined, the analyst just needs to define the appropriate ground terms to define the symbolic marking, and any other apparatus required. As discussed previously in a note in the CD, th
e reason for including a scheme is to allow classes of systems to be defined.
\par
\par DIN2. Type: Major technical
\par Location: Clause 7, Annex A.3.4
\par
\par Proposal: The definition of multiset terms (BTERM) should allow more
\par general forms of expressions. In particular, there should be
\par a mechanism to define ones own BTERM operations.
\par
\par Again, DIN would be willing to make a technical proposal
\par provided this direction is agreed on. An outline can be found
\par in the appendix of this vote.
\par
\par Rational: Up to now, there are many (practically relevant) HLPN which
\par cannot be expressed as a HLPNG due to syntactical restrictions
\par of BTERMs In particular, Coloured Petri Nets according to
\par Jensens book cannot be represented as a HLPNG.
\par
\par Overtaken by events. It turns out that terms are powerful enough to express the flexibility we need, so long as the appropriate operators are defined in the signature. After considerable technical discu
ssion by email (inputs 5, 8, 9 and 10 above), it has been agreed that BTERMs will be abolished, and that arcs will be annotated by terms that when evaluated for the algebra result in a multiset over the associated place's type. That is replace the definit
ion of A with
\par
\par - A : F --> TERM(O \\cup V) such that for all (p,t), (t',p) \\in F,
\par for all bindings \\alpha, Val_\\alpha(A(p,t)), Val_\\alpha(A(t',p)) \\in \\mu Type(p)
\par
\par This allows 'multiset' terms to be built using an appropriate signature - see input 9.
\par
\par DIN3. Type: Minor editorial
\par Location: Clause 0, p. 6, l. 16
\par
\par Proposal: Replace `forms of high-level net' by `forms of high-level nets'
\par (pl.)
\par
\par Rational: Plural
\par
\par Accept
\par Ed: The original is also acceptable as high-level net is used to mean a class of nets in this context.
\par
\par DIN4. Type: Minor editorial
\par Location: Throughout
\par
\par Proposal: Capitalization of High-level Petri Nets and other concepts
\par should be handled in a uniform way.
\par
\par Rational: Up to now, there are different versions at different
\par locations (e.g. High-level Petri nets at p. 6, l. 11,
\par High-level Petri Nets at p. 6, l. -9, and
\par high-level Petri nets at p. 7, l. 10)
\par
\par Accept (see also JPN 001)
\par
\par DIN5. Type: Minor technical
\par Location: Clause 3.1.1.3
\par
\par Proposal: Omit `(on variable substitution)'.
\par
\par Rational: Evaluation is quite a different operation than substitution;
\par evaluation is semantical (a term is evaluated to some value in
\par some domain); substitution is syntactical (in a term variables
\par are replaced by some terms; the result is another term which is
\par still a syntactical object).
\par
\par Accept
\par Ed: It is not term substitution that is meant, but substitution of a value for each of the variables. Probably '(for an assignment of values to variables)' would have been better, but this is probably not needed.
\par
\par DIN6. Type: Minor technical
\par Location: Clause 3.1.10
\par
\par Proposal: The clause should read: `A multiset of transitions associated
\par with a mode' ...
\par
\par Rational: A mode does not have an explicit reference to its transition
\par (think of two transitions with the same set of variables, then
\par it is not clear to which transition the mode refers to).
\par Therefore, the transitions must be mentioned explicitly.
\par
\par Reject.
\par Ed: There are several difficulties. DIN point out an ambiguity, if transition modes do not include the tra
nsition in their definition. The standard currently uses the term 'transition mode' in clause 5, to mean a pair (t,m) which includes the transition, as well as a value (see 5.3). In Clause 7.4, the term 'mode' is used to mean an assignment to variables fo
r
a transition, which satisfies its guard. Definition 3.1.26.2 seems to define transition mode to mean the same thing as mode. I believe the way over this is to tighten the definitions in clause 3.1.26.2, so that this distinction is clear, and so that the
current definition (clause 3.1.10) concerning transition modes is maintained.
\par
\par DIN7. Type: Minor editorial
\par Location: Clause 3.1.10
\par
\par Proposal: Replace `the demand placed on them' by `the demand imposed on them'
\par
\par Rational: The word `place' might be misleading in the context of Petri nets
\par
\par Accept
\par Ed: this will also be changed in 3.1.9, and any other occurrences I find!
\par
\par DIN8. Type: Minor technical
\par Location: Clause 3.1.13
\par
\par Proposal: Replace `comprising a set of sets' by `comprising a sequence of
\par sets' or by `comprising a list of sets'
\par
\par Rational: In an algebra, there may well be two equal sets which correspond
\par to two different sorts (of a signature). These two sets should
\par be distinguished --- as usual in Algebraic Specifications.
\par
\par Reject
\par After significant discussion (see 5, 8, 9 and 10), no technical problem was discovered with the approach taken in FCD15909, and it does appear to be simpler than the approach taken in some standard texts on algebraic specification.
\par
\par DIN9. Type: Minor editorial
\par Location: Clause 3.1
\par
\par Proposal: Unify Capitalization of headings of clauses and of words
\par after colon.
\par
\par Rational: Cf. Place and place in Clauses 3.1.14.2 and 3.1.14.3
\par
\par Accept
\par
\par DIN10. Type: Minor editorial
\par Location: Clause 3.1.15.1
\par
\par Proposal: Replace `a set element in a corresponding' by `an item in a'
\par
\par Rational: The original version is misleading due to the use of sets and
\par multisets
\par
\par Accept
\par Ed: This matches better with 3.1.15
\par
\par DIN11. Type: Minor editorial
\par Location: Clause 3.1.18
\par
\par Proposal: Replace `instatiated' by `instantiated'
\par Rational: Spelling
\par
\par Accept - see also AUS04 and USA2
\par
\par DIN12. Type: Minor editorial
\par Location: Clause 3.1.22
\par
\par Proposal: Replace `An' by `A'
\par
\par Rational: Spelling
\par
\par Accept
\par
\par DIN13. Type: Minor technical
\par Location: Clause 3.1.24.2
\par
\par Proposal: Omit `, and their reduction to simplest form'
\par
\par Rational: Evaluation is a semantical operation; it need not be operated
\par by reducing terms (cf. Comment #5)
\par
\par Accept intent
\par Ed: The idea here is expressed in the following example. For f(x) = 2x, g(y) = 5y, with
\par x,y:Nat, and the term 2(f(x))+3(4)+g(y), its value for the assignment (x,y)<- (2,1) is
\par 2(f(2)) + 3(4) + g(1) (binding/assignment/substitution)
\par = 2(4) + 3(4) + 1(5) (function computation)
\par = 5(4) + 1(5) (reduction to simplest form)
\par
\par It is accepted that there is not strictly a 'simplest form', and the following replacement text is offered:
\par
\par 'and any simplications performed (such as gathering like terms to obtain the symbolic sum representation of a multiset).'
\par
\par DIN14. Type: Minor technical
\par Location: Clause 3.1.26.4
\par
\par Proposal: Replace `multiset of transition modes' by
\par `multiset of transitions associated with a mode'
\par
\par Rational: See Comment #6
\par
\par Reject
\par Ed - see comment on DIN6
\par
\par DIN15. Type: Minor technical
\par Location: Clause 5.1, p. 11, l. -1
\par
\par Proposal: Replace `set' by `sequence' or `list'
\par
\par Rational: See Comment #8
\par
\par Reject
\par Ed - see comment for DIN8
\par
\par DIN16. Type: Minor editorial
\par Location: Clause 5.1, 5.2, 5.3
\par
\par Proposal: Replace TRANS by ACTION and PLACE by ITEM
\par
\par Rational: The abbreviations TRANS and PLACE are misleading and
\par can be easily confused with sets P and T.
\par
\par Reject
\par Ed - TRANS is the set of transition modes, and corresponds to P/T net transitions in an unfolding. Hence TRANS (not T) is an appropriate name. Similar argument for PLACE (not P).
\par
\par DIN17. Type: Minor technical
\par Location: Clause 5.4
\par
\par Proposal: Define Post(T_\\mu) explicitly and not as linear extension.
\par
\par Rational: The linear extension of an arbitrary function does not
\par necessarily exist! Think of an infinite multiset and
\par a function which maps all items to the same element.
\par
\par Maybe, the non-existence of some linear extensions is a
\par good reason to forbid infinite multisets. Cf. Comment #35
\par
\par Reject proposal, but accept the comment and add the word 'finite' before multiset at the beginning of 5.4:
\par 'Given that a finite multiset of transition modes, T_\\mu, ...'.
\par
\par DIN18. Type: Minor technical
\par Location: Clause 5.4
\par
\par Proposal: Add parentheses in the equation defining M'
\par
\par Rational: Otherwise the equation might be interpreted in a wrong way.
\par
\par Reject.
\par Ed. It follows the usual precedence rules, which are made clear in A.2.6. Addition of parentheses is therefore unnecessary, and clutters the rule.
\par
\par DIN19. Type: Minor editorial
\par Location: Clause 5.4
\par
\par Proposal: Omit `(up to the maximum)'
\par
\par Rational: The statement could suggest that a maximum does always exists,
\par which is not true. Since only finite steps are allowed, there
\par is no maximum number of transitions if there are enough tokens
\par for infinite concurrency.
\par
\par Accept
\par
\par DIN20. Type: Minor technical
\par Location: Clause 6.2
\par
\par Proposal: Replace `The expressions are evaluated by substituting values
\par for the variables' by `For each binding of variables, the
\par expression evaluates to some value.'
\par
\par Rational: See Comment #5
\par
\par Compromise. To avoid confusion with term substitution, the word 'substitution' will not be used. The above sentence in clause 6.2 is replaced by:
\par 'The expressions are evaluated by assigning values to each of the variables.'
\par The editor will search for all occurrences of 'substitution', and replace it appropriately (using assignment or binding).
\par
\par DIN21. Type: Minor technical
\par Location: Clause 6.2
\par
\par Proposal: Replace all `collection' by `multiset'; the Note can be
\par omitted
\par
\par Rational: By now, the concept of multiset should be known to the reader
\par of the standard.
\par
\par Reject. Leave as is, to promote the standard to a wider audience, and provide a link with the tutorial.
\par
\par DIN22. Type: Minor technical
\par Location: Clause 6.3.1, l.4
\par
\par Proposal: Omit `or substitution'
\par
\par Rational: See Comment #5
\par
\par Accept - see DIN20.
\par
\par DIN23. Type: Minor technical
\par Location: Clause 6.3, Clause 6.4, p.15, Fig. 1, Clause Annex A.3.4
\par
\par Proposal: Use of `[ 1, 3, 3]' as notation for a marking would be
\par more readable.
\par
\par Rational: The Notation `1 + 2(3)' gives rise to many misunderstandings:
\par + might be interpreted as plus on numbers
\par 2(3) might be interpreted as multiplication of two numbers;
\par parentheses should carry no meaning than structuring of
\par expressions!
\par Cf. Comment #32
\par
\par Reject Proposal but accept the rationale. This relates to DAN2 which DIN accepts. DAN2 scales well, whereas the above proposal does not. (Consider if there were one hundred 3s, the square bracket notation would be unworkable.) Given that a marking is def
ined as a multiset, and the symbolic sum representation is defined in A.2.1, there should be no ambiguity.
\par
\par DIN24. Type: Minor editorial
\par Location: Clause 6.4. p15, l. -3 to -1
\par
\par Proposal: Replace `square (more generally by a rectangle)' by
\par `rectangle (in this case a square)'
\par
\par Rational: Otherwise, there is an asymmetrie between the graphical
\par representation of places and transitions. Therefore, the
\par general case should occur outside parentheses in both cases
\par (or vice versa).
\par
\par Accept
\par Ed: A bit of English variety has no place in a standard!
\par
\par DIN25. Type: Major technical
\par Location: Clause 7
\par
\par Proposal: The algebra H as well as references to it should not occur
\par within the definition of HLPNG. Omit $H$ completely and
\par replace
\par
\par Type by Type: P --> S
\par M_0 by a syntactical object (cf. Comment #1 and Appendix)
\par
\par Rational: HLPNG should only consist of syntactical objects
\par Cf. Comment #1 and Appendix
\par
\par Reject - see response to comment 1.
\par
\par DIN26. Type: Minor technical
\par Location: Clause 7.2, p. 19, ll. 1-2
\par
\par Proposal: Omit `for Type(p) = H_s' and replace `BTERM(O \\cup V)'
\par by `BTERM(O \\cup V)_\{Type(p)\}'
\par
\par Rational: More concise notation, comprehensibility.
\par
\par Overtaken by events - BTERMs are abolished - See comment for DIN2.
\par
\par DIN27. Type: Minor editorial
\par Location: Clause 7.2, p. 19, l. 3
\par
\par Proposal: Replace `with a multiset of terms' by `with a multiset term'
\par
\par Rational: This is needed due to the change in the previous version; arcs
\par are inscribed by a multiset term (cf. Annex A.3.4)
\par
\par Overtaken by events - see comment for DIN2 (arcs will be annotated by terms).
\par
\par DIN28. Type: Minor editorial
\par Location: Clause 7.4
\par
\par Proposal: Replace `assign_\{bool\}' to `Val_\{\\alpha\}' etc.
\par
\par Rational: Otherwise, there is no link from \\alpha to assign_\{bool\}
\par see Annex A.3.6 (but even there, there are some inconsistencies
\par cf. Comment #41)
\par
\par Accept intent.
\par Ed: assign is used for terms (see A.3.6) whereas Val is used for multiset terms, not terms. Since TC is a term, assign is the correct function for the evaluation. However, because BTERMs no longer exis
t, the function Val is now used for terms (assign is abolished), and hence Val_\{bool, \\alpha_\{t\}\}(TC(t)) = true is now used in clause 7.4.1.
\par
\par DIN29. Type: Minor technical
\par Location: Clause 7.5
\par
\par Proposal: Add parentheses to the definition of M'
\par
\par Rational: Dissolve ambiguities (cf. Comment #18)
\par
\par Reject
\par Ed: same reason as in response to DIN18
\par
\par DIN30. Type: Minor technical
\par Location: Clause 8.2
\par
\par Proposal: Replace `the name of the type (Type(p))' by `sort'
\par
\par Rational: Otherwise Type(p) is a set which
\par has no name at all! But the sort of the Signature would do
\par because it is a syntactical object.
\par Cf. Comments #1, #25, and Appendix
\par
\par Reject.
\par Ed: This is subtle. Because the HLPNG is purposely defined concretely (us
ing the algebra) (see response to DIN1), different sorts may be mapped to the same set in the algebra (see DIN8). eg H_s1=H_s2=Z (the integers). The idea is to label the place with the name of the place's type (eg Z), because the HLPNG is operating at the
concrete level. Associating different sorts to places, which are typed the same, would be confusing.
\par
\par DIN31. Type: Minor editorial
\par Location: Clause 8.3
\par
\par Proposal: Replace `A Transitions' by `A transition'
\par
\par Rational: Typo?
\par
\par Accept: Replace the capital T by lower case (t).
\par
\par DIN32. Type: Minor technical
\par Location: Clause 8.4, Annex A.2.1
\par
\par Proposal: There should be an explicit symbol for multiplication
\par of multisets by natural numbers; e.g. `. x .'
\par
\par Rational: Parentheses should not be overloaded; in case of multisets
\par over numbers parentheses are ambiguous! Cf. Comment #23.
\par
\par Accept intent
\par DAN2 and the response to DIN23 solves this problem.
\par
\par DIN33. Type: Minor technical
\par Location: Clause 9, p. 22
\par
\par Proposal: The definition of the semantics of HLPNG can be significantly
\par simplified in the following way:
\par
\par Define
\par Type(t) = \{\\alpha: V_t --> S |
\par \\alpha is an assignment such that
\par Val_\{\\alpha\}(TC(t)) = true \}
\par
\par where V_t is the set of variables associated with transition t.
\par
\par Then, the lambda-expressions and TC' are not needed any more.
\par
\par Pre(p,t) can be defined as Val_\{\\alpha\}(A(p,t)) and
\par Post(p,t) as Val_\{\\alpha\}(A(t,p)).
\par
\par
\par Rational: Lambda expressions and TC' are not necessary and make the
\par concepts more difficult to understand.
\par
\par Accept intent
\par Ed.
Although the current version is technically correct, this is a useful simplification as stated in the above rationale, we dont have to introduce new notions (Lambda expressions). The technical details need refinement. The following change incorporates th
e intent of this comment.
\par
\par In Clause 9,
\par
\par Given the removal of BTERMs and replacement of assign by Val for terms in A.3.6,
\par
\par 1. replace the first two paras of page 23 (point 3) by
\par
\par Define V_t \\subseteq V as the set of variables associated with transition t.
\par Define \\alpha_t as an assignment for H and V_t (cf A.3.6).
\par
\par Then Type(t) = \{\\alpha_t | Val_(bool,\\alpha_t)(TC(t)) = true\}
\par
\par 2. replace point 5 by
\par
\par The pre and post maps are given, for all (p,t), (t,p)\\in F, by the following family of mappings:
\par
\par Pre_(p,t) : Type(t) ---> \\mu Type(p)
\par Post_(p,t) : Type(t) ---> \\mu Type(p)
\par
\par For (p,t)\\notin F ... (as before).
\par
\par Thus for all t\\in T, and for all m\\in Type(t)
\par
\par Pre(t,m) = \{(p,b)| p\\in P, b\\in Pre_(p,t)(m)\}
\par Post(t,m) = \{(p,b)| p\\in P, b\\in Post_(p,t)(m)\}
\par
\par where Pre_(p,t)(m) = Val_\{alpha_t = m\}(A(p,t))
\par and Post_(p,t)(m) = Val_\{alpha_t = m\}(A(t,p))
\par
\par DIN34. Type: Major technical
\par Location: Clause 10.1.1
\par
\par Proposal: Omit l. 4--8
\par
\par Rational: The status of this part is not clear at all! Is it normative?
\par Is it an implicit norm for place transition systems?
\par A norm for P/T-systems should not be defined as a special
\par case of P/T-systems because of mathematical overhead.
\par Cf. Comment #43
\par
\par Reject
\par The clause is norma
tive. The US requested that 'Petri nets' be defined as a subclass, in their vote of disapproval of the CD. It was always intended to define subclasses in a normative annex, which has been included in all drafts of the standard. Given the major nature of t
h
e change, and that 17 countries have approved this version, its removal is not possible. I would agree with DIN that the specialisation of the definition of the HLPNG results in large mathematical overhead, but it does show the relationship. Note that a m
ore usual definition of 'Petri nets' is given at the end of B1.
\par
\par DIN35. Type: Minor technical
\par Location: Clause Annex A.2
\par
\par Proposal: Perhaps, multisets should be restricted to finite multisets
\par
\par Rational: Only for finite multisets all functions have a
\par linear extension. Cf. Comment #17.
\par
\par Ed: This has been dealt with in the response to DIN17.
\par
\par DIN36. Type: Minor technical
\par Location: Clause Annex A.3.1, A.3.3
\par
\par Proposal: Separate variables from signatures
\par
\par Rational: Defining variables within signatures is very unusual. In
\par particular, it makes a change of the signature necessary, when
\par a new variable is introduced.
\par
\par Accept
\par Ed: On the basis that it may make the standard easier to read. This affects clause 7.2 (inclusion of V in the HLPNG tuple, change def of Sig, etc) and A.3.1, A.3.3 and B.1.
\par
\par DIN37. Type: Minor technical
\par Location: Clause Annex A.3.3
\par
\par Proposal: Omit `For s, s_1, ..., s_n \\in S (n > 0)' on p. 26, l. -1 and
\par include it into the third item on p. 27, l.3.
\par
\par Rational: Otherwise, the binding of n and the s_i is in the wrong way;
\par n is fixed before the operator an its arity is known. In
\par particular, n may change for each operator. To make the
\par definition mathematically sound, the binding must not be global.
\par
\par Accept intent.
\par Ed. This is subtle but important for the induction to work correctly. The agreed proposal is to leave 'For s\\in S' on page 26, as it is needed for points 1 and 2 (as well as 3) on page 27, but then to state at the beginning of 3. `For s_1, ..., s_n \\
in S (n > 0)', in alignment with DIN's proposal.
\par
\par DIN38. Type: Minor technical
\par Location: Clause Annex A.3.4
\par
\par Proposal: Add subscript `s' for each BTERM(O \\cup V)
\par
\par Rational: Otherwise BTERM(O \\cup V)_\{s\}is not defined (but used)
\par
\par Overtaken by events, since there is no longer any need for BTERMs, the problem no longer exists.
\par
\par DIN39. Type: Minor technical
\par Location: Clause Annex A.3.4
\par
\par Proposal: Add a forth way for defining BTERMS:
\par
\par * If u is a term of sort boolean and b is a BTERM,
\par then [u] b is a BTERM
\par
\par Rational: Otherwise, the abbreviations defined below are not really
\par defined; e.g. [m = e] b
\par
\par NOTE: Perhaps, there should be another notation not using square brackets
\par which are proposed to denote multiset in these comments.
\par
\par
\par Overtaken by events as BTERMs are no longer required.
\par Ed. The User is free to choose any operator symbols, so there is no need to define it in the standard.
\par
\par DIN40. Type: Minor technical
\par Location: Clause Annex A.3.5
\par
\par Proposal: For Boolean and Natural signatures there should be an
\par explicit requirement, that the sets associated with bool
\par and nat are \{false, true\}and the natural numbers, respectively.
\par
\par Rational: Otherwise, being a Boolean or Natural signature is only a
\par syntactical requirement which is not reflected in the semantics.
\par
\par Agree with intent.
\par Ed. In A.3.2 this correspondence is given in paragraphs 1 and 2, so it is already taken into account. However, clause A.3.2 has been revised in the light of deleting clause A.3.4 (BTERMs), as there is no longer a requi
rement for a Natural signature. Clause A.3.2 now comprises just the first paragraph, further clarified to ensure that these concerns are taken into account.
\par
\par DIN41. Type: Minor technical
\par Location: Clause Annex A.3.6
\par
\par Proposal: Replace assign by Val
\par
\par Rational: See Comment #28
\par
\par Accept (overtaken by events)
\par Ed: assign is used for terms, whereas Val is used for multiset terms (see DIN28, DIN33). With the removal of multiset terms (BTERMs), Val is now used for terms in preference to assign. This has been done consistently throughout.
\par
\par DIN42. Type: Minor technical
\par Location: Clause Annex A.3.6
\par
\par Proposal: In analogy to Clause A.3.3 the binding of \\sigma, s and n
\par should be made in the third item.
\par
\par Moreover, the items should be numbered as in A.3.3
\par
\par Rational: See Comment #37
\par
\par Accept intent in a similar way to DIN37.
\par
\par DIN43. Type: Major technical
\par Location: Clause Annex B
\par
\par Proposal: Omit Annex B or make it informative.
\par
\par If this Clause is not omitted, call Clause B.1
\par Place/Transition Systems (P/T-systems). The name `Petri net'
\par does not stand for a particular version of Petri nets.
\par
\par Rational: The standard should be for high-level Petri nets. By the
\par definition of place transition systems as special cases there
\par would be a standard for low-level nets either; but defining
\par place transition systems as special case of high-level nets
\par is not appropriate.
\par
\par Reject but accept the intent of the comment
\par Ed: see response to DIN34. The change of name from Petri nets to Place/Transition Systems is problematic, as the usual definition of P/T systems includes place capacity. It is agreed that Petri nets is n
ot a good name, because that term is used loosely. It has been agreed to use the term 'Place/Transition nets' for this class of net, with an appropriate change to the introductory paragraph of Annex B.
\par
\par DIN44. Type: Minor editorial
\par Location: Bibliography, p. 41, l.8
\par
\par Proposal: Replace `Grunlagen' in B. Baumgarten's book by `Grundlagen'
\par
\par Rational: Typo
\par
\par Accept.
\par -----------------------------------------------------------------------------
\par
\par Appendix
\par ========
\par
\par This appendix gives a brief outline, how the to separate syntax and semantics
\par more clearly in HLPNG. Moreover, it shows how BTERMS can be more general and
\par (and in part be specified by the user). This text is based on a communication with the editor of the Standard, J. Billington.
\par
\par If the committee agrees on a clearer separation of syntax and semantics, DIN
\par would be willing to work out these idea in more detail.
\par
\par
\par Including Flexibility
\par =====================
\par
\par The basic idea is to implicitly associate each sort s of some signature
\par SIG = (S,O) with a CORRESPONDING MULTISET (or bag) SORT b(s). Then,
\par operators (resp. the arity of the operators) of the signature may be on
\par sorts s as well as on sorts b(s); for clarity I will distinguish this kind
\par of signatures by calling them multiset (or bag) signatures.
\par
\par In the following I will roughly sketch a formalization of these concepts; if
\par you like these concepts I could formalize them in the style of the standard.
\par
\par
\par A MULTISET (or bag) SIGNATURE is a tuple BSIG = (S,O), where S is a finite
\par set of SORTS and O is a finite set of OPERATORS. Each sort s \\in S is
\par (implicitly) associated with a unique sort b(s). We define
\par BS = S \\cup \{b(s) | s \\in S \}
\par Each operation o \\in O is associated with an ARITY of BS* x BS. For clarity
\par I will use symbol s for elements of S only; I will use z for elements of BS.
\par
\par Then, TERMS can be defined as usual: For a sorted set of BSIG-variables
\par V = (V_z)_\{z \\in Z\}we define:
\par - for o \\in O_(\\epsilon,z) we have o \\in TERM(SIG,V)_z
\par - for v \\in V_z we have v \\in TERM(SIG,V)_z
\par - for o \\in O_(z1...zn,z) and ei \\in TERM(SIG,V)_\{zi\}
\par we have o(e1,...,en) \\in TERM(SIG,V)_z
\par
\par The BTERTMs used in the current version of the standard can be defined as
\par follows: For each s \\in S BTERM(SIG,V)_s = TERM(SIG,V)_b(s).
\par Basically, the uppercase B has moved from the front to a lowercase b
\par at the end.
\par
\par The standard operations on BTERMS (cf. A.3.4) can be included in any
\par multiset algebra by definition (if you want to): For each s \\in S
\par the set of operators O should contain the following operations:
\par
\par [.] : s --> b(s) (this makes an element of sort as a singleton multiset)
\par . x . : Nat x b(s) --> b(s)
\par . + . : b(s) x b(s) --> b(s)
\par
\par
\par
\par Now, what is an algebra corresponding to BSIG = (S,O): A tuple H = (S_H, O_H)
\par is a multiset algebra, if S_H is a family of sets which associates each sort
\par s \\in S with a set H_s. Moreover, we define H_\{b(s)\}= \\mu H_s;
\par i.e. H_\{b(s)\}is a multiset over the set H_s corresponding to sort s.
\par Moreover, for each operation o(z1...zn,z) \\in O there is an operation
\par o_H \\in O_H such that o: H_z1 x ... x H_zn --> H_z.
\par
\par If you have the standard operations on multiset included by definition, we
\par of course need to define that the corresponding operations in the algebra
\par behave accordingly.
\par
\par That's it.
\par
\par
\par What is more as long as BSIG does not contain any additional operations
\par which refer to a sort b(s), there is no difference to the current version of
\par the standard.
\par
\par
\par Separation of Syntax and Semantics
\par ==================================
\par
\par In addition to the above proposal, I would like to plead (again) for a
\par clearer separation of syntax and semantics in the standard! I appreciate
\par the distinction of high-level Petri nets and high-level net graphs. The
\par main motivation (see introduction) seems to be the separation of syntax
\par and semantics. This is achieved for transition inscriptions and
\par arc-inscriptions; but, not for markings.
\par
\par The inscriptions Type is semantical since each place is associated with a
\par set. Why don't we use Type: P --> S; then this inscription is also
\par purely syntactical. The initial marking could be syntactically represented
\par by M: P --> BTERM(SIG) such that M(p) \\in BTERM(SIG)_Type(p).
\par In my opinion the syntactical representation does not contradict the fact
\par that markings are changing dynamically. Similar to the correspondence of
\par syntactical arc-inscriptions to the semantical concepts of Pre and Post, there
\par is a correspondence between the syntactical representation of markings to
\par the markings of high-level Petri nets. There is no reason to consider
\par markings to be `more semantical' than arc-inscriptions, isn't it?
\par
\par To sum up: Everything (except for the algebra itself) in net graphs
\par can and should be syntactical. This would support the compatibility with
\par the concepts of net schemes. Indeed in that case, a net scheme is just
\par a net graph without an algebra.
\par
\par ------------------------------------------------------------------------
\par
\par }{\b\f7\cf1 JAPAN (Approve with Comments)}{\f7\cf1
\par
\par JPN 001 E: Unify the spelling for "High-level Petri Net". For example,
\par followings are used:
\par Line 34 of Page 6 "High-level Petri Nets"
\par Line 3, 9 of Page 7 "High-level Petri nets"
\par Line 34 of Page 8 "High-level Petri Net"
\par Line 23 of Page 11 "High-level Petri nets (HLPN)"
\par Line 8 of Page 13 "HLPNs"
\par
\par Also, unify for "High-level Petri Net Graph":
\par Line 36, 41 of Page 6 "High-level Petri Net Graph"
\par Line 9 of Page 13 "High-level Petri net graph (HLPNG)"
\par Line 17 of Page 13 "High-level Petri Net Graph"
\par Line 2 of Page 14 "HLPNGs"
\par
\par Accept - see also DIN4
\par Ed. High-level Petri Net, and High-level Petri Net Graph are now used throughout the document.
\par
\par JPN 002 E: Replace the followings with "HLPNG" according to the definition of Line 9 in Page 13.
\par Figure 1 of Page 15 "HLPN-Graph"
\par Figure 2 of Page 17 "HLPN Graph"
\par Line 25 of Page 21 "HLPN Graph"
\par
\par Accept the above 2 (figure captions), but for clarity in a major heading, spell out in full to be consistent with other major headings. This helps with the table of contents, where the reader has not yet come across the abbreviations.
\par
\par JPN 003 E: P.3, Contents: The table of contents shall not include sub-sub
\par clause to conform to "6.1.2 Table
\par of contents (p.34)" of the ISO/IEC Directives Part3, 1997.
\par
\par Rejecte
d. The ISO/IEC Directives Part3, 1997, p3, uses 3 levels of headings in its own table of contents, and this is standard type setting practice enforced by good word processors (like LaTeX). (This is a too literal reading of clause 6.1.2 (on page 19) of t
he Directives.)
\par
\par JPN 004 E: P.8, 3 Terms and Definitions: The introductory wording should be added to conform to
\par "6.3.1 Terms and definitions (p.38)" of the ISO/IEC Directives Part3,
\par 1997.
\par
\par Accepted.
\par Ed: My reading of the Directives suggests that Clause 3 should be Terms and Definitions, and Clause 4 should be Symbols and Abbreviated Terms. This is a bit of work for the editor renumbering the definitions.
\par On closer reading of the directives, having abbreviations and terms and definitions in the one clause is allowed, so long as the heading is changed appropriately - see the last para of the Directives clause 6.3.2 (page 21).
\par
\par
\par JPN 005 E: Symbols, such as mathematical symbols, should be listed in the
\par clause titled "Symbols and
\par abbreviated terms" to conform to "6.3.2 Symbols and abbreviated terms
\par (p.38)" of the ISO/IEC
\par Directives Part3, 1997.
\par
\par Accepted.
\par It was agreed at the Curitiba meeting for the Petri net specific mathematical notation, M[T_\\mu\\rangle M', be defined in clause 4.
\par
\par JPN 006 E: P.11, L.19: "Note: " shall read as "NOTE ".
\par
\par Accepted
\par
\par JPN 007 E: P.12, L.21: "M[T >M' " should read as "M[T >M']".
\par
\par Rejected. The current notation is correct, the suggested change will make it incorrect.
\par
\par JPN 008 E: P.13, L.27, L.31: The meaning of "x" and "y" used in "f(x)" and
\par "x
\par Subject: Re: Draft Disposition Report, FCD15909 (Second try)
\par
\par Dear Jonathan,
\par
\par by now, I have had a closer look at your comments and at your new proposal
\par concerning the PN-standard.
\par
\par I do agree that we are converging. In order to make sure that I did
\par understand the basic changes in your new proposal, let me briefly rephrase
\par them in my words:
\par
\par 1. In the new version, there will only the concept of terms (no BTERMS any-
\par more); but there will (must) be terms which evaluate to multisets
\par in the corresponding algebra.
\par
\par 2. An arc-inscription is legal if it evaluates to a multiset
\par of the sort/type corresponding to the involved place for all assignments.
\par
\par 3. There will be a semantical (concrete) concept of a marking and a (more)
\par syntactical concept of a marking.
\par
\par This way, the version of algebraic Petri nets as defined by the standard
\par allows sufficient `flexibility'. Therefore, we can live with this new
\par proposal.
\par
\par One problem, however, is the schema aspect, were a schema is an algebraic net
\par without a fixed algebra. Without a fixed algebra, we cannot define legal
\par arc-incriptions anymore (because evaluation of terms is no longer possible).
\par This would require a more syntactical definition (as proposed in my previous
\par comment). One way out of this is to define a schema as a HLPN with a
\par set (or rather a class) of associated algebras; then, an arc-inscription of a
\par HLPN-schema is legal, if the term evaluates to a multiset of the corresponding
\par sort in all algebras for all assigments. This seems to be in the spirit of
\par the definition of HLPN. What do you think of that?
\par
\par Still, I tend not to include the schema aspect into the standard.
\par But, it would be nice to have at least some hints on schemas and on the
\par relation of HLPNs to schemas in the standard.
\par
\par Even if schemas do not occur in the standard, I propose to have a concrete
\par concept of markings as well as a syntcatical concept of markings (ground terms
\par which evaluate to multisets)---this makes sense for some analyis algorithms
\par (cf. my previous emails).
\par
\par
\par I hope this helps to settle our discussion.
\par
\par
\par Best wishes,
\par Ekkart
\par --
\par PS: Concerning the meeting in Brazil: Unfortunately, I don't have the money
\par to come to this meeting (I rather spend it for visiting Williamsburg).
\par -------------------------------------------------------------------------
\par }{\b\f7\cf1 Email to Kindler on 24 April 1999}{\f7\cf1 (input 5.2, which includes input 5.1 - both circulated to WG11 members by email)
\par
\par Dear Ekkart,
\par
\par It is a long time since you made your input on the standard, and I am now just starting to get back into it, due to pressure of other pressing things.
\par
\par Many thanks for all the thought you have put into this.
\par Please see my comments below. I think we are converging.
\par
\par I would like to come to a conclusion about this as soon as possible, to get the disposition and the final text agreed in the next couple of weeks for ratification at the WG11 meeting in Curitiba, Brazil, in the last week of May - if at all possible.
\par
\par Best regards - Jonathan
\par
\par >Dear Jonathan, dear Members of WG11, dear Petri net experts,
\par >
\par >in the Draft Disposition Report on FCD 15909 some fundamental changes
\par >of the DIN FCD1509 vote have been rejected. We are convinced that
\par >the proposed changes are important and will significantly improve the
\par >standard and its acceptance. Therefore, I will try to convince other
\par >national bodies of the significants of these changes and to vote in favour
\par >of these changes.
\par >
\par >Kind regards,
\par >Ekkart Kindler
\par >
\par >==========================================================================
\par >This DIN reply to the Draft Disposition Report on FCD 15909 is structured
\par >as follows:
\par >
\par > I. Arguments for a clearer separation of syntax and semantics
\par >
\par >
\par > II. Proposed changes
\par >
\par > 1. For separation of syntax and semantics
\par >
\par > 2. Customizable operations on BTERMS
\par >
\par >
\par > III. Detailed reply to comments in the Draft Disposition Report
\par >
\par >
\par >I. Arguments for a clearer separation of syntax and semantics
\par >-------------------------------------------------------------
\par >
\par >DIN has proposed a version of HLPNG which is purely syntactical (see DIN1).
\par >As it stands, HLPNG are not purely syntactical because types as inscriptions
\par >of places and markings are semantical.
\par >
\par >There are several reasons for a clear separation of syntax and semantics.
\par > 1. When using HLPNG (in particular when implementing a tool), there needs to
\par > be a syntax for these annotations anyway. Maybe there is a common sense
\par > syntax for some types (e.g. natural numbers); but in general there is no
\par > such syntax (see below).
\par
\par The standard only provides an abstract syntax - the form of the syntax by terms - but
\par no notation for types, operators etc is mandated here - what
is mandated is the semantics via clause 5. This allows different syntaxes, but with a common semantics. It provides the possibility of translating between the different syntactic variants. In implementing a tool, a concrete syntax needs to be defined. Th
is is currently not within the scope of this standard, and it would be extremely difficult to get consensus on this, given the different tools in the market place. It would also take a lot more work, and can't be included in this standard.
\par >
\par > 2. There are some analysis methods for high-level Petri nets, which need
\par > a purely syntactical representation of a marking. Here are two examples:
\par >
\par > M. Lindquist: Parameterized reachability trees for predicate/transition
\par > nets. PhD thesis. Acta Polytechnica Scandinavica, Ma 54, 1989
\par >
\par > K. Schmidt: Parameterized reachability trees of algebraic Petri nets.
\par > 16th ICATPN, Springer 1995.
\par
\par It is nice to have as many analysis methods as possible, but this is no reason to vote against the standard
, which is concerned with providing an unambiguous specification language with an agreed semantics. I suspect that these analysis techniques can also be used to prove properties about a scheme, which would then provide results for a concrete version, that
is described by an HLPNG, with a particular algebra - so I dont think anything is lost here.
\par >
\par > 3. In a more syntactical version, HLPNG would better fit to the concept
\par > of Algebraic Net Schemes proposed by W. Reisig! Then, Algebraic Net
\par > Schemes are just HLPNG without a fixed algebra.
\par
\par It is certainly possible to have a more syntactic form, that does not include the algebra, for the purpose of defining schemes. What I am proposing here is that both forms are included, as we need both. This was
indicated in an editor's note in the CD. In my response to DIN in the draft disposition, I indicated that we could include both.
\par I am not sure what DIN's position is with respect to having both the scheme and a concrete definition. Is DIN happy with this?
\par >
\par >I miss to see the editors point that the HLPNG should be concrete (see reply
\par >to DIN1). Would a syntax for -- let's say -- PASCAL be more concrete if the
\par >part about the syntactical representation of real numbers would be left
\par >semantical? I would rather say, that this syntax would be incomplete.
\par >Maybe, having the standard syntax for natural numbers as inscription for
\par >markings of sort Nat is nicer than some awkward representation by a term
\par >succ(succ(zero)). Though this works nice for natural numbers (and some
\par >standard data types), this does not work if there is no common understanding
\par >(pragmatic) of the data type. The current version of HLPNG allows any type
\par >-- it might not have any `common sense syntax' (e.g. Agents when modelling
\par >distributed algorithms). Therefore, HLPNG must provide a syntax for these.
\par >A more convenient syntax for standard data types could be easily introduced
\par >by conventions.
\par
\par See comment under 1. above. We need
concrete markings, and to run the net at the concrete level - as this is what is meaningful for industrial applications. Moving terms around the net is not easy to relate to the physical world - as I have indicated to you in a previous email.
\par >
\par >In II.2 there will be a proposal how to give a purely syntactical definition
\par >of HLPNG; note that there will be the notion of a `symbolic marking' which is
\par >the syntactical representation in HLPNG and there will be a notion of a
\par >`marking' which is its semantical counterpart. Everybody is free to use only
\par >semantical markings -- if he wants to. But, there should also be a
\par >concept of
\par >HLPNG for symbolic markings (cf. 2.).
\par >
\par OK - it seems that you are accepting that there should be both. Am I right? - see under 3 above.
\par
\par >
\par >
\par >II. Proposed changes
\par >--------------------
\par >
\par >In this section, we propose a change of the definition of HLPNG which
\par >is purely syntactical and allows some more `flexibility' in building
\par >BTERMS. Both aspects are independent of each other.
\par
\par Given that we have concrete items for places, transitions and arcs, we are going to have a mixture of syntactic and semantic anyway. So I guess it is not purely syntactic, but certainly more syntactic, and suitable for describing schemes - which is fine.
\par >
\par >II.1. Syntactical representation of HLPNG
\par >-----------------------------------------
\par >
\par >This changes are basically the same as proposed in DIN25 and DIN26. The
\par >function Type is changed to associate a sort of the signature to each place
\par >(rather than a type). The initial marking is replaced by a symbolic
\par >initial marking. Moreover, there is a concept of marking and of initial
\par >marking of a HLPNG.
\par within in the same definition? - hence a mix?
\par >
\par >Clause 7.2:
\par > Replace: Type: P --> S_H
\par > By: Type: P --> S
\par >
\par Not sure that this is what you want - see below - and agree that in the scheme this function should be Sort rather than Type.
\par > Replace first sentence on page 19 (arc annotations)
\par > By: - A : F --> BTERM(O \\cup V) such that for all (p,t), (t',p) \\in F,
\par > A(p,t), A(t',p) \\in BTERM(O \\cup V)_\{Type(p)\}.
\par
\par This is too restrictive, as we need to allow for subtypes and multisets in the concrete version. (Ie there may be several sorts that would be compatible, not just Type(p).) The current
definition attempted to deal with this by allowing any sort s, that mapped to a carrier H_s = Type(p), to be the sort of BTERM. But this is also restrictive. I now think that what is required is to replace the def of A with
\par
\par - A : F --> BTERM(O \\cup V) such that for all (p,t), (t',p) \\in F,
\par for all bindings \\alpha, Val_\\alpha(A(p,t)), Val_\\alpha(A(t',p)) \\in \\mu Type(p)
\par
\par in the current definition.
\par That is, so long as the annotation on an arc evaluates to a multiset over the associated place's type, then it is allowed. (This is what is required by the enabling condition and the transition rule.)
\par
\par >
\par > Replace last item of the definition of HLPNG (marking)
\par > By: * M : P --> BTERM(O) such that for each p \\in P:
\par > M(p) \\in BTERM(O)_\{Type(p)\}, is the symbolic initial marking.
\par >
\par > Replace in the text following the items: `A typing function associates ...'
\par > (up to the end of this paragraph).
\par > By: The typing function associates a sort of the signature with each
\par >place.
\par > A place is inscribed by a BTERM representing the initial marking
\par > (see Clause 7.3) of this place.
\par >
\par >Note that, capital M will be used for symbolic markings; m will be used for
\par >markings. Maybe, the function Type should now be named Sort.
\par (Yes agreed Type --> Sort)
\par
\par >
\par >Clause 7.3 (completely new text):
\par > A marking, m, of the HLPNG is defined by
\par > m: P --> \\bigcup_\{p \\in P\}\\mu H_\{Type(p)\}such that
\par > m(p) \\in \\mu H_\{Type(p)\}. The initial marking of the
\par > HLPNG is defined by: m_0(p) = eval(M(p)).
\par
\par This, and the above changes, seem to suggest that the algebra, H, is maintained in the definition. Wouldn't it be cleaner to have schemes defined without the algebra (as it plays no part), and then have a concrete version that does include H?
\par >
\par >Ed. Note: eval is the evaluation function which can be defined by
\par >eval = Val_\{\\alpha\}where \\alpha is the unique assignment:
\par >\\alpha: \\emptyset --> H. This must be added in Appendix A.3.6
\par >(see II.2 and below).
\par >Moreover, a convention of syntactical representations of constants of
\par >standard sorts (Nat, Bool, etc.) could be introduced.
\par
\par What did you have in mind?
\par
\par >
\par >If the above changes are accepted, the following clauses
\par >need to be adapted in order to conform with the changes:
\par > - Throughout: M and M' must be replaced by m and m'
\par I would not recommend this. Much prefer that it is the syntactic version that has lower case, and the concrete version upper case - as at present.
\par
\par > - Glossary (Clause 3.1):
\par > + Symbolic initial marking must be added
\par > + Place Type must be replaced by Place sort
\par > - Clause 6.2 Place Types must be also replaced by Place Sorts and
\par > Place Marking must be replaced by Symbolic Initial Marking
\par > - Clause 6.3 The concept of marking must be added.
\par > - Clause 8.5 Can be omitted
\par > - Clause 9 (3rd item last paragraph) `D = ...' must be replaced by
\par > D = \{H_\{Type(p) | p \\in P\}\\cup \{Type(t) | t \\in T \}.
\par > - Clause A.3.6: At the end, the special case of an evaluation eval
\par > must be defined (see above and II.2).
\par > - Clause B.1: Replace Type: P --> \{dot\}by Type: P --> Dot and
\par > replace M_0: P --> Dot by M: P --> BTERM(O)
\par >
\par Probably not necessary, given that the concrete form is maintained. Possibly one could add a para in clause 6 on the scheme.
\par >
\par >II.2. Customizable operations for BTERMS
\par >----------------------------------------
\par >
\par >As it stands, BTERMS can be inductively build from TERMs (Clause A.3.4) by:
\par >i'a, i x b, and b1 + b2 (where i is a term over Nat and b, b1, b2 are
\par >BTERMS of appropriate sort). In DIN2 we argued that this is restrictive.
\par >For example, there is no BTERM with one variable i (over Nat) which gives
\par >us the multiset [1 , 2 , ... , i ] for each chosen value i, i.e. for each
\par >i each number up to i occurs exactly once in the multiset. (at least, I
\par >fail to see that this is possible; the problem is that the user is free
\par >to define operations on the TERM-level but NOT on the BTERM-level according
\par >to the current version of the standard).
\par I think we can do without BTERMs all together, and just use appropriate operators in the signature to define whatever we like. This was the comment made in the draft disposition.
\par >
\par >In order to allow more flexibility for defining own BTERM-constructs, there
\par >was an outline of a definition of BTERMS in the Appendix of the DIN vote.
\par >Here, we give a full definition which basically replaces A.3. In this
\par >proposal, we subsume proposal DIN36 (separation of variables from signatures)
\par >for a more convenient presentation -- but the proposal works without that.
\par >For arguments in favour of the separation of Variables from Signatures
\par >see III, DIN36.
\par >
\par > A.3.1 Multiset Signatures
\par >
\par > A many-sorted multiset signature BSIG = (S,O) comprises
\par >
\par > * a set S of sorts (sort symbols)
\par > for each sort s \\in S we define a unique sort b(s) representing
\par > the corresponding multiset sort over s; we define
\par > B(S) = S \\cup \{b(s) | s \\in S \}
\par
\par This is providing a restriction of the signature, which isn't warranted for the concrete definition, although it may be useful at the level of schemes.
\par >
\par > * a set O of operations (operation symbols); each operation o \\in O
\par > is associated with an arity B(S)^+, where B(S)^+ denotes the non-empty
\par > sequences over B(S). Technically, O = (O_a)_\{a \\in B(S)^+\}is an
\par > B(S)^+ indexed set.
\par >
\par > NOTE: o \\in O_z with z \\in B(S) is called a constant of BSIG.
\par >
\par >
\par > A.3.2 Variables for a Multiset Signature
\par >
\par > For a multiset signature BSIG = (S,O) a B(S)-indexed set
\par > V = (V_z)_\{z \\in B(S)\}disjoint from O is a variable set of BSIG.
\par >
\par >
\par > A.3.3 Terms
\par >
\par > Let V be a variable set for BSIG = (S,O). The BSIG-Terms over V, denote by
\par > TERM(BSIG,V)_z, are inductively defined by:
\par >
\par > * for z \\in B(S) and o \\in O_z: o \\in TERM(BSIG,V)_z
\par >
\par > * for z \\in B(S) and v \\in V_z: v \\in TERM(BSIG,V)_z
\par >
\par > * for z_1...z_n z_\{n+1\}\\in B(S) and o \\in O_\{z_1...z_\{n+1\}\}and
\par > e_i \\in TERM(BSIG,V)_\{z_i\}for i=1, ..., n:
\par > o(e_1, ..., e_n) \\in TERM(BSIG,V)_\{z_\{n+1\}\}
\par >
\par > A.3.4 Algebras
\par >
\par > For a multiset signature BSIG = (S,O), a BSIG-Algebra H = (A,F) comprises
\par (careful with A and F - as they are already used in the definition - arc annotation
\par and flow relation - other symbols required)
\par >
\par > * an indexed set A = (A_z)_\{z \\in B(S)\}of non-empty sets such that for
\par > each s \\in S we have A_\{b(s)\}= \\mu A_s, i.e. each domain of a
\par > multiset sort b(s) is really a multiset over the domain
\par >corresponding to
\par > sort s.
\par >
\par > * an indexed set of functions F = (f_o)_\{o \\in O\}where
\par > f_o: A_\{z_1\}x ... x A_\{z_n\}\\rightarrow A_\{z_\{n+1\}\}for
\par > o \\in O_\{z_1...z_\{n+1\}\}.
\par >
\par > Convention: We assume that each sorted multiset signature BSIG = (S,O) has
\par > the sorts Nat and Bool and for each sort s \\in S there are the following
\par > operations:
\par > .'. : Nat s --> b(s)
\par > .x. : Nat b(s) --> b(s)
\par > .+. : b(s) b(s) --> b(s)
\par >
\par > For each algebra, we assume that Nat and Bool correspond to the set of
\par > natural numbers N and the set Boolean, resp. Moreover, the functions
\par > corresponding to the operations .'. , .x., and .+. have the usual meaning.
\par >
\par >Ed. Note: This could be defined more formally.
\par
\par OK - all this is very nice, as it shows how the appropriate operators can be defined to obtain the syntax that is wanted for arc expressions when multiset descriptions are required on arcs - but they are not required all the time. Hence, all we need to do
is to annotate arcs with terms. If we need the machinery above, then this has nicely illustrated how it can be done. It may be appropriate to include this in the tutorial, but it is not required for the standard. Thus we dispense with BTERMs, (just have
a Sig rather than a BSIG) and annotate arcs by
\par
\par - A : F --> TERM(O \\cup V) such that for all (p,t), (t',p) \\in F,
\par for all bindings \\alpha, Val_\\alpha(A(p,t)), Val_\\alpha(A(t',p)) \\in \\mu Type(p)
\par
\par This is then more elegant than the previous definition.
\par >
\par > A.3.5 Assignment and Evaluation
\par >
\par > For a multiset signature BSIG = (S,O), some variable set V for BSIG and
\par > a BSIG-Algebra H = (A, F) an assignment is a mapping
\par > \\alpha: V --> A such that \\alpha(v) \\in A_z for v \\in V_z.
\par >
\par > An assignment \\alpha can be extended to terms
\par > Val_\{\\alpha\}: TERM(BSIG,V) --> A by the following inductive definition:
\par >
\par > * for o \\in O_z: Val_\{\\alpha\}(o) = f_\{o\}
\par >
\par > * for v \\in V_z: Val_\{\\alpha\}(v) = \\alpha(v)
\par >
\par > * for z_1...z_n z_\{n+1\}\\in B(S) and o \\in O_\{z_1...z_n\}and
\par > e_i \\in TERM(BSIG,V)_\{z_i\}for i=1, ..., n:
\par > Val_\{\\alpha\}(o(e_1, ..., e_n)) =
\par > f_o(Val_\{\\alpha\}(e_1),...,Val_\{\\alpha\}(e_n)).
\par >
\par > Val_\{\\alpha\}is called the evaluation function corresponding to \\alpha
\par >
\par > For the empty set of variables, there is a unique assignment
\par > \\alpha : \\emptyset --> A. The evaluation Val_\{\\alpha\}corresponding to
\par > this unique assignment is simply called evaluation and denoted by eval.
\par >
\par >This finishes the changes (resp. the new text) in the Appendix (A.3). Now,
\par >BTERMS(O \\cup V)_s can be consistently replaced by TERM(BSIG,V)_\{b(s)\}
\par >throughout the current text of the standard.
\par
\par OK - so at the syntactic level, terms of TERM(BSIG,V)_\{b(s)\}a
nnotate arcs, and hence will be appropriately evaluated as multisets. This leaves the problem of 'subsorts'. We may want a mixture of terms of different sorts, that may still evaluate to a multiset over the place type. eg consider a place p of sort Nat, a
nd two more sorts int4 and int5, that map to two carriers \{1,2,3,4\}, and \{1,2,3,4,5\}
, and variables associated with all these sorts. We may want to write x_Nat + x_int4 + x_int5 on the arc, and evaluate it as a multiset over the naturals. As I understand it
, your BSIG does not allow this. However, it is no problem in the concrete version, as this term would be allowed, because it evaluates correctly.
\par
\par (Note that in the evaluation of such a term, each of the variables must be evaluated as a 'singleton' multiset - by convention, and this needs to be included in the definitions. ie
\par because of history, we would like to be able to write x on an arc, rather than 1'x on the arc (where x:Type(p)), but interpret it as 1'x. That is: if we evaluate an arc expression an
d find that we return an element of Type(p), then we assume that it should be converted to a singleton multiset over Type(p).)
\par
\par >Now, the user is free to define own operations on the multiset level.
\par >
\par >
\par Always has been, as you have nicely illustrated, which allows us to eliminate BTERMs (from the concrete definition).
\par
\par >III. Further Comments
\par >---------------------
\par >
\par >In this part, we reply on the individual comments in the Draft
\par >Disposition Report in the order mentioned.
\par >
\par >
\par >AUS01--AUS08 okay
\par >
\par >DAN1--DAN3 okay
\par >
\par >DIN1: see above I and II.1
\par OK - see comments above
\par >
\par >DIN2: see above II.2
\par See Editor's comment in draft disposition, and the above comments.
\par >
\par >DIN3--DIN4: okay
\par >
\par >DIN5, DIN13, DIN15, DIN20, DIN22:
\par > Here, some words of explanation are due:
\par >
\par > Substitution is an operation on terms. In given term, some variables
\par > are replaced by a term of appropriate sort. The result of
\par > a substitution is a term again. In particular, substitution
\par > returns a syntactical object (a term).
\par >
\par Understood (see draft disposition)
\par > An evaluation of a term returns the value of the term in a given state
\par > or under a given assignment. The result is semantical (a value of the
\par > corresponding algebra). A formal definition for evaluations in our
\par > context was given in II.2 (A.3.5) above.
\par
\par Understood
\par >
\par > I have had a look in different text books on computer science; and
\par > this terminology seems to be standard.
\par >
\par Which ones? I guess there is a general understanding of substitution of values for variables used in the anglo-saxon world, so there may be some cultural differnces here.
\par
\par > In the current version of the high-level standard, there seems to be
\par > no need for the concept of substitutions at all. There
\par > is no need to define an evaluation via a substitution and reduction to
\par > a simplest form. Rather, the use of this concepts induces problems:
\par > * What is the simplest form? It is know that in general simplest
\par > forms (normal forms) do not exist (e.g. we cannot say whether
\par > 1'a + 1'b is simpler than 1'b + 1'a).
\par
\par OK - perhaps this is a bit loose - but you know what I mean from the example in the disposition of DIN 13. Perhaps one should say something like - 'gather like terms together' in 3.1.24.2, as this operation certainly occurs. Do you have some better words?
\par >
\par > * What is reduction?
\par >
\par > * Reduction according to which rules?
\par >
\par > If we use the concept of evaluations only, there is no problem.
\par >
\par
\par >DIN6--DIN7: okay
\par >
\par >DIN8: In algebraic specifications (without polymorphism), it is always taken
\par > care that a SIG-Algebra has as many domains as there are sorts in
\par > the signature.
\par Why do we need to here?
\par
\par >Of course, it may happen that two different sorts are
\par > associated with the same mathematical domain e.g. Nat as well as Agents
\par > are associated with the natural number. If the domains are considered
\par > to be a set of sets, this set will have less sets than sorts (because
\par > two sets are identical).
\par >
\par Yes - I dont see any problem. What is the problem?
\par > In order to cope with this problems there are two possibilities:
\par > * The domains are presented as a list of sets (where multiple
\par >occurrence
\par > is allowed); this approach is often taken in books on algebras.
\par > * In the context of algebraic specifications, the domains are
\par >presented
\par > as a family of sets (or as S-indexed set).
\par >
\par > The main point was, that the concept of algebras as used in the
\par > standard nicely fits to the literature and other standards in the field
\par > of algebraic specifications and mathematical logic.
\par
\par We should use economy of definition where we can. Currently I dont see the need for a more
complex definition - just following books for their sake I dont see as a virtue - but I have probably missed something here - please let me know what the technical problem is.
\par >
\par >DIN9--DIN12: okay
\par >
\par >DIN13: see DIN5
\par >
\par >DIN14: okay
\par >
\par >DIN15: see DIN5
\par >
\par >DIN16--DIN17: okay
\par >
\par >DIN18: The standard should be as unambiguous as possible. I do agree that
\par > there is no ambiguity due to the conventions. But some people might
\par > read an expression M - P + P' as M - (P + P'); the reason is that P
\par > and P' are similar to each other and different quite from M, such that
\par > the usual conventions are overruled in their minds. Therefore,
\par > additional parentheses would be helpful (and do no harm):
\par >
\par > M' = (M - Pre(...) ) + Post(...)
\par >
\par Would M' = M + Post() - Pre()
\par be acceptable - it doesn't require parenthesis, which add to clutter.
\par >DIN19: okay
\par >
\par >DIN20: see DIN5
\par >
\par >DIN21: okay
\par >DIN22: see DIN5
\par >
\par >DIN23--DIN24:
\par >
\par >DIN25, DIN26: see DIN1
\par >
\par >DIN27--DIN28: okay
\par >
\par >DIN29: see DIN18
\par >
\par >DIN30: see DIN1
\par >
\par >DIN31--DIN35: okay
\par >
\par >DIN36: Similar to DIN8, the separation of variables from signatures is
\par > common sense in algebraic specifications. The reason is that
\par > the same signature is often used with different variables--and the
\par > whole machinery (SIG-morphism and algebra-morphisms etc.) works
\par > without variables.
\par >
\par > But even in algebraic high-level nets, this separation is adopted.
\par > For example K. Schmidt (see I.) uses one signature for the net, but
\par > the variables are locally defined for each transition.
\par >
\par > Maybe, this is a matter of taste. But why not using the concepts
\par > in the same way as in the field of algebraic specifications?
\par Thanks for the example above (II.2). I shall look into this one.
\par >
\par >DIN37--DIN39: okay
\par >
\par >DIN40: The statement that the domains for sorts Nat and Bool should
\par >correspond
\par > to N and Boolean in the algebra is there, indeed. But it is in the
\par > syntactical part, where algebras do not occur. The appropriate place
\par > would be in A.3.5.
\par It seems quite natural to me where it is - perhaps there should be a forward reference to A.3.5. What do others think? However, this needs to be revised in the light of just using terms rather than BTERMs. It see
ms that only a Boolean Signature is required.
\par
\par >DIN41-DIN44: okay
\par >
\par >JPN001--JPN0014: okay
\par >
\par >UK1E--UK11: okay
\par >
\par >USA1--USA4: okay}{\fs20
\par }}