:: PETRI semantic presentation

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Relation of c₁,c₂;
redefine mode Element as Element of c₃ -> Element of [:a₁,a₂:];
coherence

proof end;

end;

definition

attr a₁ is strict;
struct PT_net_Str -> ;
aggr PT_net_Str(# Places, Transitions, S-T_Arcs, T-S_Arcs #) -> PT_net_Str ;
sel Places c₁ -> non empty set ;
sel Transitions c₁ -> non empty set ;
sel S-T_Arcs c₁ -> non empty Relation of the Places of a₁,the Transitions of a₁;
sel T-S_Arcs c₁ -> non empty Relation of the Transitions of a₁,the Places of a₁;

end;

definition

let c₁ be PT_net_Str ;
mode place of a₁ is Element of the Places of a₁;
mode places of a₁ is Element of the Places of a₁;
mode transition of a₁ is Element of the Transitions of a₁;
mode transitions of a₁ is Element of the Transitions of a₁;
mode S-T_arc of a₁ is Element of the S-T_Arcs of a₁;
mode T-S_arc of a₁ is Element of the T-S_Arcs of a₁;

end;

definition

let c₁ be PT_net_Str ;
let c₂ be S-T_arc of c₁;
redefine func `1 as c₂ `1 -> place of a₁;
coherence

proof end;

redefine func `2 as c₂ `2 -> transition of a₁;
coherence

proof end;

end;

definition

let c₁ be PT_net_Str ;
let c₂ be T-S_arc of c₁;
redefine func `1 as c₂ `1 -> transition of a₁;
coherence

proof end;

redefine func `2 as c₂ `2 -> place of a₁;
coherence

proof end;

end;

definition

let c₁ be PT_net_Str ;
let c₂ be Subset of the Places of c₁;
func *' c₂ -> Subset of the Transitions of a₁ equals :: PETRI:def 1
{ b₁ where B is transition of a₁ : ex b₁ being T-S_arc of a₁ex b₂ being place of a₁ st
( b₃ in a₂ & b₂ = [b₁,b₃] ) } ;
coherence

proof end;

correctness ;
func c₂ *' -> Subset of the Transitions of a₁ equals :: PETRI:def 2
{ b₁ where B is transition of a₁ : ex b₁ being S-T_arc of a₁ex b₂ being place of a₁ st
( b₃ in a₂ & b₂ = [b₃,b₁] ) } ;
coherence

proof end;

correctness ;

end;

:: deftheorem Def1 defines *' PETRI:def 1 :

:: deftheorem Def2 defines *' PETRI:def 2 :

theorem Th1: :: PETRI:1

for b₁ being PT_net_Str
for b₂ being Subset of the Places of b₁ holds *' b₂ = { (b₃ `1 ) where B is T-S_arc of b₁ : b₃ `2 in b₂ }

proof end;

theorem Th2: :: PETRI:2

for b₁ being PT_net_Str
for b₂ being Subset of the Places of b₁
for b₃ being set holds
( b₃ in *' b₂ iff ex b₄ being T-S_arc of b₁ex b₅ being place of b₁ st
( b₅ in b₂ & b₄ = [b₃,b₅] ) )

proof end;

theorem Th3: :: PETRI:3

for b₁ being PT_net_Str
for b₂ being Subset of the Places of b₁ holds b₂ *' = { (b₃ `2 ) where B is S-T_arc of b₁ : b₃ `1 in b₂ }

proof end;

theorem Th4: :: PETRI:4

for b₁ being PT_net_Str
for b₂ being Subset of the Places of b₁
for b₃ being set holds
( b₃ in b₂ *' iff ex b₄ being S-T_arc of b₁ex b₅ being place of b₁ st
( b₅ in b₂ & b₄ = [b₅,b₃] ) )

proof end;

definition

let c₁ be PT_net_Str ;
let c₂ be Subset of the Transitions of c₁;
func *' c₂ -> Subset of the Places of a₁ equals :: PETRI:def 3
{ b₁ where B is place of a₁ : ex b₁ being S-T_arc of a₁ex b₂ being transition of a₁ st
( b₃ in a₂ & b₂ = [b₁,b₃] ) } ;
coherence

proof end;

correctness ;
func c₂ *' -> Subset of the Places of a₁ equals :: PETRI:def 4
{ b₁ where B is place of a₁ : ex b₁ being T-S_arc of a₁ex b₂ being transition of a₁ st
( b₃ in a₂ & b₂ = [b₃,b₁] ) } ;
coherence

proof end;

correctness ;

end;

:: deftheorem Def3 defines *' PETRI:def 3 :

:: deftheorem Def4 defines *' PETRI:def 4 :

theorem Th5: :: PETRI:5

for b₁ being PT_net_Str
for b₂ being Subset of the Transitions of b₁ holds *' b₂ = { (b₃ `1 ) where B is S-T_arc of b₁ : b₃ `2 in b₂ }

proof end;

theorem Th6: :: PETRI:6

for b₁ being PT_net_Str
for b₂ being Subset of the Transitions of b₁
for b₃ being set holds
( b₃ in *' b₂ iff ex b₄ being S-T_arc of b₁ex b₅ being transition of b₁ st
( b₅ in b₂ & b₄ = [b₃,b₅] ) )

proof end;

theorem Th7: :: PETRI:7

for b₁ being PT_net_Str
for b₂ being Subset of the Transitions of b₁ holds b₂ *' = { (b₃ `2 ) where B is T-S_arc of b₁ : b₃ `1 in b₂ }

proof end;

theorem Th8: :: PETRI:8

for b₁ being PT_net_Str
for b₂ being Subset of the Transitions of b₁
for b₃ being set holds
( b₃ in b₂ *' iff ex b₄ being T-S_arc of b₁ex b₅ being transition of b₁ st
( b₅ in b₂ & b₄ = [b₅,b₃] ) )

proof end;

theorem Th9: :: PETRI:9

for b₁ being PT_net_Str holds *' ({} the Places of b₁) = {}

proof end;

theorem Th10: :: PETRI:10

for b₁ being PT_net_Str holds ({} the Places of b₁) *' = {}

proof end;

theorem Th11: :: PETRI:11

for b₁ being PT_net_Str holds *' ({} the Transitions of b₁) = {}

proof end;

theorem Th12: :: PETRI:12

for b₁ being PT_net_Str holds ({} the Transitions of b₁) *' = {}

proof end;

definition

let c₁ be PT_net_Str ;
let c₂ be Subset of the Places of c₁;
attr a₂ is Deadlock-like means :: PETRI:def 5
*' a₂ is Subset of (a₂ *' );

