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


begin

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
proofend;

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
proofend;

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
proofend;

begin

:: Boolean Markings of Place/Transition Net
definition
let PTN be PT_net_Str ;
func Bool_marks_of PTN ->  FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN  equals :: BOOLMARK:def 1
 Funcs ( the carrier of PTN,BOOLEAN);
correctness
coherence
Funcs ( the carrier of PTN,BOOLEAN) is FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN ;
;
end;

:: 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);

definition
let PTN be PT_net_Str ;
mode Boolean_marking of PTN is Element of Bool_marks_of PTN;
end;

:: Firable and Firing Conditions for Transitions
definition
let PTN be Petri_net;
let M0 be Boolean_marking of PTN;
let t be transition of PTN;
predt is_firable_on M0 means :Def2: :: BOOLMARK:def 2
M0 .: (*' {t}) c= {TRUE};
end;

:: deftheorem Def2 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} );

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;

definition
let PTN be Petri_net;
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) is Boolean_marking of PTN
proofend;
correctness
;
end;

:: 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);

:: 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;
predQ is_firable_on M0 means :Def4: :: BOOLMARK:def 4
( Q = {} or ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M &amp; Q /. 1 is_firable_on M0 &amp; M /. 1 = Firing ((Q /. 1),M0) &amp; ( for i being Element of NAT st i < len Q &amp; i > 0 holds
( Q /. (i + 1) is_firable_on M /. i &amp; M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) );
end;

:: deftheorem Def4 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 &amp; Q /. 1 is_firable_on M0 &amp; M /. 1 = Firing ((Q /. 1),M0) &amp; ( for i being Element of NAT st i < len Q &amp; i > 0 holds
( Q /. (i + 1) is_firable_on M /. i &amp; 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;

definition
let PTN be Petri_net;
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 &amp; it = M /. (len M) &amp; M /. 1 = Firing ((Q /. 1),M0) &amp; ( for i being Element of NAT st i < len Q &amp; 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 ) &amp; ( not Q = {} implies ex b1 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M &amp; b1 = M /. (len M) &amp; M /. 1 = Firing ((Q /. 1),M0) &amp; ( for i being Element of NAT st i < len Q &amp; i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) )
proofend;
uniqueness
 for b1, b2 being Boolean_marking of PTN holds
( ( Q = {} &amp; b1 = M0 &amp; b2 = M0 implies b1 = b2 ) &amp; ( not Q = {} &amp; ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M &amp; b1 = M /. (len M) &amp; M /. 1 = Firing ((Q /. 1),M0) &amp; ( for i being Element of NAT st i < len Q &amp; i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) &amp; ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M &amp; b2 = M /. (len M) &amp; M /. 1 = Firing ((Q /. 1),M0) &amp; ( for i being Element of NAT st i < len Q &amp; i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies b1 = b2 ) )
proofend;
correctness
consistency
for b1 being Boolean_marking of PTN holds verum;
;
end;

:: 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 b4 being Boolean_marking of PTN holds
( ( Q = {} implies ( b4 = Firing (Q,M0) iff b4 = M0 ) ) &amp; ( not Q = {} implies ( b4 = Firing (Q,M0) iff ex M being FinSequence of Bool_marks_of PTN st
( len Q = len M &amp; b4 = M /. (len M) &amp; M /. 1 = Firing ((Q /. 1),M0) &amp; ( for i being Element of NAT st i < len Q &amp; i > 0 holds
M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) );

theorem Th4: :: BOOLMARK:4
for A being non empty set
for y being set
for f being Function holds (f +* (A --> y)) .: A = {y}
proofend;

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
proofend;

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
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 &amp; 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 *' by PETRI:def_8;
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 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 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} &amp; ( 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 by Def2;
 M0 .: Sd = {FALSE} by Th4;
hence  contradiction by A5, A12, A10; ::_thesis: verum
end;

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} )
proofend;

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 &amp; i <= len Q0 holds
(Q0 ^ Q1) /. i = Q0 /. i
proofend;

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)))
proofend;

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) &amp; Q0 is_firable_on M0 )
proofend;

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 )
proofend;

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)
proofend;

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} )
proofend;