Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Some Elementary Notions of the Theory of Petri Nets

**by****Waldemar Korczynski**- Received August 10, 1990
- MML identifier: NET_1

- [ Mizar article, MML identifier index ]

environ vocabulary RELAT_1, BOOLE, TARSKI, NET_1, SETFAM_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1; constructors REAL_1, SETFAM_1, XBOOLE_0; clusters RELAT_1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin definition struct Net (# Places, Transitions -> set, Flow -> Relation #); end; ::The above definition describes a "structure of a Petri net" which ::is a kind of relational system. reserve x,y for set; reserve N for Net; definition let N be Net; attr N is Petri means :: NET_1:def 1 the Places of N misses the Transitions of N & (the Flow of N) c= [:the Places of N, the Transitions of N:] \/ [:the Transitions of N, the Places of N:]; synonym N is_Petri_net; end; :: A Petri net is defined as a triple of the form :: N = (Places, Transitions, Flow) :: with Places and Transitions being disjoint sets and :: Flow c= (Transitions x Places) U (Places x Transitions) :: It is allowed that both sets Places and Transitions are empty. :: A Petri net is here described as a predicate defined in the set :: (on the mode) Net. definition let N be Net; func Elements(N) equals :: NET_1:def 2 (the Places of N) \/ (the Transitions of N); end; :: The set Elements(N) of so called "elements of a Petri net is defined :: as the union of its Places and Transitions. Here a function assigning :: to a Petri net such a set is defined. canceled 3; theorem :: NET_1:4 (the Places of N) c= Elements(N); theorem :: NET_1:5 (the Transitions of N) c= Elements(N); :: The above definition describes the set of elements of a Petri net :: as a (parametrized) TYPE ("mode" in Mizar) which is sometimes :: "technically" (because of the Mizar -writing technology) more :: convenient. theorem :: NET_1:6 x in Elements(N) iff x in the Places of N or x in the Transitions of N; theorem :: NET_1:7 Elements(N) <> {} implies (x is Element of Elements(N) implies x is Element of the Places of N or x is Element of the Transitions of N); theorem :: NET_1:8 x is Element of the Places of N & the Places of N <> {} implies x is Element of Elements(N); theorem :: NET_1:9 x is Element of the Transitions of N & the Transitions of N <> {} implies x is Element of Elements(N); definition cluster Net (#{}, {}, {}#) -> Petri; end; :: This lemma is of rather "technical" nature. It allows a definition :: of a "subtype" of the type Net. (see the following definition of the :: type Pnet). definition cluster strict Petri Net; end; definition mode Pnet is Petri Net; end; :: The above definition defines a Petri net as a TYPE of the structure :: Net. The type is not empty. canceled; theorem :: NET_1:11 for N being Pnet holds not (x in the Places of N & x in the Transitions of N); :: This lemma is of rather "technical" character. It will be used in the :: proof of the correctness of a definition of a function bellow. (See :: the definition of the functions Enter and Exit.) theorem :: NET_1:12 for N being Pnet holds ([x,y] in the Flow of N & x in the Transitions of N) implies y in the Places of N; theorem :: NET_1:13 for N being Pnet holds ([x,y] in the Flow of N & y in the Transitions of N) implies x in the Places of N; theorem :: NET_1:14 for N being Pnet holds ([x,y] in the Flow of N & x in the Places of N) implies y in the Transitions of N; theorem :: NET_1:15 for N being Pnet holds ([x,y] in the Flow of N & y in the Places of N) implies x in the Transitions of N; definition let N be Pnet; let x,y; canceled 2; pred pre N,x,y means :: NET_1:def 5 [y,x] in the Flow of N & x in the Transitions of N; pred post N,x,y means :: NET_1:def 6 [x,y] in the Flow of N & x in the Transitions of N; end; definition let N be Net; let x be Element of Elements(N); func Pre(N,x) means :: NET_1:def 7 y in it iff y in Elements(N) & [y,x] in the Flow of N; func Post(N,x) means :: NET_1:def 8 y in it iff y in Elements(N) & [x,y] in the Flow of N; end; theorem :: NET_1:16 for N being Pnet for x being Element of Elements(N) holds Pre(N,x) c= Elements(N); theorem :: NET_1:17 for N being Pnet for x being Element of Elements N holds Pre(N,x) c= Elements N; theorem :: NET_1:18 for N being Pnet for x being Element of Elements(N) holds Post(N,x) c= Elements(N); theorem :: NET_1:19 for N being Pnet for x being Element of Elements N holds Post(N,x) c= Elements N; theorem :: NET_1:20 for N being Pnet for y being Element of Elements(N) holds y in the Transitions of N implies (x in Pre(N,y) iff pre N,y,x); theorem :: NET_1:21 for N being Pnet for y being Element of Elements(N) holds y in the Transitions of N implies (x in Post(N,y) iff post N,y,x); definition let N be Pnet; let x be Element of Elements(N); assume Elements(N) <> {}; func enter(N,x) means :: NET_1:def 9 (x in the Places of N implies it = {x}) & (x in the Transitions of N implies it = Pre(N,x)); end; theorem :: NET_1:22 for N being Pnet for x being Element of Elements(N) holds Elements(N) <> {} implies enter(N,x) ={x} or enter(N,x) = Pre(N,x); theorem :: NET_1:23 for N being Pnet for x being Element of Elements(N) holds Elements(N) <> {} implies enter(N,x) c= Elements(N); theorem :: NET_1:24 for N being Pnet for x being Element of Elements N holds Elements N <> {} implies enter(N,x) c= Elements N; definition let N be Pnet; let x be Element of Elements(N); assume Elements(N) <> {}; func exit(N,x) -> set means :: NET_1:def 10 (x in the Places of N implies it = {x}) & (x in the Transitions of N implies it = Post(N,x)); end; theorem :: NET_1:25 for N being Pnet for x being Element of Elements(N) holds Elements(N) <> {} implies exit(N,x) ={x} or exit(N,x) = Post(N,x); theorem :: NET_1:26 for N being Pnet for x being Element of Elements(N) holds Elements(N) <> {} implies exit(N,x) c= Elements(N); theorem :: NET_1:27 for N being Pnet for x being Element of Elements N holds Elements N <> {} implies exit(N,x) c= Elements N; definition let N be Pnet; let x be Element of Elements(N); func field(N,x) equals :: NET_1:def 11 enter(N,x) \/ exit(N,x); end; definition let N be Net; let x be Element of the Transitions of N; func Prec(N,x) means :: NET_1:def 12 y in it iff y in the Places of N & [y,x] in the Flow of N; func Postc(N,x) means :: NET_1:def 13 y in it iff y in the Places of N & [x,y] in the Flow of N; end; definition let N be Pnet; let X be set; func Entr(N,X) means :: NET_1:def 14 x in it iff x c= Elements N & ex y being Element of Elements N st y in X & x = enter(N,y); func Ext(N,X) means :: NET_1:def 15 x in it iff x c= Elements N & ex y being Element of Elements N st y in X & x = exit(N,y); end; theorem :: NET_1:28 for N being Pnet for x being Element of Elements(N) for X being set holds Elements(N) <> {} & X c= Elements(N) & x in X implies enter(N,x) in Entr(N,X); theorem :: NET_1:29 for N being Pnet for x being Element of Elements(N) for X being set holds Elements(N) <> {} & X c= Elements(N) & x in X implies exit(N,x) in Ext(N,X); definition let N be Pnet; let X be set; func Input(N,X) equals :: NET_1:def 16 union Entr(N,X); func Output(N,X) equals :: NET_1:def 17 union Ext(N,X); end; theorem :: NET_1:30 for N being Pnet for x for X being set holds Elements(N) <> {} & X c= Elements(N) implies (x in Input(N,X) iff ex y being Element of Elements(N) st y in X & x in enter(N,y)); theorem :: NET_1:31 for N being Pnet for x for X being set holds Elements(N) <> {} & X c= Elements(N) implies (x in Output(N,X) iff ex y being Element of Elements(N) st y in X & x in exit(N,y)); theorem :: NET_1:32 for N being Pnet for X being Subset of Elements(N) for x being Element of Elements(N) holds Elements(N) <> {} implies (x in Input(N,X) iff (x in X & x in the Places of N or ex y being Element of Elements(N) st y in X & y in the Transitions of N & pre N,y,x)); theorem :: NET_1:33 for N being Pnet for X being Subset of Elements(N) for x being Element of Elements(N) holds Elements(N) <> {} implies (x in Output(N,X) iff (x in X & x in the Places of N or ex y being Element of Elements(N) st y in X & y in the Transitions of N & post N,y,x));

Back to top