end;

:: deftheorem Def5 defines Deadlock-like PETRI:def 5 :

definition

let c₁ be PT_net_Str ;
attr a₁ is With_Deadlocks means :: PETRI:def 6
ex b₁ being Subset of the Places of a₁ st b₁ is Deadlock-like;

end;

:: deftheorem Def6 defines With_Deadlocks PETRI:def 6 :

registration

cluster With_Deadlocks PT_net_Str ;
existence

proof end;

end;

definition

let c₁ be PT_net_Str ;
let c₂ be Subset of the Places of c₁;
attr a₂ is Trap-like means :: PETRI:def 7
a₂ *' is Subset of (*' a₂);

end;

:: deftheorem Def7 defines Trap-like PETRI:def 7 :

definition

let c₁ be PT_net_Str ;
attr a₁ is With_Traps means :: PETRI:def 8
ex b₁ being Subset of the Places of a₁ st b₁ is Trap-like;

end;

:: deftheorem Def8 defines With_Traps PETRI:def 8 :

registration

cluster With_Traps PT_net_Str ;
existence

proof end;

end;

definition

let c₁, c₂ be non empty set ;
let c₃ be non empty Relation of c₁,c₂;
redefine func ~ as c₃ ~ -> non empty Relation of a₂,a₁;
coherence

proof end;

end;

definition

