:: Some Elementary Notions of the Theory of Petri Nets
:: by Waldemar Korczy\'nski
::
:: Received August 10, 1990
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, SETFAM_1, NET_1,
STRUCT_0, PETRI;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, PARTIT_2,
STRUCT_0, PETRI;
constructors TARSKI, SUBSET_1, RELAT_1, STRUCT_0, PETRI, PARTIT_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1;
requirements SUBSET, BOOLE;
begin
definition let P be PT_net_Str;
func Flow P -> set equals
:: NET_1:def 1
(the S-T_Arcs of P) \/ the T-S_Arcs of P;
end;
registration let P be PT_net_Str;
cluster Flow P -> Relation-like;
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 PT_net_Str;
definition
let N be PT_net_Str;
attr N is Petri means
:: NET_1:def 2
the carrier of N misses the carrier' of N & (
Flow N) c= [:the carrier of N, the carrier' of N:] \/ [:the
carrier' of N, the carrier of N:];
end;
:: A Petri net is defined as a triple of the form
:: N = (carrier, carrier', Flow)
:: with carrier and carrier' being disjoint sets and
:: Flow c= (carrier' x carrier) U (carrier x carrier')
:: It is allowed that both sets carrier and carrier' are empty.
:: A Petri net is here described as a predicate defined in the set
:: (on the mode) PT_net_Str.
definition
let N be PT_net_Str;
func Elements(N) -> set equals
:: NET_1:def 3
(the carrier of N) \/ (the carrier' of N);
end;
theorem :: NET_1:1
Elements(N) <> {} implies (x is Element of Elements(N) implies x is
Element of the carrier of N or x is Element of the carrier' of N);
theorem :: NET_1:2
x is Element of the carrier of N & the carrier of N <> {} implies x is
Element of Elements(N);
theorem :: NET_1:3
x is Element of the carrier' of N & the carrier' of N <> {}
implies x is Element of Elements(N);
registration
cluster PT_net_Str (#{}, {}, {}({},{}), {}({},{})#) -> Petri;
end;
:: This lemma is of rather "technical" nature. It allows a definition
:: of a "subtype" of the type PT_net_Str. (see the following definition of the
:: type Pnet).
registration
cluster strict Petri for PT_net_Str;
end;
definition
mode Pnet is Petri PT_net_Str;
end;
:: The above definition defines a Petri net as a TYPE of the structure
:: PT_net_Str. The type is not empty.
theorem :: NET_1:4
for N being Pnet holds not (x in the carrier of N & x in the carrier' 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:5
for N being Pnet holds [x,y] in Flow N & x in the
carrier' of N implies y in the carrier of N;
theorem :: NET_1:6
for N being Pnet holds [x,y] in Flow N & y in the
carrier' of N implies x in the carrier of N;
theorem :: NET_1:7
for N being Pnet holds [x,y] in Flow N & x in the carrier of N
implies y in the carrier' of N;
theorem :: NET_1:8
for N being Pnet holds [x,y] in Flow N & y in the carrier of N
implies x in the carrier' of N;
definition
let N be Pnet;
let x,y;
pred pre N,x,y means
:: NET_1:def 4
[y,x] in Flow N & x in the carrier' of N;
pred post N,x,y means
:: NET_1:def 5
[x,y] in Flow N & x in the carrier' of N;
end;
definition
let N be PT_net_Str;
let x be Element of Elements(N);
func Pre(N,x) -> set means
:: NET_1:def 6
for y being object holds y in it iff y in Elements(N) & [y,x] in Flow N;
func Post(N,x) -> set means
:: NET_1:def 7
for y being object holds y in it iff y in Elements(N) & [x,y] in Flow N;
end;
theorem :: NET_1:9
for N being Pnet for x being Element of Elements(N) holds Pre(N,
x) c= Elements(N);
theorem :: NET_1:10
for N being Pnet for x being Element of Elements N holds Pre(N,x) c=
Elements N;
theorem :: NET_1:11
for N being Pnet for x being Element of Elements(N) holds Post(N
,x) c= Elements(N);
theorem :: NET_1:12
for N being Pnet for x being Element of Elements N holds Post(N,x) c=
Elements N;
theorem :: NET_1:13
for N being Pnet for y being Element of Elements(N) holds y in the
carrier' of N implies (x in Pre(N,y) iff pre N,y,x);
theorem :: NET_1:14
for N being Pnet for y being Element of Elements(N) holds y in the
carrier' 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) -> set means
:: NET_1:def 8
(x in the carrier of N implies it = {x}) & (x in
the carrier' of N implies it = Pre(N,x));
end;
theorem :: NET_1:15
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:16
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies enter(N,x) c= Elements(N);
theorem :: NET_1:17
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 9
(x in the carrier of N implies it = {x})
& (x in the carrier' of N implies it = Post(N,x));
end;
theorem :: NET_1:18
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:19
for N being Pnet for x being Element of Elements(N) holds
Elements(N) <> {} implies exit(N,x) c= Elements(N);
theorem :: NET_1:20
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) -> set equals
:: NET_1:def 10
enter(N,x) \/ exit(N,x);
end;
definition
let N be PT_net_Str;
let x be Element of the carrier' of N;
func Prec(N,x) -> set means
:: NET_1:def 11
for y being object holds
y in it iff y in the carrier of N & [y,x] in Flow N;
func Postc(N,x) -> set means
:: NET_1:def 12
for y being object holds
y in it iff y in the carrier of N & [x,y] in Flow N;
end;
definition
let N be Pnet;
let X be set;
func Entr(N,X) -> set means
:: NET_1:def 13
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) -> set 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 = exit(N,y);
end;
theorem :: NET_1:21
for N being Pnet for x being Element of Elements(N) for X being
set holds Elements(N) <> {} & x in X implies enter(N,x) in Entr(N,X);
theorem :: NET_1:22
for N being Pnet for x being Element of Elements(N) for X being
set holds 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) -> set equals
:: NET_1:def 15
union Entr(N,X);
func Output(N,X) -> set equals
:: NET_1:def 16
union Ext(N,X);
end;
theorem :: NET_1:23
for N being Pnet for x for X being set holds 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:24
for N being Pnet for x for X being set holds 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:25
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 carrier of N or ex y being Element of Elements(N) st y in X & y in the
carrier' of N & pre N,y,x));
theorem :: NET_1:26
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 carrier of N or ex y being Element of Elements(N) st y in X & y in the
carrier' of N & post N,y,x));