:: 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-2019 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;
begin
theorem :: BOOLMARK:1
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;
theorem :: BOOLMARK:2
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;
theorem :: BOOLMARK:3
for A, B being set, f being Function, x being set holds A misses
B implies (f +* (A --> x)).:B = f.:B;
:: 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
:: BOOLMARK:def 1
Funcs(the carrier of PTN, BOOLEAN);
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
:: BOOLMARK:def 2
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
:: BOOLMARK:def 3
M0 +* (*'{t}-->FALSE) +*
({t}*'-->TRUE);
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
:: 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);
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
:: 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);
end;
theorem :: BOOLMARK:4
for A being non empty set, y being set, f being Function holds (f
+*(A --> y)).:A = {y};
theorem :: BOOLMARK:5
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;
theorem :: BOOLMARK:6
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};
theorem :: BOOLMARK:7
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;
theorem :: BOOLMARK:8
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));
theorem :: BOOLMARK:9
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;
theorem :: BOOLMARK:10
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;
theorem :: BOOLMARK:11
for PTN being Petri_net, M0 being Boolean_marking of PTN, t
being transition of PTN holds Firing(t,M0) = Firing(<*t*>,M0);
theorem :: BOOLMARK:12
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};