:: 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-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FUNCT_1, SUBSET_1, FUNCT_4, FUNCOP_1, RELAT_1,
TARSKI, PETRI, FUNCT_2, MARGREL1, ARYTM_3, XBOOLEAN, FINSEQ_1, PARTFUN1,
XXREAL_0, CARD_1, ORDINAL4, NAT_1, ARYTM_1, BOOLMARK, STRUCT_0, PNPROC_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, FINSEQ_1,
FUNCT_4, MARGREL1, PETRI, XXREAL_0, STRUCT_0;
constructors DOMAIN_1, FUNCT_4, XREAL_0, NAT_1, MARGREL1, PETRI, FUNCOP_1,
RELSET_1, NUMBERS;
registrations XXREAL_0, XREAL_0, FINSEQ_1, MARGREL1, ORDINAL1, CARD_1,
RELSET_1, STRUCT_0;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions PETRI, XBOOLE_0;
equalities XBOOLE_0, XBOOLEAN, SUBSET_1;
expansions PETRI;
theorems SUBSET_1, TARSKI, ZFMISC_1, PETRI, FUNCT_1, FUNCOP_1, FUNCT_2,
FUNCT_4, FINSEQ_1, FINSEQ_4, NAT_1, FINSEQ_2, FINSEQ_3, RELAT_1,
RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1,
SEQ_4;
schemes FINSEQ_2, NAT_1;
begin
theorem Th1:
for A, B being non empty set, f being Function of A,B, C being
Subset of A, v being Element of B holds f +* (C-->v) is Function of A,B
proof
let A, B be non empty set;
let f be Function of A,B;
let C be Subset of A;
let v be Element of B;
A1: dom f = A by FUNCT_2:def 1;
rng f c= B & rng(C-->v) c= {v} by FUNCOP_1:13,RELAT_1:def 19;
then
A2: rng f \/ rng(C-->v) c= B \/ {v} by XBOOLE_1:13;
rng(f +* (C-->v)) c= rng f \/ rng(C-->v) by FUNCT_4:17;
then rng(f +* (C-->v)) c= B \/ {v} by A2,XBOOLE_1:1;
then
A3: rng(f +* (C-->v)) c= B by ZFMISC_1:40;
dom(f +* (C-->v)) = (dom f) \/ dom(C-->v) by FUNCT_4:def 1
.= [#]A \/ C by A1,FUNCOP_1:13
.= A by SUBSET_1:11;
hence thesis by A3,FUNCT_2:def 1,RELSET_1:4;
end;
theorem Th2:
for X, Y being non empty set, A, B being Subset of X, f being
Function of X,Y st f.:A misses f.:B holds A misses B
proof
let X, Y be non empty set;
let A, B be Subset of X;
let f be Function of X,Y such that
A1: f.:A /\ f.:B = {};
assume A /\ B <> {};
then consider x being Element of X such that
A2: x in A /\ B by SUBSET_1:4;
x in B by A2,XBOOLE_0:def 4;
then
A3: f.x in f.:B by FUNCT_2:35;
x in A by A2,XBOOLE_0:def 4;
then f.x in f.:A by FUNCT_2:35;
hence contradiction by A1,A3,XBOOLE_0:def 4;
end;
theorem Th3:
for A, B being set, f being Function, x being set holds A misses
B implies (f +* (A --> x)).:B = f.:B
proof
let A, B be set, f be Function, x be set;
assume that
A1: A /\ B = {} and
A2: (f +* (A --> x)).:B <> f.:B;
A3: dom(f +* (A --> x)) = dom f \/ dom(A --> x) by FUNCT_4:def 1;
A4: dom(A --> x) = A by FUNCOP_1:13;
A5: not (for y being object holds y in (f +* (A --> x)).:B iff y in f.:B)
by A2,TARSKI:2;
now
per cases by A5;
case
ex y being set st y in (f +* (A --> x)).:B & not y in f.:B;
then consider y being set such that
A6: y in (f +* (A --> x)).:B and
A7: not y in f.:B;
consider z being object such that
A8: z in dom(f +* (A --> x)) and
A9: z in B and
A10: y = (f +* (A --> x)).z by A6,FUNCT_1:def 6;
not z in A by A1,A9,XBOOLE_0:def 4;
then z in dom f & y = f.z by A3,A4,A8,A10,FUNCT_4:11,XBOOLE_0:def 3;
hence contradiction by A7,A9,FUNCT_1:def 6;
end;
case
ex y being set st not y in (f +* (A --> x)).:B & y in f.:B;
then consider y being set such that
A11: not y in (f +* (A --> x)).:B and
A12: y in f.:B;
consider z being object such that
A13: z in dom f and
A14: z in B and
A15: y = f.z by A12,FUNCT_1:def 6;
not z in A by A1,A14,XBOOLE_0:def 4;
then
A16: y = (f +* (A --> x)).z by A4,A15,FUNCT_4:11;
z in dom(f +* (A --> x)) by A3,A13,XBOOLE_0:def 3;
hence contradiction by A11,A14,A16,FUNCT_1:def 6;
end;
end;
hence thesis;
end;
:: Main definitions, theorems block
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
Funcs(the carrier of PTN, BOOLEAN);
correctness;
end;
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;
pred t is_firable_on M0 means
M0.:*'{t} c= {TRUE};
end;
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
M0 +* (*'{t}-->FALSE) +*
({t}*'-->TRUE);
coherence
proof
set M1 = M0 +* (*'{t}-->FALSE) +* ({t}*'-->TRUE);
M0 +* (*'{t}-->FALSE) is Function of the carrier of PTN, BOOLEAN by Th1;
then M1 is Function of the carrier of PTN, BOOLEAN by Th1;
hence thesis by FUNCT_2:8;
end;
correctness;
end;
:: 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;
pred Q is_firable_on M0 means
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);
end;
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:
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
proof
defpred P2[Nat] means for Q being FinSequence of the
carrier' of PTN st $1 = len Q holds (Q = {} implies ex M1 being
Boolean_marking of PTN st M1 = M0) & (Q <> {} implies ex M2 being
Boolean_marking of PTN st ex M being FinSequence of Bool_marks_of PTN st len Q
= len M & M2 = 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));
A1: now
let n be Nat;
assume
A2: P2[n];
thus P2[n+1]
proof
let Q be FinSequence of the carrier' of PTN such that
A3: n+1=len Q;
thus Q = {} implies ex M1 being Boolean_marking of PTN st M1 = M0;
thus Q <> {} implies ex M2 being Boolean_marking of PTN, M being
FinSequence of Bool_marks_of PTN st len Q = len M & M2 = 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)
proof
assume Q <> {};
then len Q<>0;
then consider
Q1 being FinSequence of the carrier' of PTN, t being
transition of PTN such that
A4: Q=Q1^<*t*> by FINSEQ_2:19;
A5: n+1=len Q1+ 1 by A3,A4,FINSEQ_2:16;
per cases;
suppose
A6: Q1={};
take M2 = Firing(t,M0);
take M = <*M2*>;
A7: len Q = len Q1 + len <*t*> by A4,FINSEQ_1:22
.= 0 + len <*t*> by A6
.= 0 + 1 by FINSEQ_1:39;
hence len Q = len M by FINSEQ_1:39;
hence M2 = M/.len M by A7,FINSEQ_4:16;
Q = <*t*> by A4,A6,FINSEQ_1:34;
then Q/.1 = t by FINSEQ_4:16;
hence M/.1 = Firing(Q/.1,M0) by FINSEQ_4:16;
let i be Nat;
assume i < len Q & i > 0;
hence thesis by A7,NAT_1:13;
end;
suppose
A8: Q1<> {};
then
A9: len Q1 > 0 by NAT_1:3;
then 0 + 1 < len Q1 + 1 by XREAL_1:6;
then 1<= len Q1 by NAT_1:13;
then
A10: 1 in dom Q1 by FINSEQ_3:25;
A11: len Q = len Q1 + len<*t*> by A4,FINSEQ_1:22
.=len Q1 + 1 by FINSEQ_1:40;
consider B2 being Boolean_marking of PTN, B being FinSequence of
Bool_marks_of PTN such that
A12: len Q1 = len B and
A13: B2 = B/.len B and
A14: B/.1 = Firing(Q1/.1,M0) and
A15: for i being Nat st i < len Q1 & i > 0 holds B
/.(i+1) = Firing(Q1/.(i+1),B/.i) by A2,A5,A8;
take M2 = Firing(t,B2);
take M = B^<*M2*>;
A16: len M =len B + len<*M2*> by FINSEQ_1:22
.=len B + 1 by FINSEQ_1:40;
hence len Q = len M by A12,A11;
thus M2 = M/.len M by A16,FINSEQ_4:67;
0 + 1 < len B + 1 by A12,A9,XREAL_1:6;
then
A17: 1<= len B by NAT_1:13;
then 1 in dom B by FINSEQ_3:25;
hence M/.1 = B/.1 by FINSEQ_4:68
.= Firing(Q/.1,M0) by A4,A14,A10,FINSEQ_4:68;
let i be Nat such that
A18: i < len Q and
A19: i > 0;
thus M/.(i+1) = Firing(Q/.(i+1),M/.i)
proof
1<=i+1 & i+1<=len Q1+1 by A11,A18,NAT_1:12,13;
then
A20: Seg (len Q1 + 1) = Seg (len Q1) \/ {len Q1 + 1} & i+1 in
Seg (len Q1 + 1) by FINSEQ_1:1,9;
per cases by A20,XBOOLE_0:def 3;
suppose
A21: i+1 in Seg (len Q1);
then i + 1 <= len B by A12,FINSEQ_1:1;
then i + 1 <= len B + 1 by NAT_1:12;
then
A22: i <= len B by XREAL_1:6;
0 + 1 < i + 1 by A19,XREAL_1:6;
then 1<=i by NAT_1:13;
then
A23: i in dom B by A22,FINSEQ_3:25;
i + 1 <= len Q1 by A21,FINSEQ_1:1;
then i < len Q1 by NAT_1:13;
then
A24: B/.(i+1) = Firing(Q1/.(i+1),B/.i) by A15,A19;
i+1 in dom Q1 by A21,FINSEQ_1:def 3;
then
A25: Q1/.(i+1)=Q/.(i+1) by A4,FINSEQ_4:68;
i+1 in dom B by A12,A21,FINSEQ_1:def 3;
then B/.(i+1)=M/.(i+1) by FINSEQ_4:68;
hence thesis by A24,A25,A23,FINSEQ_4:68;
end;
suppose
A26: i+1 in {len Q1 + 1};
A27: len B in dom B by A17,FINSEQ_3:25;
A28: i + 1 = len Q1 + 1 by A26,TARSKI:def 1;
then M/.(i+1)=M2 & Q/.(i+1)=t by A4,A12,FINSEQ_4:67;
hence thesis by A12,A13,A28,A27,FINSEQ_4:68;
end;
end;
end;
end;
end;
end;
A29: P2[0];
for n being Nat holds P2[n] from NAT_1:sch 2(A29,A1);
hence thesis;
end;
uniqueness
proof
let B1,B2 be Boolean_marking of PTN;
thus Q = {} & B1 = M0 & B2 = M0 implies B1 = B2;
assume Q <> {};
given M1 being FinSequence of Bool_marks_of PTN such that
A30: len Q = len M1 and
A31: B1 = M1/.len M1 and
A32: M1/.1 = Firing(Q/.1,M0) and
A33: for i being Nat st i < len Q & i > 0 holds M1/.(i+1) =
Firing(Q/.(i+1),M1/.i);
A34: dom M1 = Seg len Q by A30,FINSEQ_1:def 3;
given M2 being FinSequence of Bool_marks_of PTN such that
A35: len Q = len M2 and
A36: B2 = M2/.len M2 and
A37: M2/.1 = Firing(Q/.1,M0) and
A38: for i being Nat st i < len Q & i > 0 holds M2/.(i+1) =
Firing(Q/.(i+1),M2/.i);
defpred P2[Nat] means $1 in Seg len Q implies M1/.$1 = M2/.$1;
A39: now
let j be Nat;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
assume
A40: P2[j];
now
assume
A41: j + 1 in Seg len Q;
per cases;
suppose
j = 0;
hence M1/.(j+1) = M2/.(j+1) by A32,A37;
end;
suppose
A42: j <> 0;
then
A43: j > 0 by NAT_1:3;
j + 1 <= len Q & j < j + 1 by A41,FINSEQ_1:1,XREAL_1:29;
then
A44: j < len Q by XXREAL_0:2;
1 <= j by A42,NAT_1:14;
hence M1/.(j+1) = Firing(Q/.(jj+1),M2/.jj) by A33,A40,A44,FINSEQ_1:1
.= M2/.(j+1) by A38,A43,A44;
end;
end;
hence P2[j+1];
end;
A45: P2[0] by FINSEQ_1:1;
A46: for j being Nat holds P2[j] from NAT_1:sch 2(A45,A39);
now
let j be Nat;
assume
A47: j in dom M1;
then
A48: j in dom M2 by A35,A34,FINSEQ_1:def 3;
thus M1.j = M1/.j by A47,PARTFUN1:def 6
.= M2/.j by A46,A34,A47
.= M2.j by A48,PARTFUN1:def 6;
end;
hence B1 = B2 by A30,A31,A35,A36,FINSEQ_2:9;
end;
correctness;
end;
theorem Th4:
for A being non empty set, y being set, f being Function holds (f
+*(A --> y)).:A = {y}
proof
let A be non empty set, y be set, f be Function;
now
let u be object;
thus u in (f+*(A --> y)).:A implies u = y
proof
assume u in (f+*(A --> y)).:A;
then consider z being object such that
z in dom(f+*(A --> y)) and
A1: z in A and
A2: u = (f+*(A --> y)).z by FUNCT_1:def 6;
z in dom(A --> y) by A1,FUNCOP_1:13;
then u = (A --> y).z by A2,FUNCT_4:13;
hence thesis by A1,FUNCOP_1:7;
end;
consider x being object such that
A3: x in A by XBOOLE_0:def 1;
A4: x in dom(A --> y) by A3,FUNCOP_1:13;
then
A5: x in dom(f+*(A --> y)) by FUNCT_4:12;
(A --> y).x = y by A3,FUNCOP_1:7;
then y = (f+*(A --> y)).x by A4,FUNCT_4:13;
hence u = y implies u in (f+*(A --> y)).:A by A3,A5,FUNCT_1:def 6;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th5:
for PTN being Petri_net, M0 being Boolean_marking of PTN, t
being transition of PTN, s being place of PTN st s in {t}*' holds Firing(t,M0).
s = TRUE
proof
let PTN be Petri_net, M0 be Boolean_marking of PTN, t be transition of PTN,
s be place of PTN;
set M = M0 +* (*'{t}-->FALSE) +* ({t}*'-->TRUE);
A1: [#]the carrier of PTN = the carrier of PTN;
A2: dom M0 = the carrier of PTN & dom (*'{t}-->FALSE) = (*'{t})
by FUNCT_2:def 1;
dom ({t}*'-->TRUE) = ({t}*') by FUNCT_2:def 1;
then
A3: dom M = dom(M0 +* (*'{t}-->FALSE)) \/ {t}*' by FUNCT_4:def 1
.= (the carrier of PTN) \/ (*'{t}) \/ ({t}*') by A2,FUNCT_4:def 1
.= (the carrier of PTN) \/ ((*'{t}) \/ ({t}*')) by XBOOLE_1:4
.= the carrier of PTN by A1,SUBSET_1:11;
assume
A4: s in {t}*';
then ((M0 +* (*'{t}-->FALSE)) +* ({t}*'-->TRUE)).:({t}*') = {TRUE} by Th4;
then M.s in {TRUE} by A4,A3,FUNCT_1:def 6;
hence thesis by TARSKI:def 1;
end;
Lm1: now
let PTN be Petri_net;
let Sd be non empty Subset of the carrier of PTN;
set M0 = ((the carrier of PTN)-->TRUE qua Function) +* (Sd-->FALSE);
A1: [#]the carrier of PTN = the carrier of PTN;
dom ((the carrier of PTN)-->TRUE qua Function) = the carrier of PTN & dom
(Sd -->FALSE) = Sd by FUNCOP_1:13;
then
A2: dom M0 = (the carrier of PTN) \/ Sd by FUNCT_4:def 1
.= the carrier of PTN by A1,SUBSET_1:11;
A3: rng M0 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 M0 c= BOOLEAN by A3,XBOOLE_1:1;
then reconsider M0 as Boolean_marking of PTN by A2,FUNCT_2:def 2;
assume
A5: for M0 being Boolean_marking of PTN st M0.:Sd = {FALSE} for t being
transition of PTN st t is_firable_on M0 holds Firing(t,M0).:Sd = {FALSE};
assume Sd is not Deadlock-like;
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 qua Function).:*'{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 qua set} by Th4;
hence contradiction by A5,A12,A10;
end;
theorem
for PTN being Petri_net, 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} for t being transition of PTN st t is_firable_on M0 holds Firing(t,M0
).:Sd = {FALSE}
proof
let PTN be Petri_net, Sd be non empty Subset of the carrier of PTN;
thus Sd is Deadlock-like implies for M0 being Boolean_marking of PTN st M0.:
Sd = {FALSE} for t being transition of PTN st t is_firable_on M0 holds Firing(t
,M0).:Sd = {FALSE}
proof
assume Sd is Deadlock-like;
then
A1: *'Sd is Subset of Sd*';
let M0 be Boolean_marking of PTN such that
A2: M0.:Sd = {FALSE};
let t be transition of PTN;
assume t is_firable_on M0;
then M0.:*'{t} c= {TRUE};
then
A3: M0.:*'{t} misses {FALSE} by XBOOLE_1:63,ZFMISC_1:11;
then *'{t} misses Sd by A2,Th2;
then not t in *'Sd by A1,PETRI:19;
then {t}*' misses Sd by PETRI:20;
hence Firing(t,M0).:Sd = (M0 +* (*'{t}-->FALSE)).:Sd by Th3
.= {FALSE} by A2,A3,Th2,Th3;
end;
thus thesis by Lm1;
end;
theorem Th7:
for D being non empty set for Q0,Q1 being FinSequence of D, i
being Element of NAT st 1<=i & i<=len Q0 holds (Q0^Q1)/.i=Q0/.i
proof
let D be non empty set;
let Q0,Q1 be FinSequence of D, i be Element of NAT;
len Q0<=len Q0+len Q1 by NAT_1:11;
then
A1: i<=len Q0 implies i<=len Q0 + len Q1 by XXREAL_0:2;
i in dom Q0 implies i in Seg(len Q0) by FINSEQ_1:def 3;
then i in dom Q0 implies 1<=i & i<=len(Q0^Q1) by A1,FINSEQ_1:1,22;
then
A2: i in dom Q0 implies i in dom (Q0^Q1) by FINSEQ_3:25;
i in dom Q0 implies Q0.i=Q0/.i by PARTFUN1:def 6;
then
A3: i in dom Q0 implies (Q0^Q1).i=Q0/.i by FINSEQ_1:def 7;
i in dom Q0 iff i in Seg len Q0 by FINSEQ_1:def 3;
hence thesis by A2,A3,FINSEQ_1:1,PARTFUN1:def 6;
end;
theorem Th8:
for PTN being Petri_net, M0 being Boolean_marking of PTN, Q0,
Q1 being FinSequence of the carrier' of PTN holds Firing(Q0^Q1,M0) = Firing(
Q1,Firing(Q0,M0))
proof
let PTN be Petri_net;
let M0 be Boolean_marking of PTN;
let Q0, Q1 be FinSequence of the carrier' of PTN;
now
per cases;
case
A1: Q0 = {} & Q1 = {};
then
A2: Q0^Q1 = {} by FINSEQ_1:34;
Firing(Q1,Firing(Q0,M0)) = Firing(Q1,M0) by A1,Def5
.= M0 by A1,Def5;
hence thesis by A2,Def5;
end;
case
A3: Q0 = {} & Q1 <> {};
then Firing(Q0^Q1,M0) = Firing(Q1,M0) by FINSEQ_1:34;
hence thesis by A3,Def5;
end;
case
A4: Q0 <> {} & Q1 = {};
then Firing(Q0^Q1,M0) = Firing(Q0,M0) by FINSEQ_1:34;
hence thesis by A4,Def5;
end;
case
A5: Q0 <> {} & Q1 <> {};
then consider M3 being FinSequence of Bool_marks_of PTN such that
A6: len Q0 = len M3 & Firing(Q0,M0) = M3/.len M3 and
A7: M3/.1 = Firing(Q0/.1,M0) and
A8: for i being Nat st i < len Q0 & i > 0 holds M3/.(i+1
) = Firing(Q0/.(i+1),M3/.i) by Def5;
consider M being FinSequence of Bool_marks_of PTN such that
A9: len (Q0^Q1) = len M and
A10: Firing(Q0^Q1,M0) = M/.len M and
A11: M/.1 = Firing((Q0^Q1)/.1,M0) and
A12: for i being Nat st i < len (Q0^Q1) & i > 0 holds M/.
(i+1) = Firing((Q0^Q1)/.(i+1),M/.i) by A5,Def5;
defpred P2[Nat] means 1+$1<=len Q0 implies M/.(1+$1)=M3/.(1+$1);
0<len Q1 by A5,NAT_1:3;
then 0+len Q0<len Q0 + len Q1 by XREAL_1:6;
then
A13: len Q0<len (Q0^Q1) by FINSEQ_1:22;
A14: now
let k be Nat;
A15: 0<=k by NAT_1:2;
assume
A16: P2[k];
now
assume
A17: 1+(k+1)<=len Q0;
then
A18: (Q0^Q1)/.(1+(k+1))=Q0/.(1+(k+1)) by Th7,NAT_1:11;
A19: 1+k<len Q0 by A17,NAT_1:13;
then 1+k<len (Q0^Q1) by A13,XXREAL_0:2;
then M/.(1+(k+1)) = Firing(Q0/.(1+(k+1)),M3/.(1+k)) by A12,A15,A16
,A17,A18,NAT_1:13;
hence M/.(1+(k+1)) = M3/.(1+(k+1)) by A8,A15,A19;
end;
hence P2[k+1];
end;
reconsider m = len Q0 - 1 as Element of NAT by A5,NAT_1:3,20;
let i be Element of NAT;
len Q1 > 0 by A5,NAT_1:3;
then
A20: 0+1<=len Q1 by NAT_1:13;
consider M4 being FinSequence of Bool_marks_of PTN such that
A21: len Q1 = len M4 and
A22: Firing(Q1,Firing(Q0,M0)) = M4/.len M4 and
A23: M4/.1 = Firing(Q1/.1,Firing(Q0,M0)) and
A24: for i being Nat st i < len Q1 & i > 0 holds M4/.(i+1
) = Firing(Q1/.(i+1),M4/.i) by A5,Def5;
consider k being Nat such that
A25: len M4 = k + 1 by A5,A21,NAT_1:6;
A26: P2[0] by A11,A7,Th7;
A27: for k being Nat holds P2[k] from NAT_1:sch 2(A26,A14);
defpred P2[Nat] means 1+$1<=len Q1 implies M/.(len Q0+1+$1)=
M4/.(1+$1);
A28: now
let k be Nat;
assume
A29: P2[k];
0<=k + len Q0 by NAT_1:2;
then
A30: len Q0 + 1+k+1 = len Q0 + 1 + (k+1) & 0<len Q0 + k + 1;
A31: 0<=k by NAT_1:2;
now
assume
A32: 1+(k+1)<=len Q1;
then
A33: (Q0^Q1)/.(len Q0+(1+(k+1)))=Q1/.(1+(k+1)) by NAT_1:11,SEQ_4:136;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
A34: 1+k<len Q1 by A32,NAT_1:13;
then len Q0+(1+k) < len Q0+ len Q1 by XREAL_1:6;
then len Q0+1+kk < len (Q0^Q1) by FINSEQ_1:22;
then M/.(len Q0+1+(kk+1)) = Firing(Q1/.(1+(kk+1)),M4/.(1+kk))
by A12,A30
,A29,A32,A33,NAT_1:13;
hence M/.(len Q0+1+(k+1)) = M4/.(1+(k+1)) by A24,A31,A34;
end;
hence P2[k+1];
end;
len Q0 > 0 by A5,NAT_1:3;
then M/.(len Q0+1+0)= Firing((Q0^Q1)/.(len Q0+1),M/.(1+m)) by A12,A13
.=Firing((Q0^Q1)/.(len Q0+1),Firing(Q0,M0)) by A6,A27
.=M4/.(1+0) by A23,A20,SEQ_4:136;
then
A35: P2[0];
A36: for k being Nat holds P2[k] from NAT_1:sch 2(A35,A28);
reconsider k as Element of NAT by ORDINAL1:def 12;
M/.len M = M/.(len Q0 +(1+k)) by A9,A21,A25,FINSEQ_1:22
.= M/.(len Q0 +1+k)
.= M4/.len M4 by A21,A36,A25;
hence thesis by A10,A22;
end;
end;
hence thesis;
end;
theorem Th9:
for PTN being Petri_net, M0 being Boolean_marking of PTN, 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
let PTN be Petri_net;
let M0 be Boolean_marking of PTN;
let Q0, Q1 be FinSequence of the carrier' of PTN;
assume
A1: Q0^Q1 is_firable_on M0;
now
per cases;
case
Q0 = {} & Q1 = {};
hence thesis;
end;
case
A2: Q0 = {} & Q1 <> {};
hence Q0 is_firable_on M0;
Q0^Q1 = Q1 by A2,FINSEQ_1:34;
hence Q1 is_firable_on Firing(Q0,M0) by A1,A2,Def5;
end;
case
A3: Q0 <> {} & Q1 = {};
hence Q1 is_firable_on Firing(Q0,M0);
thus Q0 is_firable_on M0 by A1,A3,FINSEQ_1:34;
end;
case
A4: Q0 <> {} & Q1 <> {};
let i be Element of NAT;
len Q1 > 0 by A4,NAT_1:3;
then
A5: 0+1<=len Q1 by NAT_1:13;
then
A6: Q1/.1 = (Q0^Q1)/.(len Q0 + 1) by SEQ_4:136;
reconsider m = len Q0 - 1 as Element of NAT by A4,NAT_1:3,20;
consider M4 being FinSequence of Bool_marks_of PTN such that
A7: len Q1 = len M4 and
Firing(Q1,Firing(Q0,M0)) = M4/.len M4 and
A8: M4/.1 = Firing(Q1/.1,Firing(Q0,M0)) and
A9: for i being Nat st i < len Q1 & i > 0 holds M4/.(i+1
) = Firing(Q1/.(i+1),M4/.i) by A4,Def5;
consider M3 being FinSequence of Bool_marks_of PTN such that
A10: len Q0 = len M3 and
A11: Firing(Q0,M0) = M3/.len M3 and
A12: M3/.1 = Firing(Q0/.1,M0) and
A13: for i being Nat st i < len Q0 & i > 0 holds M3/.(i+1
) = Firing(Q0/.(i+1),M3/.i) by A4,Def5;
consider j being Nat such that
A14: len M3 = j + 1 by A4,A10,NAT_1:6;
reconsider j as Element of NAT by ORDINAL1:def 12;
consider M being FinSequence of Bool_marks_of PTN such that
len (Q0^Q1) = len M and
A15: (Q0^Q1)/.1 is_firable_on M0 and
A16: M/.1 = Firing((Q0^Q1)/.1,M0) and
A17: for i being Element of NAT st i < len (Q0^Q1) & i > 0 holds (Q0
^Q1)/.(i+1) is_firable_on M/.i & M/.(i+1) = Firing((Q0^Q1)/.(i+1),M/.i) by A1
,A4;
defpred P2[Nat] means 1+$1<=len Q0 implies M/.(1+$1)=M3/.(1+
$1);
0<len Q1 by A4,NAT_1:3;
then 0+len Q0<len Q0 + len Q1 by XREAL_1:6;
then
A18: len Q0<len (Q0^Q1) by FINSEQ_1:22;
A19: now
let k be Nat;
A20: 0<=k by NAT_1:2;
assume
A21: P2[k];
now
assume
A22: 1+(k+1)<=len Q0;
then
A23: (Q0^Q1)/.(1+(k+1))=Q0/.(1+(k+1)) by Th7,NAT_1:11;
A24: 1+k<len Q0 by A22,NAT_1:13;
then 1+k<len (Q0^Q1) by A18,XXREAL_0:2;
then M/.(1+(k+1)) = Firing(Q0/.(1+(k+1)),M3/.(1+k)) by A17,A20,A21
,A22,A23,NAT_1:13;
hence M/.(1+(k+1)) = M3/.(1+(k+1)) by A13,A20,A24;
end;
hence P2[k+1];
end;
A25: P2[0] by A16,A12,Th7;
A26: for k being Nat holds P2[k] from NAT_1:sch 2(A25,A19);
A27: now
let i be Element of NAT;
assume that
A28: i < len Q0 and
A29: i > 0;
consider j being Nat such that
A30: i = j + 1 by A29,NAT_1:6;
i + 1 >= 1 & i + 1 <= len Q0 by A28,NAT_1:11,13;
then i + 1 in dom Q0 by FINSEQ_3:25;
then
A31: (Q0^Q1)/.(i+1) = Q0/.(i+1) by FINSEQ_4:68;
reconsider j as Element of NAT by ORDINAL1:def 12;
i = j+1 by A30;
then
A32: M/.i = M3/.i by A26,A28;
A33: i + 1 <= len Q0 by A28,NAT_1:13;
A34: i < len (Q0^Q1) by A18,A28,XXREAL_0:2;
then M/.(i+1) = Firing((Q0^Q1)/.(i+1),M/.i) by A17,A29;
hence
Q0/.(i+1) is_firable_on M3/.i & M3/.(i+1) = Firing(Q0/.(i+1),M3/.
i) by A17,A26,A29,A34,A31,A32,A33;
end;
defpred P2[Nat] means 1+$1<=len Q1 implies M/.(len Q0+1+$1)=
M4/.(1+$1);
A35: now
let k be Nat;
assume
A36: P2[k];
0<=k + len Q0 by NAT_1:2;
then
A37: len Q0 + 1+k+1 = len Q0 + 1 + (k+1) & 0<len Q0 + k + 1;
A38: 0<=k by NAT_1:2;
now
assume
A39: 1+(k+1)<=len Q1;
then
A40: (Q0^Q1)/.(len Q0+(1+(k+1)))=Q1/.(1+(k+1)) by NAT_1:11,SEQ_4:136;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
A41: 1+k<len Q1 by A39,NAT_1:13;
then len Q0+(1+k) < len Q0+ len Q1 by XREAL_1:6;
then len Q0+1+kk < len (Q0^Q1) by FINSEQ_1:22;
then M/.(len Q0+1+(kk+1)) = Firing(Q1/.(1+(kk+1)),M4/.(1+kk))
by A17,A37
,A36,A39,A40,NAT_1:13;
hence M/.(len Q0+1+(k+1)) = M4/.(1+(k+1)) by A9,A38,A41;
end;
hence P2[k+1];
end;
A42: len Q0 > 0 by A4,NAT_1:3;
then M/.(len Q0+1+0)= Firing((Q0^Q1)/.(len Q0+1),M/.(1+m)) by A17,A18
.=Firing((Q0^Q1)/.(len Q0+1),Firing(Q0,M0)) by A10,A11,A26
.=M4/.(1+0) by A8,A5,SEQ_4:136;
then
A43: P2[0];
A44: for k being Nat holds P2[k] from NAT_1:sch 2(A43,A35);
A45: now
let i be Element of NAT such that
A46: i < len Q1 and
A47: i > 0;
consider j being Nat such that
A48: i = j + 1 by A47,NAT_1:6;
reconsider j as Element of NAT by ORDINAL1:def 12;
len Q0 + 1 + j = len Q0 + (j + 1);
then
A49: M/.(len Q0 + i) = M4/.i by A44,A46,A48;
i + 1 >= 1 & i + 1 <= len Q1 by A46,NAT_1:11,13;
then
A50: i + 1 in dom Q1 by FINSEQ_3:25;
A51: (Q0^Q1)/.(len Q0+i+1) = (Q0^Q1)/.(len Q0+(i+1))
.= Q1/.(i+1) by A50,FINSEQ_4:69;
A52: len Q0 + 1 + i = len Q0 + i + 1 & i + 1 <= len Q1 by A46,NAT_1:13;
len (Q0^Q1) = len Q0 + len Q1 by FINSEQ_1:22;
then
A53: len Q0 + i < len (Q0^Q1) by A46,XREAL_1:6;
A54: i < len Q0 + i by A4,NAT_1:3,XREAL_1:29;
then M/.(len Q0+i+1) = Firing((Q0^Q1)/.(len Q0+i+1),M/.(len Q0+i)) by
A17,A47,A53;
hence
Q1/.(i+1) is_firable_on M4/.i & M4/.(i+1) = Firing(Q1/.(i+1),M4/.
i) by A17,A44,A47,A53,A54,A51,A49,A52;
end;
len M3 = j + 1 by A14;
then M/.len M3 = M3/.len M3 by A10,A26;
then Q1/.1 is_firable_on M3/.len M3 by A17,A10,A42,A18,A6;
hence Q1 is_firable_on Firing(Q0,M0) by A11,A7,A8,A45;
0+1<=len Q0 by A42,NAT_1:13;
then Q0/.1 is_firable_on M0 by A15,Th7;
hence Q0 is_firable_on M0 by A10,A12,A27;
end;
end;
hence thesis;
end;
theorem Th10:
for PTN being Petri_net, M0 being Boolean_marking of PTN, t
being transition of PTN holds t is_firable_on M0 iff <*t*> is_firable_on M0
proof
let PTN be Petri_net, M0 be Boolean_marking of PTN, t be transition of PTN;
hereby
set M = <*Firing(<*t*>/.1,M0)*>;
A1: M/.1 = Firing(<*t*>/.1,M0) by FINSEQ_4:16;
A2: now
A3: len <*t*> = 0 + 1 by FINSEQ_1:39;
let i be Element of NAT;
assume i < len <*t*> & i > 0;
hence <*t*>/.(i+1) is_firable_on M/.i & M/.(i+1) = Firing(<*t*>/.(i+1),M
/.i) by A3,NAT_1:13;
end;
assume t is_firable_on M0;
then
A4: <*t*>/.1 is_firable_on M0 by FINSEQ_4:16;
len <*t*> = 1 by FINSEQ_1:39
.= len M by FINSEQ_1:39;
hence <*t*> is_firable_on M0 by A4,A1,A2;
end;
assume <*t*> is_firable_on M0;
then
ex M being FinSequence of Bool_marks_of PTN st len <*t*> = len M & <*t*>
/.1 is_firable_on M0 & M/.1 = Firing(<*t*>/.1,M0) & for i being Element of NAT
st i < len <*t*> & i > 0 holds <*t*>/.(i +1) is_firable_on M/.i & M/.(i+1) =
Firing(<*t*>/.(i+1),M/.i);
hence thesis by FINSEQ_4:16;
end;
theorem Th11:
for PTN being Petri_net, M0 being Boolean_marking of PTN, t
being transition of PTN holds Firing(t,M0) = Firing(<*t*>,M0)
proof
let PTN be Petri_net, M0 be Boolean_marking of PTN, t be transition of PTN;
set M = <*Firing(<*t*>/.1,M0)*>;
A1: len <*t*> = 1 & <*t*>/.1 = t by FINSEQ_1:39,FINSEQ_4:16;
A2: M/.1 = Firing(<*t*>/.1,M0) by FINSEQ_4:16;
A3: now
A4: len <*t*> = 0 + 1 by FINSEQ_1:39;
let i be Nat;
assume i < len <*t*> & i > 0;
hence M/.(i+1) = Firing(<*t*>/.(i+1),M/.i) by A4,NAT_1:13;
end;
len <*t*> = 1 by FINSEQ_1:39
.= len M by FINSEQ_1:39;
hence thesis by A1,A2,A3,Def5;
end;
theorem
for PTN being Petri_net, 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} for Q being FinSequence of the carrier' of PTN st Q is_firable_on
M0 holds Firing(Q,M0).:Sd = {FALSE}
proof
let PTN be Petri_net, Sd be non empty Subset of the carrier of PTN;
set M0 = ((the carrier of PTN)-->TRUE qua Function) +* (Sd-->FALSE);
A1: [#]the carrier of PTN = the carrier of PTN;
dom ((the carrier of PTN)-->TRUE qua Function) = the carrier of PTN & dom
(Sd -->FALSE) = Sd by FUNCOP_1:13;
then
A2: dom M0 = (the carrier of PTN) \/ Sd by FUNCT_4:def 1
.= the carrier of PTN by A1,SUBSET_1:11;
rng (Sd-->FALSE) c= {FALSE} by FUNCOP_1:13;
then
A3: rng (Sd-->FALSE) c= BOOLEAN by XBOOLE_1:1;
thus Sd is Deadlock-like implies for M0 being Boolean_marking of PTN st M0.:
Sd = {FALSE} for Q being FinSequence of the carrier' of PTN st Q
is_firable_on M0 holds Firing(Q,M0).:Sd = {FALSE}
proof
assume
A4: Sd is Deadlock-like;
let M0 be Boolean_marking of PTN such that
A5: M0.:Sd = {FALSE};
defpred P[FinSequence of the carrier' of PTN] means $1 is_firable_on M0
implies Firing($1,M0).:Sd = {FALSE};
A6: *'Sd is Subset of Sd*' by A4;
A7: now
let Q be FinSequence of the carrier' of PTN;
let x be transition of PTN;
assume
A8: P[Q];
thus P[ Q^<*x*>]
proof
Firing(Q^<*x*>,M0) = Firing(<*x*>,Firing(Q,M0)) by Th8;
then
A9: ex M being FinSequence of Bool_marks_of PTN st len <*x*> = len M &
Firing(Q^<*x*>,M0) = M/.len M & M/.1 = Firing(<*x*>/.1,Firing(Q,M0) ) & for i
being Nat st i < len <*x*> & i > 0 holds M/.(i+1) = Firing(<*x*>/.(i
+1),M/.i) by Def5;
<*x*>/.1 = x by FINSEQ_4:16;
then
A10: Firing(Q^<*x*>, M0) = Firing(Q,M0) +* (*'{x}-->FALSE) +* ({x}*'
-->TRUE) by A9,FINSEQ_1:39;
assume
A11: Q^<*x*> is_firable_on M0;
then <*x*> is_firable_on Firing(Q,M0) by Th9;
then x is_firable_on Firing(Q,M0) by Th10;
then Firing(Q,M0).:*'{x} c= {TRUE};
then
A12: Firing(Q,M0).:*'{x} misses {FALSE} by XBOOLE_1:63,ZFMISC_1:11;
then *'{x} misses Sd by A8,A11,Th2,Th9;
then not x in *'Sd by A6,PETRI:19;
then {x}*' misses Sd by PETRI:20;
hence
Firing(Q^<*x*>,M0).:Sd = (Firing(Q,M0) +* (*'{x}-->FALSE)).:Sd by A10
,Th3
.= {FALSE} by A8,A11,A12,Th2,Th3,Th9;
end;
end;
A13: P[<*> the carrier' of PTN] by A5,Def5;
thus for Q0 being FinSequence of the carrier' of PTN holds P[Q0] from
FINSEQ_2:sch 2(A13,A7);
end;
A14: rng M0 c= rng ((the carrier of PTN)-->TRUE) \/ rng (Sd-->FALSE) by
FUNCT_4:17;
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 A3,
XBOOLE_1:8;
then rng M0 c= BOOLEAN by A14,XBOOLE_1:1;
then reconsider M0 as Boolean_marking of PTN by A2,FUNCT_2:def 2;
assume
A15: for M0 being Boolean_marking of PTN st M0.:Sd = {FALSE} for Q being
FinSequence of the carrier' of PTN st Q is_firable_on M0 holds Firing(Q,M0)
.:Sd = {FALSE};
assume *'Sd is not Subset of Sd*';
then consider t being transition of PTN such that
A16: t in *'Sd and
A17: not t in Sd*' by SUBSET_1:2;
Sd misses *'{t} by A17,PETRI:19;
then
A18: ((the carrier of PTN)-->TRUE qua Function).:*'{t} = M0.:*'{t} by Th3;
reconsider Q = <*t*> as FinSequence of the carrier' of PTN;
{t}*' meets Sd by A16,PETRI:20;
then consider s being object such that
A19: s in {t}*' /\ Sd by XBOOLE_0:4;
s in {t}*' by A19,XBOOLE_0:def 4;
then
A20: Firing(t,M0).s = TRUE by Th5;
s in Sd by A19,XBOOLE_0:def 4;
then TRUE in Firing(t,M0).:Sd by A20,FUNCT_2:35;
then Firing(t,M0).:Sd <> {FALSE} by TARSKI:def 1;
then
A21: Firing(Q,M0).:Sd <> {FALSE} by Th11;
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 A18,XBOOLE_1:1;
then t is_firable_on M0;
then
A22: Q is_firable_on M0 by Th10;
(M0).:(Sd) = {FALSE qua set} by Th4;
hence contradiction by A15,A22,A21;
end;