:: by Pauline N. Kawamoto, Yasushi Fuwa and Yatsuka Nakamura

::

:: Received October 8, 1993

:: Copyright (c) 1993-2018 Association of Mizar Users

theorem Th1: :: BOOLMARK:1

for A, B being non empty set

for f being Function of A,B

for C being Subset of A

for v being Element of B holds f +* (C --> v) is Function of A,B

for f being Function of A,B

for C being Subset of A

for v being Element of B holds f +* (C --> v) is Function of A,B

proof end;

theorem Th2: :: BOOLMARK:2

for X, Y being non empty set

for A, B being Subset of X

for f being Function of X,Y st f .: A misses f .: B holds

A misses B

for A, B being Subset of X

for f being Function of X,Y st f .: A misses f .: B holds

A misses B

proof end;

theorem Th3: :: BOOLMARK:3

for A, B being set

for f being Function

for x being set st A misses B holds

(f +* (A --> x)) .: B = f .: B

for f being Function

for x being set st A misses B holds

(f +* (A --> x)) .: B = f .: B

proof end;

:: Boolean Markings of Place/Transition Net

definition

let PTN be PT_net_Str ;

coherence

Funcs ( the carrier of PTN,BOOLEAN) is FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN ;

;

end;
func Bool_marks_of PTN -> FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN equals :: BOOLMARK:def 1

Funcs ( the carrier of PTN,BOOLEAN);

correctness Funcs ( the carrier of PTN,BOOLEAN);

coherence

Funcs ( the carrier of PTN,BOOLEAN) is FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN ;

;

:: deftheorem defines Bool_marks_of BOOLMARK:def 1 :

for PTN being PT_net_Str holds Bool_marks_of PTN = Funcs ( the carrier of PTN,BOOLEAN);

for PTN being PT_net_Str holds Bool_marks_of PTN = Funcs ( the carrier of PTN,BOOLEAN);

:: Firable and Firing Conditions for Transitions

:: deftheorem defines is_firable_on BOOLMARK:def 2 :

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for t being transition of PTN holds

