:: 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-2012 Association of Mizar Users


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;
:: original:Element
redefine mode Element of r ->  Element of [:A,B:];
coherence
 for b1 being Element of r holds b1 is Element of [:A,B:]
proofend;
end;

:: Place/Transition Net Structure
definition
attrc1 is strict ;
struct PT_net_Str  ->  2-sorted ;
aggrPT_net_Str(# carrier, carrier', S-T_Arcs, T-S_Arcs #) ->  PT_net_Str ;
sel S-T_Arcs c1 ->  Relation of the carrier of c1, the carrier' of c1;
sel T-S_Arcs c1 ->  Relation of the carrier' of c1, the carrier of c1;
end;

definition
let N be PT_net_Str ;
attrN is with_S-T_arc  means :Def1: :: PETRI:def 1
 not the S-T_Arcs of N is empty ;
attrN is with_T-S_arc  means :Def2: :: PETRI:def 2
 not the T-S_Arcs of N is empty ;
end;

:: deftheorem Def1 defines with_S-T_arc PETRI:def_1_:_
 for N being PT_net_Str holds
( N is with_S-T_arc iff not the S-T_Arcs of N is empty );

:: deftheorem Def2 defines with_T-S_arc PETRI:def_2_:_
 for N being PT_net_Str holds
( N is with_T-S_arc iff not the T-S_Arcs of N is empty );

definition
func TrivialPetriNet  ->  PT_net_Str  equals :: PETRI:def 3
 PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);
coherence
 PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #) is PT_net_Str ;
end;

:: deftheorem  defines TrivialPetriNet PETRI:def_3_:_
 TrivialPetriNet = PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);

registration
cluster TrivialPetriNet  ->  non empty non void strict with_S-T_arc with_T-S_arc ;
coherence
 ( TrivialPetriNet is with_S-T_arc & TrivialPetriNet is with_T-S_arc & TrivialPetriNet is strict & not TrivialPetriNet is empty & not TrivialPetriNet is void )
proofend;
end;

registration
cluster non empty non void strict with_S-T_arc with_T-S_arc for PT_net_Str ;
existence
 ex b1 being PT_net_Str st
( not b1 is empty & not b1 is void & b1 is with_S-T_arc & b1 is with_T-S_arc & b1 is strict )
proofend;
end;

registration
let N be with_S-T_arc PT_net_Str ;
cluster the S-T_Arcs of N ->  non empty ;
coherence
 not the S-T_Arcs of N is empty by Def1;
end;

registration
let N be with_T-S_arc PT_net_Str ;
cluster the T-S_Arcs of N ->  non empty ;
coherence
 not the T-S_Arcs of N is empty by Def2;
end;

definition
mode Petri_net is non empty non void with_S-T_arc with_T-S_arc PT_net_Str ;
end;

:: Place, Transition, and Arc (s->t, t->s) Elements
definition
let PTN be Petri_net;
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 be Petri_net;
let x be S-T_arc of PTN;
:: original:`1
redefine funcx `1  ->  place of PTN;
coherence
 x `1 is place of PTN
proofend;
:: original:`2
redefine funcx `2  ->  transition of PTN;
coherence
 x `2 is transition of PTN
proofend;
end;

:: Redefinition of Relation for t->s Arcs
definition
let PTN be Petri_net;
let x be T-S_arc of PTN;
:: original:`1
redefine funcx `1  ->  transition of PTN;
coherence
 x `1 is transition of PTN
proofend;
:: original:`2
redefine funcx `2  ->  place of PTN;
coherence
 x `2 is place of PTN
proofend;
end;

definition
let PTN be Petri_net;
let S0 be Subset of the carrier of PTN;
func *' S0 ->  Subset of the carrier' of PTN equals :: PETRI:def 4
 {  t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [t,s] )  }  ;
coherence
  {  t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [t,s] )  }  is Subset of the carrier' of PTN
proofend;
correctness
;
funcS0 *'  ->  Subset of the carrier' of PTN equals :: PETRI:def 5
 {  t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,t] )  }  ;
coherence
  {  t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,t] )  }  is Subset of the carrier' of PTN
proofend;
correctness
;
end;

:: deftheorem  defines *' PETRI:def_4_:_
 for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds *' S0 =  {  t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [t,s] )  }  ;

:: deftheorem  defines *' PETRI:def_5_:_
 for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds S0 *' =  {  t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,t] )  }  ;

theorem :: PETRI:1
for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds *' S0 =  {  (f `1) where f is T-S_arc of PTN : f `2 in S0  }
proofend;

