:: PETRI semantic presentation

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

proof end;

end;

definition

attr c₁ 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 c₁,the Transitions of c₁;
sel T-S_Arcs c₁ -> non empty Relation of the Transitions of c₁,the Places of c₁;

end;

definition

let PTN be PT_net_Str ;
mode place of PTN is Element of the Places of PTN;
mode places of PTN is Element of the Places of PTN;
mode transition of PTN is Element of the Transitions of PTN;
mode transitions of PTN is Element of the Transitions 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;

definition

let PTN be PT_net_Str ;
let x be S-T_arc of PTN;
:: original: `1
redefine func x `1 -> place of PTN;
coherence

proof end;

:: original: `2
redefine func x `2 -> transition of PTN;
coherence

proof end;

end;

definition

let PTN be PT_net_Str ;
let x be T-S_arc of PTN;
:: original: `1
redefine func x `1 -> transition of PTN;
coherence

proof end;

:: original: `2
redefine func x `2 -> place of PTN;
coherence

proof end;

end;

definition

let PTN be PT_net_Str ;
let S0 be Subset of the Places of PTN;
func *' S0 -> Subset of the Transitions of PTN equals :: PETRI:def 1
{ 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

proof end;

correctness ;
func S0 *' -> Subset of the Transitions of PTN equals :: PETRI:def 2
{ 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

proof end;

correctness ;

end;

:: deftheorem defines *' PETRI:def 1 :

:: deftheorem defines *' PETRI:def 2 :

theorem :: PETRI:1

for PTN being PT_net_Str
for S0 being Subset of the Places of PTN holds *' S0 = { (f `1 ) where f is T-S_arc of PTN : f `2 in S0 }

proof end;

theorem Th2: :: PETRI:2

for PTN being PT_net_Str
for S0 being Subset of the Places 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] ) )

proof end;

theorem :: PETRI:3

for PTN being PT_net_Str
for S0 being Subset of the Places of PTN holds S0 *' = { (f `2 ) where f is S-T_arc of PTN : f `1 in S0 }

proof end;

theorem Th4: :: PETRI:4

for PTN being PT_net_Str
for S0 being Subset of the Places 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] ) )

proof end;

definition

let PTN be PT_net_Str ;
let T0 be Subset of the Transitions of PTN;
func *' T0 -> Subset of the Places of PTN equals :: PETRI:def 3
{ 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

proof end;

correctness ;
func T0 *' -> Subset of the Places of PTN equals :: PETRI:def 4
{ 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

proof end;

correctness ;

end;

:: deftheorem defines *' PETRI:def 3 :

:: deftheorem defines *' PETRI:def 4 :

theorem :: PETRI:5

for PTN being PT_net_Str
for T0 being Subset of the Transitions of PTN holds *' T0 = { (f `1 ) where f is S-T_arc of PTN : f `2 in T0 }

proof end;

theorem Th6: :: PETRI:6

for PTN being PT_net_Str
for T0 being Subset of the Transitions 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] ) )

proof end;

theorem :: PETRI:7

for PTN being PT_net_Str
for T0 being Subset of the Transitions of PTN holds T0 *' = { (f `2 ) where f is T-S_arc of PTN : f `1 in T0 }

proof end;

theorem Th8: :: PETRI:8

for PTN being PT_net_Str
for T0 being Subset of the Transitions 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] ) )

proof end;

theorem :: PETRI:9

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

proof end;

theorem :: PETRI:10

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

proof end;

theorem :: PETRI:11

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

proof end;

theorem :: PETRI:12

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

proof end;

definition

let PTN be PT_net_Str ;
let IT be Subset of the Places of PTN;
attr IT is Deadlock-like means :: PETRI:def 5
*' IT is Subset of (IT *' );

end;

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

definition

let IT be PT_net_Str ;
attr IT is With_Deadlocks means :: PETRI:def 6
ex S being Subset of the Places of IT st S is Deadlock-like;

end;

:: deftheorem defines With_Deadlocks PETRI:def 6 :

registration

cluster With_Deadlocks PT_net_Str ;
existence