( t is_firable_on M0 iff M0 .: (*' {t}) c= {TRUE} );

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for t being transition of PTN holds

( t is_firable_on M0 iff M0 .: (*' {t}) c= {TRUE} );

notation

let PTN be Petri_net;

let M0 be Boolean_marking of PTN;

let t be transition of PTN;

antonym t is_not_firable_on M0 for t is_firable_on M0;

end;
let M0 be Boolean_marking of PTN;

let t be transition of PTN;

antonym t is_not_firable_on M0 for t is_firable_on M0;

definition

let PTN be Petri_net;

let M0 be Boolean_marking of PTN;

let t be transition of PTN;

(M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE) is Boolean_marking of PTN

;

end;
let M0 be Boolean_marking of PTN;

let t be transition of PTN;

func Firing (t,M0) -> Boolean_marking of PTN equals :: BOOLMARK:def 3

(M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE);

coherence (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE);

(M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE) is Boolean_marking of PTN

proof end;

correctness ;

:: deftheorem defines Firing BOOLMARK:def 3 :

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for t being transition of PTN holds Firing (t,M0) = (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE);

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for t being transition of PTN holds Firing (t,M0) = (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE);

:: Firable and Firing Conditions for Transition Sequences

definition

let PTN be Petri_net;

let M0 be Boolean_marking of PTN;

let Q be FinSequence of the carrier' of PTN;

end;
let M0 be Boolean_marking of PTN;

let Q be FinSequence of the carrier' of PTN;

pred Q is_firable_on M0 means :: BOOLMARK:def 4

( Q = {} or ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & Q /. 1 is_firable_on M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds

( Q /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) );

( Q = {} or ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & Q /. 1 is_firable_on M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds

( Q /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) );

:: deftheorem defines is_firable_on BOOLMARK:def 4 :

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for Q being FinSequence of the carrier' of PTN holds

( Q is_firable_on M0 iff ( Q = {} or ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & Q /. 1 is_firable_on M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds

( Q /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) );

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for Q being FinSequence of the carrier' of PTN holds

( Q is_firable_on M0 iff ( Q = {} or ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & Q /. 1 is_firable_on M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds

( Q /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) );

notation

let PTN be Petri_net;

let M0 be Boolean_marking of PTN;

let Q be FinSequence of the carrier' of PTN;

antonym Q is_not_firable_on M0 for Q is_firable_on M0;

end;
let M0 be Boolean_marking of PTN;

let Q be FinSequence of the carrier' of PTN;

antonym Q is_not_firable_on M0 for Q is_firable_on M0;

definition

let PTN be Petri_net;

let M0 be Boolean_marking of PTN;

let Q be FinSequence of the carrier' of PTN;

( ( Q = {} implies ex b_{1} being Boolean_marking of PTN st b_{1} = M0 ) & ( not Q = {} implies ex b_{1} being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & b_{1} = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) )

for b_{1}, b_{2} being Boolean_marking of PTN holds

( ( Q = {} & b_{1} = M0 & b_{2} = M0 implies b_{1} = b_{2} ) & ( not Q = {} & ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & b_{1} = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) & ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & b_{2} = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies b_{1} = b_{2} ) )

consistency

for b_{1} being Boolean_marking of PTN holds verum;

;

end;
let M0 be Boolean_marking of PTN;

let Q be FinSequence of the carrier' of PTN;

func Firing (Q,M0) -> Boolean_marking of PTN means :Def5: :: BOOLMARK:def 5

it = M0 if Q = {}

otherwise ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & it = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) );

existence it = M0 if Q = {}

otherwise ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & it = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) );

( ( Q = {} implies ex b

( len Q = len M & b

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) )

proof end;

uniqueness for b

( ( Q = {} & b

( len Q = len M & b

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) & ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & b

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies b

proof end;

correctness consistency

for b

;

:: deftheorem Def5 defines Firing BOOLMARK:def 5 :

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for Q being FinSequence of the carrier' of PTN

for b_{4} being Boolean_marking of PTN holds

( ( Q = {} implies ( b_{4} = Firing (Q,M0) iff b_{4} = M0 ) ) & ( not Q = {} implies ( b_{4} = Firing (Q,M0) iff ex M being FinSequence of Bool_marks_of PTN st

( len Q = len M & b_{4} = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Nat st i < len Q & i > 0 holds

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) );

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for Q being FinSequence of the carrier' of PTN

for b

( ( Q = {} implies ( b

( len Q = len M & b

M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) );

theorem Th5: :: BOOLMARK:5

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for t being transition of PTN

for s being place of PTN st s in {t} *' holds

(Firing (t,M0)) . s = TRUE

for M0 being Boolean_marking of PTN

for t being transition of PTN

for s being place of PTN st s in {t} *' holds

(Firing (t,M0)) . s = TRUE

proof end;

Lm1: now :: thesis: for PTN being Petri_net

for Sd being non empty Subset of the carrier of PTN st ( for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} ) holds

Sd is Deadlock-like

for Sd being non empty Subset of the carrier of PTN st ( for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} ) holds

Sd is Deadlock-like

let PTN be Petri_net; :: thesis: for Sd being non empty Subset of the carrier of PTN st ( for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} ) holds

Sd is Deadlock-like

let Sd be non empty Subset of the carrier of PTN; :: thesis: ( ( for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} ) implies Sd is Deadlock-like )

set M0 = ( the carrier of PTN --> TRUE) +* (Sd --> FALSE);

A1: [#] the carrier of PTN = the carrier of PTN ;

( dom ( the carrier of PTN --> TRUE) = the carrier of PTN & dom (Sd --> FALSE) = Sd ) by FUNCOP_1:13;

then A2: dom (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) = the carrier of PTN \/ Sd by FUNCT_4:def 1

.= the carrier of PTN by A1, SUBSET_1:11 ;

A3: rng (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) c= (rng ( the carrier of PTN --> TRUE)) \/ (rng (Sd --> FALSE)) by FUNCT_4:17;

rng (Sd --> FALSE) c= {FALSE} by FUNCOP_1:13;

then A4: rng (Sd --> FALSE) c= BOOLEAN by XBOOLE_1:1;

rng ( the carrier of PTN --> TRUE) c= {TRUE} by FUNCOP_1:13;

then rng ( the carrier of PTN --> TRUE) c= BOOLEAN by XBOOLE_1:1;

then (rng ( the carrier of PTN --> TRUE)) \/ (rng (Sd --> FALSE)) c= BOOLEAN by A4, XBOOLE_1:8;

then rng (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) c= BOOLEAN by A3, XBOOLE_1:1;

then reconsider M0 = ( the carrier of PTN --> TRUE) +* (Sd --> FALSE) as Boolean_marking of PTN by A2, FUNCT_2:def 2;

assume A5: for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} ; :: thesis: Sd is Deadlock-like

assume not Sd is Deadlock-like ; :: thesis: contradiction

then not *' Sd c= Sd *' ;

then consider t being transition of PTN such that

A6: t in *' Sd and

A7: not t in Sd *' by SUBSET_1:2;

{t} *' meets Sd by A6, PETRI:20;

then consider s being object such that

A8: s in ({t} *') /\ Sd by XBOOLE_0:4;

s in {t} *' by A8, XBOOLE_0:def 4;

then A9: (Firing (t,M0)) . s = TRUE by Th5;

s in Sd by A8, XBOOLE_0:def 4;

then TRUE in (Firing (t,M0)) .: Sd by A9, FUNCT_2:35;

then A10: (Firing (t,M0)) .: Sd <> {FALSE} by TARSKI:def 1;

Sd misses *' {t} by A7, PETRI:19;

then A11: ( the carrier of PTN --> TRUE) .: (*' {t}) = M0 .: (*' {t}) by Th3;

( rng ( the carrier of PTN --> TRUE) c= {TRUE} & ( the carrier of PTN --> TRUE) .: (*' {t}) c= rng ( the carrier of PTN --> TRUE) ) by FUNCOP_1:13, RELAT_1:111;

then M0 .: (*' {t}) c= {TRUE} by A11, XBOOLE_1:1;

then A12: t is_firable_on M0 ;

M0 .: Sd = {FALSE} by Th4;

hence contradiction by A5, A12, A10; :: thesis: verum

end;
for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} ) holds

Sd is Deadlock-like

let Sd be non empty Subset of the carrier of PTN; :: thesis: ( ( for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} ) implies Sd is Deadlock-like )

set M0 = ( the carrier of PTN --> TRUE) +* (Sd --> FALSE);

A1: [#] the carrier of PTN = the carrier of PTN ;

( dom ( the carrier of PTN --> TRUE) = the carrier of PTN & dom (Sd --> FALSE) = Sd ) by FUNCOP_1:13;

then A2: dom (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) = the carrier of PTN \/ Sd by FUNCT_4:def 1

.= the carrier of PTN by A1, SUBSET_1:11 ;

A3: rng (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) c= (rng ( the carrier of PTN --> TRUE)) \/ (rng (Sd --> FALSE)) by FUNCT_4:17;

rng (Sd --> FALSE) c= {FALSE} by FUNCOP_1:13;

then A4: rng (Sd --> FALSE) c= BOOLEAN by XBOOLE_1:1;

rng ( the carrier of PTN --> TRUE) c= {TRUE} by FUNCOP_1:13;

then rng ( the carrier of PTN --> TRUE) c= BOOLEAN by XBOOLE_1:1;

then (rng ( the carrier of PTN --> TRUE)) \/ (rng (Sd --> FALSE)) c= BOOLEAN by A4, XBOOLE_1:8;

then rng (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) c= BOOLEAN by A3, XBOOLE_1:1;

then reconsider M0 = ( the carrier of PTN --> TRUE) +* (Sd --> FALSE) as Boolean_marking of PTN by A2, FUNCT_2:def 2;

assume A5: for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} ; :: thesis: Sd is Deadlock-like

assume not Sd is Deadlock-like ; :: thesis: contradiction

then not *' Sd c= Sd *' ;

then consider t being transition of PTN such that

A6: t in *' Sd and

A7: not t in Sd *' by SUBSET_1:2;

{t} *' meets Sd by A6, PETRI:20;

then consider s being object such that

A8: s in ({t} *') /\ Sd by XBOOLE_0:4;

s in {t} *' by A8, XBOOLE_0:def 4;

then A9: (Firing (t,M0)) . s = TRUE by Th5;

s in Sd by A8, XBOOLE_0:def 4;

then TRUE in (Firing (t,M0)) .: Sd by A9, FUNCT_2:35;

then A10: (Firing (t,M0)) .: Sd <> {FALSE} by TARSKI:def 1;

Sd misses *' {t} by A7, PETRI:19;

then A11: ( the carrier of PTN --> TRUE) .: (*' {t}) = M0 .: (*' {t}) by Th3;

( rng ( the carrier of PTN --> TRUE) c= {TRUE} & ( the carrier of PTN --> TRUE) .: (*' {t}) c= rng ( the carrier of PTN --> TRUE) ) by FUNCOP_1:13, RELAT_1:111;

then M0 .: (*' {t}) c= {TRUE} by A11, XBOOLE_1:1;

then A12: t is_firable_on M0 ;

M0 .: Sd = {FALSE} by Th4;

hence contradiction by A5, A12, A10; :: thesis: verum

theorem :: BOOLMARK:6

for PTN being Petri_net

for Sd being non empty Subset of the carrier of PTN holds

( Sd is Deadlock-like iff for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} )

for Sd being non empty Subset of the carrier of PTN holds

( Sd is Deadlock-like iff for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for t being transition of PTN st t is_firable_on M0 holds

(Firing (t,M0)) .: Sd = {FALSE} )

proof end;

theorem Th7: :: BOOLMARK:7

for D being non empty set

for Q0, Q1 being FinSequence of D

for i being Element of NAT st 1 <= i & i <= len Q0 holds

(Q0 ^ Q1) /. i = Q0 /. i

for Q0, Q1 being FinSequence of D

for i being Element of NAT st 1 <= i & i <= len Q0 holds

(Q0 ^ Q1) /. i = Q0 /. i

proof end;

theorem Th8: :: BOOLMARK:8

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for Q0, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))

for M0 being Boolean_marking of PTN

for Q0, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0)))

proof end;

theorem Th9: :: BOOLMARK:9

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for Q0, Q1 being FinSequence of the carrier' of PTN st Q0 ^ Q1 is_firable_on M0 holds

( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 )

for M0 being Boolean_marking of PTN

for Q0, Q1 being FinSequence of the carrier' of PTN st Q0 ^ Q1 is_firable_on M0 holds

( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 )

proof end;

theorem Th10: :: BOOLMARK:10

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for t being transition of PTN holds

( t is_firable_on M0 iff <*t*> is_firable_on M0 )

for M0 being Boolean_marking of PTN

for t being transition of PTN holds

( t is_firable_on M0 iff <*t*> is_firable_on M0 )

proof end;

theorem Th11: :: BOOLMARK:11

for PTN being Petri_net

for M0 being Boolean_marking of PTN

for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)

for M0 being Boolean_marking of PTN

for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0)

proof end;

theorem :: BOOLMARK:12

for PTN being Petri_net

for Sd being non empty Subset of the carrier of PTN holds

( Sd is Deadlock-like iff for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds

(Firing (Q,M0)) .: Sd = {FALSE} )

for Sd being non empty Subset of the carrier of PTN holds

( Sd is Deadlock-like iff for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds

for Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds

(Firing (Q,M0)) .: Sd = {FALSE} )

proof end;