:: Basic Concepts for Petri Nets with Boolean Markings.Boolean Markings and the Firability/Firing of Transitions
:: by Pauline N. Kawamoto, Yasushi Fuwa and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem Th1: :: BOOLMARK:1
theorem Th2: :: BOOLMARK:2
theorem Th3: :: BOOLMARK:3
:: deftheorem defines Bool_marks_of BOOLMARK:def 1 :
:: deftheorem Def2 defines is_firable_on BOOLMARK:def 2 :
:: deftheorem defines Firing BOOLMARK:def 3 :
:: deftheorem Def4 defines is_firable_on BOOLMARK:def 4 :
definition
let PTN be
PT_net_Str ;
let M0 be
Boolean_marking of
PTN;
let Q be
FinSequence of the
Transitions 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
Element of
NAT st
i < len Q &
i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),
(M /. i) ) );
existence
( ( Q = {} implies ex b1 being Boolean_marking of PTN st b1 = M0 ) & ( not Q = {} implies ex b1 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & b1 = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Element of NAT st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) ) ) )
uniqueness
for b1, b2 being Boolean_marking of PTN holds
( ( Q = {} & b1 = M0 & b2 = M0 implies b1 = b2 ) & ( not Q = {} & ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M & b1 = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Element of 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 & b2 = M /. (len M) & M /. 1 = Firing (Q /. 1),M0 & ( for i being Element of NAT st i < len Q & i > 0 holds
M /. (i + 1) = Firing (Q /. (i + 1)),(M /. i) ) ) implies b1 = b2 ) )
correctness
consistency
for b1 being Boolean_marking of PTN holds verum;
;
end;
:: deftheorem Def5 defines Firing BOOLMARK:def 5 :
theorem :: BOOLMARK:4
canceled;
theorem Th5: :: BOOLMARK:5
theorem Th6: :: BOOLMARK:6
Lm1:
now
let PTN be
PT_net_Str ;
:: thesis: for Sd being non empty Subset of the Places 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
Places 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 Places of PTN --> TRUE ) +* (Sd --> FALSE );
A1:
[#] the
Places of
PTN = the
Places of
PTN
;
(
dom (the Places of PTN --> TRUE ) = the
Places of
PTN &
dom (Sd --> FALSE ) = Sd )
by FUNCOP_1:19;
then A2:
dom ((the Places of PTN --> TRUE ) +* (Sd --> FALSE )) =
the
Places of
PTN \/ Sd
by FUNCT_4:def 1
.=
the
Places of
PTN
by A1, SUBSET_1:28
;
A3:
rng ((the Places of PTN --> TRUE ) +* (Sd --> FALSE )) c= (rng (the Places of PTN --> TRUE )) \/ (rng (Sd --> FALSE ))
by FUNCT_4:18;
rng (Sd --> FALSE ) c= {FALSE }
by FUNCOP_1:19;
then A4:
rng (Sd --> FALSE ) c= BOOLEAN
by XBOOLE_1:1;
rng (the Places of PTN --> TRUE ) c= {TRUE }
by FUNCOP_1:19;
then
rng (the Places of PTN --> TRUE ) c= BOOLEAN
by XBOOLE_1:1;
then
(rng (the Places of PTN --> TRUE )) \/ (rng (Sd --> FALSE )) c= BOOLEAN
by A4, XBOOLE_1:8;
then
rng ((the Places of PTN --> TRUE ) +* (Sd --> FALSE )) c= BOOLEAN
by A3, XBOOLE_1:1;
then reconsider M0 =
(the Places 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: contradictionthen
not
*' Sd c= Sd *'
by PETRI:def 5;
then consider t being
transition of
PTN such that A6:
t in *' Sd
and A7:
not
t in Sd *'
by SUBSET_1:7;
{t} *' meets Sd
by A6, PETRI:20;
then consider s being
set 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 Th6;
s in Sd
by A8, XBOOLE_0:def 4;
then
TRUE in (Firing t,M0) .: Sd
by A9, FUNCT_2:43;
then A10:
(Firing t,M0) .: Sd <> {FALSE }
by TARSKI:def 1;
Sd misses *' {t}
by A7, PETRI:19;
then A11:
(the Places of PTN --> TRUE ) .: (*' {t}) = M0 .: (*' {t})
by Th3;
(
rng (the Places of PTN --> TRUE ) c= {TRUE } &
(the Places of PTN --> TRUE ) .: (*' {t}) c= rng (the Places of PTN --> TRUE ) )
by FUNCOP_1:19, RELAT_1:144;
then
M0 .: (*' {t}) c= {TRUE }
by A11, XBOOLE_1:1;
then A12:
t is_firable_on M0
by Def2;
M0 .: Sd = {FALSE }
by Th5;
hence
contradiction
by A5, A12, A10;
:: thesis: verum
end;
theorem :: BOOLMARK:7
theorem Th8: :: BOOLMARK:8
theorem :: BOOLMARK:9
canceled;
theorem Th10: :: BOOLMARK:10
theorem Th11: :: BOOLMARK:11
theorem Th12: :: BOOLMARK:12
theorem Th13: :: BOOLMARK:13
theorem :: BOOLMARK:14