proof end;

end;

definition

let PTN be PT_net_Str ;
let IT be Subset of the Places of PTN;
attr IT is Trap-like means :: PETRI:def 7
IT *' is Subset of (*' IT);

end;

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

definition

let IT be PT_net_Str ;
attr IT is With_Traps means :: PETRI:def 8
ex S being Subset of the Places of IT st S is Trap-like;

end;

:: deftheorem defines With_Traps PETRI:def 8 :

registration

cluster With_Traps PT_net_Str ;
existence

proof end;

end;

definition

let A, B be non empty set ;
let r be non empty Relation of A,B;
:: original: ~
redefine func r ~ -> non empty Relation of B,A;
coherence

proof end;

end;

definition

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

end;

:: deftheorem defines .: PETRI:def 9 :

theorem :: PETRI:13

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

theorem :: PETRI:14

for PTN being PT_net_Str holds
( the Places of PTN = the Places of (PTN .: ) & the Transitions of PTN = the Transitions 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 PT_net_Str ;
let S0 be Subset of the Places of PTN;
func S0 .: -> Subset of the Places of (PTN .: ) equals :: PETRI:def 10
S0;
coherence ;

end;

:: deftheorem defines .: PETRI:def 10 :

definition

let PTN be PT_net_Str ;
let s be place of PTN;
func s .: -> place of (PTN .: ) equals :: PETRI:def 11
s;
coherence ;

end;

:: deftheorem defines .: PETRI:def 11 :

definition

let PTN be PT_net_Str ;
let S0 be Subset of the Places of (PTN .: );
func .: S0 -> Subset of the Places of PTN equals :: PETRI:def 12
S0;
coherence ;

end;

:: deftheorem defines .: PETRI:def 12 :

definition

let PTN be PT_net_Str ;
let s be place of (PTN .: );
func .: s -> place of PTN equals :: PETRI:def 13
s;
coherence ;

end;

:: deftheorem defines .: PETRI:def 13 :

definition

let PTN be PT_net_Str ;
let T0 be Subset of the Transitions of PTN;
func T0 .: -> Subset of the Transitions of (PTN .: ) equals :: PETRI:def 14
T0;
coherence ;

end;

:: deftheorem defines .: PETRI:def 14 :

definition

let PTN be PT_net_Str ;
let t be transition of PTN;
func t .: -> transition of (PTN .: ) equals :: PETRI:def 15
t;
coherence ;

end;

:: deftheorem defines .: PETRI:def 15 :

definition

let PTN be PT_net_Str ;
let T0 be Subset of the Transitions of (PTN .: );
func .: T0 -> Subset of the Transitions of PTN equals :: PETRI:def 16
T0;
coherence ;

end;

:: deftheorem defines .: PETRI:def 16 :

definition

let PTN be PT_net_Str ;
let t be transition of (PTN .: );
func .: t -> transition of PTN equals :: PETRI:def 17
t;
coherence ;

end;

:: deftheorem defines .: PETRI:def 17 :

theorem Th15: :: PETRI:15

for PTN being PT_net_Str
for S being Subset of the Places of PTN holds (S .: ) *' = *' S

proof end;

theorem Th16: :: PETRI:16

for PTN being PT_net_Str
for S being Subset of the Places of PTN holds *' (S .: ) = S *'

proof end;

theorem :: PETRI:17

for PTN being PT_net_Str
for S being Subset of the Places of PTN holds
( S is Deadlock-like iff S .: is Trap-like )

proof end;

theorem :: PETRI:18

for PTN being PT_net_Str
for S being Subset of the Places of PTN holds
( S is Trap-like iff S .: is Deadlock-like )

proof end;

theorem :: PETRI:19

for PTN being PT_net_Str
for t being transition of PTN
for S0 being Subset of the Places of PTN holds
( t in S0 *' iff *' {t} meets S0 )

proof end;

theorem :: PETRI:20

for PTN being PT_net_Str
for t being transition of PTN
for S0 being Subset of the Places of PTN holds
( t in *' S0 iff {t} *' meets S0 )

proof end;