theorem Th2: :: PETRI:2
for PTN being Petri_net
for S0 being Subset of the carrier of PTN
for x being set holds
( x in *' S0 iff ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [x,s] ) )
proofend;

theorem :: PETRI:3
for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds S0 *' =  {  (f `2) where f is S-T_arc of PTN : f `1 in S0  }
proofend;

theorem Th4: :: PETRI:4
for PTN being Petri_net
for S0 being Subset of the carrier of PTN
for x being set holds
( x in S0 *' iff ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,x] ) )
proofend;

definition
let PTN be Petri_net;
let T0 be Subset of the carrier' of PTN;
func *' T0 ->  Subset of the carrier of PTN equals :: PETRI:def 6
 {  s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [s,t] )  }  ;
coherence
  {  s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [s,t] )  }  is Subset of the carrier of PTN
proofend;
correctness
;
funcT0 *'  ->  Subset of the carrier of PTN equals :: PETRI:def 7
 {  s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,s] )  }  ;
coherence
  {  s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,s] )  }  is Subset of the carrier of PTN
proofend;
correctness
;
end;

:: deftheorem  defines *' PETRI:def_6_:_
 for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds *' T0 =  {  s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [s,t] )  }  ;

:: deftheorem  defines *' PETRI:def_7_:_
 for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds T0 *' =  {  s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,s] )  }  ;

theorem :: PETRI:5
for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds *' T0 =  {  (f `1) where f is S-T_arc of PTN : f `2 in T0  }
proofend;

theorem Th6: :: PETRI:6
for PTN being Petri_net
for T0 being Subset of the carrier' of PTN
for x being set holds
( x in *' T0 iff ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [x,t] ) )
proofend;

theorem :: PETRI:7
for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds T0 *' =  {  (f `2) where f is T-S_arc of PTN : f `1 in T0  }
proofend;

theorem Th8: :: PETRI:8
for PTN being Petri_net
for T0 being Subset of the carrier' of PTN
for x being set holds
( x in T0 *' iff ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,x] ) )
proofend;

theorem :: PETRI:9
for PTN being Petri_net holds *' ({} the carrier of PTN) = {}
proofend;

theorem :: PETRI:10
for PTN being Petri_net holds ({} the carrier of PTN) *' = {}
proofend;

theorem :: PETRI:11
for PTN being Petri_net holds *' ({} the carrier' of PTN) = {}
proofend;

theorem :: PETRI:12
for PTN being Petri_net holds ({} the carrier' of PTN) *' = {}
proofend;

begin

:: Deadlock-like Attribute for Place Sets
definition
let PTN be Petri_net;
let IT be Subset of the carrier of PTN;
attrIT is Deadlock-like  means :: PETRI:def 8
 *' IT is Subset of (IT *');
end;

:: deftheorem  defines Deadlock-like PETRI:def_8_:_
 for PTN being Petri_net
for IT being Subset of the carrier of PTN holds
( IT is Deadlock-like iff *' IT is Subset of (IT *') );

:: With_Deadlocks Mode for Place\Transition Nets
definition
let IT be Petri_net;
attrIT is With_Deadlocks  means :: PETRI:def 9
 ex S being Subset of the carrier of IT st S is Deadlock-like ;
end;

:: deftheorem  defines With_Deadlocks PETRI:def_9_:_
 for IT being Petri_net holds
( IT is With_Deadlocks iff ex S being Subset of the carrier of IT st S is Deadlock-like );

registration
cluster non empty non void V49() with_S-T_arc with_T-S_arc With_Deadlocks for PT_net_Str ;
existence
 ex b1 being Petri_net st b1 is With_Deadlocks
proofend;
end;

begin

:: Trap-like Attribute for Place Sets
definition
let PTN be Petri_net;
let IT be Subset of the carrier of PTN;
attrIT is Trap-like  means :: PETRI:def 10
IT *' is Subset of (*' IT);
end;

:: deftheorem  defines Trap-like PETRI:def_10_:_
 for PTN being Petri_net
for IT being Subset of the carrier of PTN holds
( IT is Trap-like iff IT *' is Subset of (*' IT) );

:: With_Traps Mode for Place\Transition Nets
definition
let IT be Petri_net;
attrIT is With_Traps  means :: PETRI:def 11
 ex S being Subset of the carrier of IT st S is Trap-like ;
end;

:: deftheorem  defines With_Traps PETRI:def_11_:_
 for IT being Petri_net holds
( IT is With_Traps iff ex S being Subset of the carrier of IT st S is Trap-like );

registration
cluster non empty non void V49() with_S-T_arc with_T-S_arc With_Traps for PT_net_Str ;
existence
 ex b1 being Petri_net st b1 is With_Traps
proofend;
end;

definition
let A, B be non empty set ;
let r be non empty Relation of A,B;
:: original:~
redefine funcr ~  ->  non empty Relation of B,A;
coherence
 r ~ is non empty Relation of B,A
proofend;
end;

begin

:: Duality Definitions and Theorems for Place/Transition Nets
definition
let PTN be PT_net_Str ;
funcPTN .:  ->  strict PT_net_Str  equals :: PETRI:def 12
 PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #);