let c₁ be PT_net_Str ;
func c₁ .: -> strict PT_net_Str equals :: PETRI:def 9
PT_net_Str(# the Places of a₁,the Transitions of a₁,(the T-S_Arcs of a₁ ~ ),(the S-T_Arcs of a₁ ~ ) #);
correctness ;

end;

:: deftheorem Def9 defines .: PETRI:def 9 :

theorem Th13: :: PETRI:13

for b₁ being PT_net_Str holds (b₁ .: ) .: = PT_net_Str(# the Places of b₁,the Transitions of b₁,the S-T_Arcs of b₁,the T-S_Arcs of b₁ #) ;

theorem Th14: :: PETRI:14

for b₁ being PT_net_Str holds
( the Places of b₁ = the Places of (b₁ .: ) & the Transitions of b₁ = the Transitions of (b₁ .: ) & the S-T_Arcs of b₁ ~ = the T-S_Arcs of (b₁ .: ) & the T-S_Arcs of b₁ ~ = the S-T_Arcs of (b₁ .: ) ) ;

definition

let c₁ be PT_net_Str ;
let c₂ be Subset of the Places of c₁;
func c₂ .: -> Subset of the Places of (a₁ .: ) equals :: PETRI:def 10
a₂;
coherence ;

end;

:: deftheorem Def10 defines .: PETRI:def 10 :

definition

let c₁ be PT_net_Str ;
let c₂ be place of c₁;
func c₂ .: -> place of (a₁ .: ) equals :: PETRI:def 11
a₂;
coherence ;

end;

:: deftheorem Def11 defines .: PETRI:def 11 :

definition

let c₁ be PT_net_Str ;
let c₂ be Subset of the Places of (c₁ .: );
func .: c₂ -> Subset of the Places of a₁ equals :: PETRI:def 12
a₂;
coherence ;

end;

:: deftheorem Def12 defines .: PETRI:def 12 :

definition

let c₁ be PT_net_Str ;
let c₂ be place of (c₁ .: );
func .: c₂ -> place of a₁ equals :: PETRI:def 13
a₂;
coherence ;

end;

:: deftheorem Def13 defines .: PETRI:def 13 :

definition

let c₁ be PT_net_Str ;
let c₂ be Subset of the Transitions of c₁;
func c₂ .: -> Subset of the Transitions of (a₁ .: ) equals :: PETRI:def 14
a₂;
coherence ;

end;

:: deftheorem Def14 defines .: PETRI:def 14 :

definition

let c₁ be PT_net_Str ;
let c₂ be transition of c₁;
func c₂ .: -> transition of (a₁ .: ) equals :: PETRI:def 15
a₂;
coherence ;

end;

:: deftheorem Def15 defines .: PETRI:def 15 :

definition

let c₁ be PT_net_Str ;
let c₂ be Subset of the Transitions of (c₁ .: );
func .: c₂ -> Subset of the Transitions of a₁ equals :: PETRI:def 16
a₂;
coherence ;

end;

:: deftheorem Def16 defines .: PETRI:def 16 :

definition

let c₁ be PT_net_Str ;
let c₂ be transition of (c₁ .: );
func .: c₂ -> transition of a₁ equals :: PETRI:def 17
a₂;
coherence ;

end;

:: deftheorem Def17 defines .: PETRI:def 17 :

theorem Th15: :: PETRI:15

for b₁ being PT_net_Str
for b₂ being Subset of the Places of b₁ holds (b₂ .: ) *' = *' b₂

proof end;

theorem Th16: :: PETRI:16

for b₁ being PT_net_Str
for b₂ being Subset of the Places of b₁ holds *' (b₂ .: ) = b₂ *'

proof end;

theorem Th17: :: PETRI:17

for b₁ being PT_net_Str
for b₂ being Subset of the Places of b₁ holds
( b₂ is Deadlock-like iff b₂ .: is Trap-like )

proof end;

theorem Th18: :: PETRI:18

for b₁ being PT_net_Str
for b₂ being Subset of the Places of b₁ holds
( b₂ is Trap-like iff b₂ .: is Deadlock-like )

proof end;

theorem Th19: :: PETRI:19

for b₁ being PT_net_Str
for b₂ being transition of b₁
for b₃ being Subset of the Places of b₁ holds
( b₂ in b₃ *' iff *' {b₂} meets b₃ )

proof end;

theorem Th20: :: PETRI:20

for b₁ being PT_net_Str
for b₂ being transition of b₁
for b₃ being Subset of the Places of b₁ holds
( b₂ in *' b₃ iff {b₂} *' meets b₃ )

proof end;