:: Basic Petri Net Concepts.
:: Place/Transition Net Structure, Deadlocks, Traps, Dual Nets
:: by Pauline N. Kawamoto, Yasushi Fuwa and Yatsuka Nakamura
::
:: Received November 27, 1992
:: Copyright (c) 1992-2026 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 XBOOLE_0, RELAT_1, SUBSET_1, ZFMISC_1, MCART_1, ARYTM_3, TARSKI,
PETRI, STRUCT_0, PNPROC_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, RELSET_1,
MCART_1, DOMAIN_1, PARTIT_2, STRUCT_0;
constructors RELSET_1, DOMAIN_1, STRUCT_0, PARTIT_2, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
expansions XBOOLE_0;
theorems SUBSET_1, MCART_1, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0;
schemes DOMAIN_1;
begin
:: Redefinition of Element for Non-empty Relation
definition
let A, B be non empty set;
let r be non empty Relation of A, B;
redefine mode Element of r -> Element of [:A,B:]; :: redefines Element (SUBSET_1, definition)
coherence
proof
let a be Element of r;
thus thesis;
end;
end;
:: Place/Transition Net Structure
definition
struct(2-sorted) PT_net_Str (# carrier, carrier' -> set,
S-T_Arcs -> Relation of the carrier, the carrier',
T-S_Arcs -> Relation of the carrier', the carrier #);
end;
definition let N be PT_net_Str;
attr N is with_S-T_arc means
:Def1: the S-T_Arcs of N is non empty;
attr N is with_T-S_arc means
:Def2: the T-S_Arcs of N is non empty;
end;
definition
func TrivialPetriNet -> PT_net_Str equals
PT_net_Str (# {{}}, {{}}, [#]({{}},{{}}), [#]({{}},{{}}) #);
coherence;
end;
registration
cluster TrivialPetriNet ->
with_S-T_arc with_T-S_arc strict non empty non void;
coherence;
end;
registration
cluster non empty non void with_S-T_arc with_T-S_arc strict for PT_net_Str;
existence
proof
take TrivialPetriNet;
thus thesis;
end;
end;
registration let N be with_S-T_arc PT_net_Str;
cluster the S-T_Arcs of N -> non empty;
coherence by Def1;
end;
registration let N be with_T-S_arc PT_net_Str;
cluster the T-S_Arcs of N -> non empty;
coherence by Def2;
end;
definition
mode Petri_net
is non empty non void with_S-T_arc with_T-S_arc PT_net_Str;
end;
reserve PTN for Petri_net;
:: Place, Transition, and Arc (s->t, t->s) Elements
definition
let PTN;
mode place of PTN is Element of the carrier of PTN;
mode places of PTN is Element of the carrier of PTN;
mode transition of PTN is Element of the carrier' of PTN;
mode transitions of PTN is Element of the carrier' of PTN;
mode S-T_arc of PTN is Element of the S-T_Arcs of PTN;
mode T-S_arc of PTN is Element of the T-S_Arcs of PTN;
end;
:: Redefinition of Relation for s->t Arcs
definition
let PTN;
let x be S-T_arc of PTN;
redefine func x`1 -> place of PTN; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
thus x`1 is place of PTN;
end;
redefine func x`2 -> transition of PTN; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
thus x`2 is transition of PTN;
end;
end;
:: Redefinition of Relation for t->s Arcs
definition
let PTN;
let x be T-S_arc of PTN;
redefine func x`1 -> transition of PTN; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
thus x`1 is transition of PTN;
end;
redefine func x`2 -> place of PTN; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
thus x`2 is place of PTN;
end;
end;
:: *S, S* Definitions and Theorems
reserve S0 for Subset of the carrier of PTN;
definition
let PTN, S0;
func *'S0 -> Subset of the carrier' of PTN equals
{ t where t is
transition of PTN : ex f being T-S_arc of PTN, s being place of PTN st s in S0
& f = [t,s] };
coherence
proof
defpred P[set] means ex f being T-S_arc of PTN, s being place of PTN st s
in S0 & f = [$1,s];
{ t where t is transition of PTN : P[t] } is Subset of the carrier'
of PTN from DOMAIN_1:sch 7;
hence thesis;
end;
correctness;
func S0*' -> Subset of the carrier' of PTN equals
{ t where t is
transition of PTN : ex f being S-T_arc of PTN, s being place of PTN st s in S0
& f = [s,t] };
coherence
proof
defpred P[set] means ex f being S-T_arc of PTN, s being place of PTN st s
in S0 & f = [s,$1];
{ t where t is transition of PTN : P[t] } is Subset of the carrier'
of PTN from DOMAIN_1:sch 7;
hence thesis;
end;
correctness;
end;
theorem
*'S0 = {f`1 where f is T-S_arc of PTN : f`2 in S0}
proof
thus *'S0 c= {f`1 where f is T-S_arc of PTN : f`2 in S0}
proof
let x be object;
assume x in *'S0;
then consider t being transition of PTN such that
A1: x = t and
A2: ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [ t,s];
consider f being T-S_arc of PTN, s being place of PTN such that
A3: s in S0 and
A4: f = [t,s] by A2;
f`1 = t & f`2 = s by A4;
hence thesis by A1,A3;
end;
let x be object;
assume x in {f`1 where f is T-S_arc of PTN : f`2 in S0};
then consider f being T-S_arc of PTN such that
A5: x = f`1 & f`2 in S0;
f = [f`1,f`2] by MCART_1:21;
hence thesis by A5;
end;
theorem Th2:
for x being object holds x in *'S0 iff ex f being T-S_arc of PTN, s
being place of PTN st s in S0 & f = [x,s]
proof
let x be object;
thus x in *'S0 implies ex f being T-S_arc of PTN, s being place of PTN st s
in S0 & f = [x,s]
proof
assume x in *'S0;
then consider t being transition of PTN such that
A1: x = t and
A2: ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [ t,s];
consider f being T-S_arc of PTN, s being place of PTN such that
A3: s in S0 & f = [t,s] by A2;
take f, s;
thus thesis by A1,A3;
end;
given f being T-S_arc of PTN, s being place of PTN such that
A4: s in S0 and
A5: f = [x,s];
x = f`1 by A5;
hence thesis by A4,A5;
end;
theorem
S0*' = {f`2 where f is S-T_arc of PTN : f`1 in S0}
proof
thus S0*' c= {f`2 where f is S-T_arc of PTN : f`1 in S0}
proof
let x be object;
assume x in S0*';
then consider t being transition of PTN such that
A1: x = t and
A2: ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [ s,t];
consider f being S-T_arc of PTN, s being place of PTN such that
A3: s in S0 and
A4: f = [s,t] by A2;
f`1 = s & f`2 = t by A4;
hence thesis by A1,A3;
end;
let x be object;
assume x in {f`2 where f is S-T_arc of PTN : f`1 in S0};
then consider f being S-T_arc of PTN such that
A5: x = f`2 & f`1 in S0;
f = [f`1,f`2] by MCART_1:21;
hence thesis by A5;
end;
theorem Th4:
for x being object holds x in S0*' iff ex f being S-T_arc of PTN, s
being place of PTN st s in S0 & f = [s,x]
proof
let x be object;
thus x in S0*' implies ex f being S-T_arc of PTN, s being place of PTN st s
in S0 & f = [s,x]
proof
assume x in S0*';
then consider t being transition of PTN such that
A1: x = t and
A2: ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [ s,t];
consider f being S-T_arc of PTN, s being place of PTN such that
A3: s in S0 & f = [s,t] by A2;
take f, s;
thus thesis by A1,A3;
end;
given f being S-T_arc of PTN, s being place of PTN such that
A4: s in S0 and
A5: f = [s,x];
x = f`2 by A5;
hence thesis by A4,A5;
end;
:: *T, T* Definitions and Theorems
reserve T0 for Subset of the carrier' of PTN;
definition
let PTN, T0;
func *'T0 -> Subset of the carrier of PTN equals
{ s where s is place of PTN
: ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [s,t] }
;
coherence
proof
defpred P[set] means ex f being S-T_arc of PTN, t being transition of PTN
st t in T0 & f = [$1,t];
{ s where s is place of PTN : P[s] } is Subset of the carrier of PTN
from DOMAIN_1:sch 7;
hence thesis;
end;
correctness;
func T0*' -> Subset of the carrier of PTN equals
{ s where s is place of PTN
: ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,s] }
;
coherence
proof
defpred P[set] means ex f being T-S_arc of PTN, t being transition of PTN
st t in T0 & f = [t,$1];
{ s where s is place of PTN : P[s] } is Subset of the carrier of PTN
from DOMAIN_1:sch 7;
hence thesis;
end;
correctness;
end;
theorem
*'T0 = {f`1 where f is S-T_arc of PTN : f`2 in T0}
proof
thus *'T0 c= {f`1 where f is S-T_arc of PTN : f`2 in T0}
proof
let x be object;
assume x in *'T0;
then consider s being place of PTN such that
A1: x = s and
A2: ex f being S-T_arc of PTN, t being transition of PTN st t in T0 &
f = [s,t];
consider f being S-T_arc of PTN, t being transition of PTN such that
A3: t in T0 and
A4: f = [s,t] by A2;
f`1 = s & f`2 = t by A4;
hence thesis by A1,A3;
end;
let x be object;
assume x in {f`1 where f is S-T_arc of PTN : f`2 in T0};
then consider f being S-T_arc of PTN such that
A5: x = f`1 & f`2 in T0;
f = [f`1,f`2] by MCART_1:21;
hence thesis by A5;
end;
theorem Th6:
for x being set holds x in *'T0 iff ex f being S-T_arc of PTN, t
being transition of PTN st t in T0 & f = [x,t]
proof
let x be set;
thus x in *'T0 implies ex f being S-T_arc of PTN, t being transition of PTN
st t in T0 & f = [x,t]
proof
assume x in *'T0;
then consider s being place of PTN such that
A1: x = s and
A2: ex f being S-T_arc of PTN, t being transition of PTN st t in T0 &
f = [s,t];
consider f being S-T_arc of PTN, t being transition of PTN such that
A3: t in T0 & f = [s,t] by A2;
take f, t;
thus thesis by A1,A3;
end;
given f being S-T_arc of PTN, t being transition of PTN such that
A4: t in T0 and
A5: f = [x,t];
x = f`1 by A5;
hence thesis by A4,A5;
end;
theorem
T0*' = {f`2 where f is T-S_arc of PTN : f`1 in T0}
proof
thus T0*' c= {f`2 where f is T-S_arc of PTN : f`1 in T0}
proof
let x be object;
assume x in T0*';
then consider s being place of PTN such that
A1: x = s and
A2: ex f being T-S_arc of PTN, t being transition of PTN st t in T0 &
f = [t,s];
consider f being T-S_arc of PTN, t being transition of PTN such that
A3: t in T0 and
A4: f = [t,s] by A2;
f`1 = t & f`2 = s by A4;
hence thesis by A1,A3;
end;
let x be object;
assume x in {f`2 where f is T-S_arc of PTN : f`1 in T0};
then consider f being T-S_arc of PTN such that
A5: x = f`2 & f`1 in T0;
f = [f`1,f`2] by MCART_1:21;
hence thesis by A5;
end;
theorem Th8:
for x being set holds x in T0*' iff ex f being T-S_arc of PTN, t
being transition of PTN st t in T0 & f = [t,x]
proof
let x be set;
thus x in T0*' implies ex f being T-S_arc of PTN, t being transition of PTN
st t in T0 & f = [t,x]
proof
assume x in T0*';
then consider s being place of PTN such that
A1: x = s and
A2: ex f being T-S_arc of PTN, t being transition of PTN st t in T0 &
f = [t,s];
consider f being T-S_arc of PTN, t being transition of PTN such that
A3: t in T0 & f = [t,s] by A2;
take f, t;
thus thesis by A1,A3;
end;
given f being T-S_arc of PTN, t being transition of PTN such that
A4: t in T0 and
A5: f = [t,x];
x = f`2 by A5;
hence thesis by A4,A5;
end;
theorem
*'{}the carrier of PTN = {}
proof
set x = the Element of *'{}the carrier of PTN;
assume not thesis;
then x in *'{}the carrier of PTN;
then ex t being transition of PTN st x = t & ex f being T-S_arc of PTN, s
being place of PTN st s in {}the carrier of PTN & f = [t,s];
hence contradiction;
end;
theorem
({}the carrier of PTN)*' = {}
proof
set x = the Element of ({}the carrier of PTN)*';
assume not thesis;
then x in ({}the carrier of PTN)*';
then ex t being transition of PTN st x = t & ex f being S-T_arc of PTN, s
being place of PTN st s in {}the carrier of PTN & f = [s,t];
hence contradiction;
end;
theorem
*'{}the carrier' of PTN = {}
proof
set x = the Element of *'{}the carrier' of PTN;
assume not thesis;
then x in *'{}the carrier' of PTN;
then ex s being place of PTN st x = s & ex f being S-T_arc of PTN, t being
transition of PTN st t in {}the carrier' of PTN & f = [s,t];
hence contradiction;
end;
theorem
({}the carrier' of PTN)*' = {}
proof
set x = the Element of ({}the carrier' of PTN)*';
assume not thesis;
then x in ({}the carrier' of PTN)*';
then ex s being place of PTN st x = s & ex f being T-S_arc of PTN, t being
transition of PTN st t in {}the carrier' of PTN & f = [t,s];
hence contradiction;
end;
begin
:: Deadlock-like Attribute for Place Sets
definition
let PTN;
let IT be Subset of the carrier of PTN;
attr IT is Deadlock-like means
*'IT is Subset of IT*';
end;
:: With_Deadlocks Mode for Place\Transition Nets
definition
let IT be Petri_net;
attr IT is With_Deadlocks means
ex S being Subset of the carrier of IT st S is Deadlock-like;
end;
registration
cluster With_Deadlocks for Petri_net;
existence
proof
take PTN1 = TrivialPetriNet;
reconsider s = {} as place of PTN1 by TARSKI:def 1;
reconsider t = {} as transition of PTN1 by TARSKI:def 1;
A1: [#]({{}},{{}}) = {[{},{}]} by ZFMISC_1:29;
then reconsider stf = [{},{}] as S-T_arc of PTN1 by TARSKI:def 1;
reconsider tsf = [{},{}] as T-S_arc of PTN1 by A1,TARSKI:def 1;
{{}} c= the carrier of PTN1;
then reconsider S = {{}} as Subset of the carrier of PTN1;
take S;
tsf = [t,s];
then t in *'S;
then {t} c= *'S by ZFMISC_1:31;
then
A2: {t} = *'S;
stf = [s,t];
then t in S*';
hence *'S is Subset of S*' by A2,ZFMISC_1:31;
end;
end;
begin
:: Trap-like Attribute for Place Sets
definition
let PTN;
let IT be Subset of the carrier of PTN;
attr IT is Trap-like means
IT*' is Subset of *'IT;
end;
:: With_Traps Mode for Place\Transition Nets
definition
let IT be Petri_net;
attr IT is With_Traps means
ex S being Subset of the carrier of IT st S is Trap-like;
end;
registration
cluster With_Traps for Petri_net;
existence
proof
take PTN1 = TrivialPetriNet;
reconsider s = {} as place of PTN1 by TARSKI:def 1;
reconsider t = {} as transition of PTN1 by TARSKI:def 1;
A1: [#]({{}},{{}}) = {[{},{}]} by ZFMISC_1:29;
then reconsider stf = [{},{}] as S-T_arc of PTN1 by TARSKI:def 1;
reconsider tsf = [{},{}] as T-S_arc of PTN1 by A1,TARSKI:def 1;
{{}} c= the carrier of PTN1;
then reconsider S = {{}} as Subset of the carrier of PTN1;
take S;
stf = [s,t];
then t in S*';
then {t} c= S*' by ZFMISC_1:31;
then
A2: {t} = S*';
tsf = [t,s];
then t in *'S;
hence S*' is Subset of *'S by A2,ZFMISC_1:31;
end;
end;
definition
let A, B be non empty set;
let r be non empty Relation of A, B;
redefine func r~ -> non empty Relation of B, A; :: redefines ~ (RELAT_1, definition)
coherence
proof
set x = the Element of r;
consider y, z being object such that
A1: x = [y,z] by RELAT_1:def 1;
[z,y] in r~ by A1,RELAT_1:def 7;
hence thesis;
end;
end;
begin
:: Duality Definitions and Theorems for Place/Transition Nets
definition
let PTN be PT_net_Str;
func PTN.: -> strict PT_net_Str equals
PT_net_Str(# the carrier of PTN, the
carrier' of PTN, (the T-S_Arcs of PTN)~, (the S-T_Arcs of PTN)~ #);
correctness;
end;
registration let PTN be Petri_net;
cluster PTN.: -> with_S-T_arc with_T-S_arc non empty non void;
coherence
proof
(the T-S_Arcs of PTN)~ is non empty;
hence the S-T_Arcs of PTN.: is non empty;
(the S-T_Arcs of PTN)~ is non empty;
hence the T-S_Arcs of PTN.: is non empty;
thus thesis;
end;
end;
theorem
PTN.:.: = the PT_net_Str of PTN;
theorem
the carrier of PTN = the carrier of PTN.: & the carrier' of PTN = the
carrier' of PTN.: & (the S-T_Arcs of PTN)~ = the T-S_Arcs of PTN.: & (the
T-S_Arcs of PTN)~ = the S-T_Arcs of PTN.:;
definition
let PTN;
let S0 be Subset of the carrier of PTN;
func S0.: -> Subset of the carrier of PTN.: equals
S0;
coherence;
end;
definition
let PTN;
let s be place of PTN;
func s.: -> place of PTN.: equals
s;
coherence;
end;
definition
let PTN;
let S0 be Subset of the carrier of PTN.:;
func .:S0 -> Subset of the carrier of PTN equals
S0;
coherence;
end;
definition
let PTN;
let s be place of PTN.:;
func .:s -> place of PTN equals
s;
coherence;
end;
definition
let PTN;
let T0 be Subset of the carrier' of PTN;
func T0.: -> Subset of the carrier' of PTN.: equals
T0;
coherence;
end;
definition
let PTN;
let t be transition of PTN;
func t.: -> transition of PTN.: equals
t;
coherence;
end;
definition
let PTN;
let T0 be Subset of the carrier' of PTN.:;
func .:T0 -> Subset of the carrier' of PTN equals
T0;
coherence;
end;
definition
let PTN;
let t be transition of PTN.:;
func .:t -> transition of PTN equals
t;
coherence;
end;
reserve S for Subset of the carrier of PTN;
theorem Th15:
S.:*' = *'S
proof
thus S.:*' c= *'S
proof
let x be object;
assume x in S.:*';
then consider f being S-T_arc of PTN.:, s being place of PTN.: such that
A1: s in S.: and
A2: f = [s,x] by Th4;
[x,.:s] is T-S_arc of PTN by A2,RELAT_1:def 7;
hence thesis by A1,Th2;
end;
let x be object;
assume x in *'S;
then consider f being T-S_arc of PTN, s being place of PTN such that
A3: s in S and
A4: f = [x,s] by Th2;
[s.:,x] is S-T_arc of PTN.: by A4,RELAT_1:def 7;
hence thesis by A3,Th4;
end;
theorem Th16:
*'(S.:) = S*'
proof
thus *'(S.:) c= S*'
proof
let x be object;
assume x in *'(S.:);
then consider f being T-S_arc of PTN.:, s being place of PTN.: such that
A1: s in S.: and
A2: f = [x,s] by Th2;
[.:s,x] is S-T_arc of PTN by A2,RELAT_1:def 7;
hence thesis by A1,Th4;
end;
let x be object;
assume x in S*';
then consider f being S-T_arc of PTN, s being place of PTN such that
A3: s in S and
A4: f = [s,x] by Th4;
[x,s.:] is T-S_arc of PTN.: by A4,RELAT_1:def 7;
hence thesis by A3,Th2;
end;
theorem
S is Deadlock-like iff S.: is Trap-like
proof
A1: S.:*' = *'S by Th15;
thus S is Deadlock-like implies S.: is Trap-like
by A1,Th16;
assume S.:*' is Subset of *'(S.:);
hence *'S is Subset of S*' by A1,Th16;
end;
theorem
S is Trap-like iff S.: is Deadlock-like
proof
A1: S.:*' = *'S by Th15;
thus S is Trap-like implies S.: is Deadlock-like
by A1,Th16;
assume *'(S.:) is Subset of S.:*';
hence S*' is Subset of *'S by A1,Th16;
end;
theorem
for PTN being Petri_net, t being transition of PTN, S0 being Subset
of the carrier of PTN holds t in S0*' iff *'{t} meets S0
proof
let PTN be Petri_net;
let t be transition of PTN;
let S0 be Subset of the carrier of PTN;
thus t in S0*' implies *'{t} meets S0
proof
assume t in S0*';
then consider f being S-T_arc of PTN, s being place of PTN such that
A1: s in S0 and
A2: f = [s,t] by Th4;
t in {t} by TARSKI:def 1;
then s in *'{t} by A2;
hence *'{t} /\ S0 <> {} by A1,XBOOLE_0:def 4;
end;
assume *'{t} /\ S0 <> {};
then consider s being place of PTN such that
A3: s in *'{t} /\ S0 by SUBSET_1:4;
A4: s in S0 by A3,XBOOLE_0:def 4;
s in *'{t} by A3,XBOOLE_0:def 4;
then consider f being S-T_arc of PTN, t0 being transition of PTN such that
A5: t0 in {t} and
A6: f = [s,t0] by Th6;
t0 = t by A5,TARSKI:def 1;
hence thesis by A4,A6;
end;
theorem
for PTN being Petri_net, t being transition of PTN, S0 being Subset
of the carrier of PTN holds t in *'S0 iff {t}*' meets S0
proof
let PTN be Petri_net;
let t be transition of PTN;
let S0 be Subset of the carrier of PTN;
thus t in *'S0 implies {t}*' meets S0
proof
assume t in *'S0;
then consider f being T-S_arc of PTN, s being place of PTN such that
A1: s in S0 and
A2: f = [t,s] by Th2;
t in {t} by TARSKI:def 1;
then s in {t}*' by A2;
hence {t}*' /\ S0 <> {} by A1,XBOOLE_0:def 4;
end;
assume {t}*' /\ S0 <> {};
then consider s being place of PTN such that
A3: s in {t}*' /\ S0 by SUBSET_1:4;
A4: s in S0 by A3,XBOOLE_0:def 4;
s in {t}*' by A3,XBOOLE_0:def 4;
then consider f being T-S_arc of PTN, t0 being transition of PTN such that
A5: t0 in {t} and
A6: f = [t0,s] by Th8;
t0 = t by A5,TARSKI:def 1;
hence thesis by A4,A6;
end;