correctness
coherence
PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #) is strict PT_net_Str ;
;
end;

:: deftheorem  defines .: PETRI:def_12_:_
 for PTN being PT_net_Str holds PTN .: = PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #);

registration
let PTN be Petri_net;
clusterPTN .:  ->  non empty non void strict with_S-T_arc with_T-S_arc ;
coherence
 ( PTN .: is with_S-T_arc & PTN .: is with_T-S_arc & not PTN .: is empty & not PTN .: is void )
proofend;
end;

theorem :: PETRI:13
for PTN being Petri_net holds (PTN .:) .: = PT_net_Str(# the carrier of PTN, the carrier' of PTN, the S-T_Arcs of PTN, the T-S_Arcs of PTN #) ;

theorem :: PETRI:14
for PTN being Petri_net holds
( 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 be Petri_net;
let S0 be Subset of the carrier of PTN;
funcS0 .:  ->  Subset of the carrier of (PTN .:) equals :: PETRI:def 13
S0;
coherence
 S0 is Subset of the carrier of (PTN .:) ;
end;

:: deftheorem  defines .: PETRI:def_13_:_
 for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds S0 .: = S0;

definition
let PTN be Petri_net;
let s be place of PTN;
funcs .:  ->  place of (PTN .:) equals :: PETRI:def 14
s;
coherence
 s is place of (PTN .:) ;
end;

:: deftheorem  defines .: PETRI:def_14_:_
 for PTN being Petri_net
for s being place of PTN holds s .: = s;

definition
let PTN be Petri_net;
let S0 be Subset of the carrier of (PTN .:);
func .: S0 ->  Subset of the carrier of PTN equals :: PETRI:def 15
S0;
coherence
 S0 is Subset of the carrier of PTN ;
end;

:: deftheorem  defines .: PETRI:def_15_:_
 for PTN being Petri_net
for S0 being Subset of the carrier of (PTN .:) holds .: S0 = S0;

definition
let PTN be Petri_net;
let s be place of (PTN .:);
func .: s ->  place of PTN equals :: PETRI:def 16
s;
coherence
 s is place of PTN ;
end;

:: deftheorem  defines .: PETRI:def_16_:_
 for PTN being Petri_net
for s being place of (PTN .:) holds .: s = s;

definition
let PTN be Petri_net;
let T0 be Subset of the carrier' of PTN;
funcT0 .:  ->  Subset of the carrier' of (PTN .:) equals :: PETRI:def 17
T0;
coherence
 T0 is Subset of the carrier' of (PTN .:) ;
end;

:: deftheorem  defines .: PETRI:def_17_:_
 for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds T0 .: = T0;

definition
let PTN be Petri_net;
let t be transition of PTN;
funct .:  ->  transition of (PTN .:) equals :: PETRI:def 18
t;
coherence
 t is transition of (PTN .:) ;
end;

:: deftheorem  defines .: PETRI:def_18_:_
 for PTN being Petri_net
for t being transition of PTN holds t .: = t;

definition
let PTN be Petri_net;
let T0 be Subset of the carrier' of (PTN .:);
func .: T0 ->  Subset of the carrier' of PTN equals :: PETRI:def 19
T0;
coherence
 T0 is Subset of the carrier' of PTN ;
end;

:: deftheorem  defines .: PETRI:def_19_:_
 for PTN being Petri_net
for T0 being Subset of the carrier' of (PTN .:) holds .: T0 = T0;

definition
let PTN be Petri_net;
let t be transition of (PTN .:);
func .: t ->  transition of PTN equals :: PETRI:def 20
t;
coherence
 t is transition of PTN ;
end;

:: deftheorem  defines .: PETRI:def_20_:_
 for PTN being Petri_net
for t being transition of (PTN .:) holds .: t = t;

theorem Th15: :: PETRI:15
for PTN being Petri_net
for S being Subset of the carrier of PTN holds (S .:) *' = *' S
proofend;

theorem Th16: :: PETRI:16
for PTN being Petri_net
for S being Subset of the carrier of PTN holds *' (S .:) = S *'
proofend;

theorem :: PETRI:17
for PTN being Petri_net
for S being Subset of the carrier of PTN holds
( S is Deadlock-like iff S .: is Trap-like )
proofend;

theorem :: PETRI:18
for PTN being Petri_net
for S being Subset of the carrier of PTN holds
( S is Trap-like iff S .: is Deadlock-like )
proofend;

theorem :: PETRI:19
for PTN being Petri_net
for t being transition of PTN
for S0 being Subset of the carrier of PTN holds
( t in S0 *' iff *' {t} meets S0 )
proofend;

theorem :: PETRI:20
for PTN being Petri_net
for t being transition of PTN
for S0 being Subset of the carrier of PTN holds
( t in *' S0 iff {t} *' meets S0 )
proofend;