Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Basic Concepts for Petri Nets with Boolean Markings

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

MML identifier: BOOLMARK
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, FUNCT_4, FUNCOP_1, RELAT_1, BOOLE, SUBSET_1, FINSEQ_1,
PETRI, FRAENKEL, NET_1, MARGREL1, FUNCT_2, ARYTM_3, ARYTM_1, BOOLMARK,
FINSEQ_4;
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, RELAT_1,
FUNCT_1, FUNCT_2, DOMAIN_1, FRAENKEL, FUNCOP_1, FINSEQ_1, FINSEQ_4,
FUNCT_4, MARGREL1, PETRI;
constructors NAT_1, DOMAIN_1, FINSEQ_4, FUNCT_4, MARGREL1, PETRI, REAL_1,
XREAL_0, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FINSEQ_1, RELSET_1, MARGREL1, FUNCOP_1, XREAL_0, ARYTM_3,
ZFMISC_1, XBOOLE_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 Places of PTN, BOOLEAN
equals
:: BOOLMARK:def 1

Funcs(the Places 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 PT_net_Str;
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};
antonym t is_not_firable_on M0;
end;

definition
let PTN be PT_net_Str;
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 PT_net_Str;
let M0 be Boolean_marking of PTN;
let Q be FinSequence of the Transitions 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 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);
antonym Q is_not_firable_on M0;
end;

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

canceled;

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

theorem :: BOOLMARK:6
for PTN being PT_net_Str,
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:7
for PTN being PT_net_Str,
Sd being non empty Subset of the Places of PTN
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:8
for D being non empty set
for Q0,Q1 being FinSequence of D, i being Nat st 1<=i & i<=len Q0
holds (Q0^Q1)/.i=Q0/.i;

canceled;

theorem :: BOOLMARK:10
for PTN being PT_net_Str,
M0 being Boolean_marking of PTN,
Q0, Q1 being FinSequence of the Transitions of PTN
holds Firing(Q0^Q1,M0) = Firing(Q1,Firing(Q0,M0));

theorem :: BOOLMARK:11
for PTN being PT_net_Str,
M0 being Boolean_marking of PTN,
Q0, Q1 being FinSequence of the Transitions of PTN
st Q0^Q1 is_firable_on M0
holds Q1 is_firable_on Firing(Q0,M0) & Q0 is_firable_on M0;

theorem :: BOOLMARK:12
for PTN being PT_net_Str,
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:13
for PTN being PT_net_Str,
M0 being Boolean_marking of PTN,
t being transition of PTN
holds Firing(t,M0) = Firing(<*t*>,M0);

theorem :: BOOLMARK:14
for PTN being PT_net_Str,
Sd being non empty Subset of the Places of PTN