:: Basic Petri Net Concepts. Place/Transition Net Structure, Deadlocks, Traps, Dual Nets
:: by Pauline N. Kawamoto, Yasushi Fuwa and Yatsuka Nakamura
::
:: Received November 27, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
:: Redefinition of Element for Non-empty Relation
definition
let
A
,
B
be non
empty
set
;
let
r
be non
empty
Relation
of
A
,
B
;
:: original:
Element
redefine
mode
Element
of
r
->
Element
of
[:
A
,
B
:]
;
coherence
for
b
1
being
Element
of
r
holds
b
1
is
Element
of
[:
A
,
B
:]
proof
end;
end;
:: Place/Transition Net Structure
definition
attr
c
1
is
strict
;
struct
PT_net_Str
->
2-sorted
;
aggr
PT_net_Str
(#
carrier
,
carrier'
,
S-T_Arcs
,
T-S_Arcs
#)
->
PT_net_Str
;
sel
S-T_Arcs
c
1
->
Relation
of the
carrier
of
c
1
, the
carrier'
of
c
1
;
sel
T-S_Arcs
c
1
->
Relation
of the
carrier'
of
c
1
, the
carrier
of
c
1
;
end;
definition
let
N
be
PT_net_Str
;
attr
N
is
with_S-T_arc
means
:
Def1
:
:: PETRI:def 1
not the
S-T_Arcs
of
N
is
empty
;
attr
N
is
with_T-S_arc
means
:
Def2
:
:: PETRI:def 2
not the
T-S_Arcs
of
N
is
empty
;
end;
::
deftheorem
Def1
defines
with_S-T_arc
PETRI:def 1 :
for
N
being
PT_net_Str
holds
(
N
is
with_S-T_arc
iff not the
S-T_Arcs
of
N
is
empty
);
::
deftheorem
Def2
defines
with_T-S_arc
PETRI:def 2 :
for
N
being
PT_net_Str
holds
(
N
is
with_T-S_arc
iff not the
T-S_Arcs
of
N
is
empty
);
definition
func
TrivialPetriNet
->
PT_net_Str
equals
:: PETRI:def 3
PT_net_Str
(#
{
{}
}
,
{
{}
}
,
(
[#]
(
{
{}
}
,
{
{}
}
)
)
,
(
[#]
(
{
{}
}
,
{
{}
}
)
)
#);
coherence
PT_net_Str
(#
{
{}
}
,
{
{}
}
,
(
[#]
(
{
{}
}
,
{
{}
}
)
)
,
(
[#]
(
{
{}
}
,
{
{}
}
)
)
#) is
PT_net_Str
;
end;
::
deftheorem
defines
TrivialPetriNet
PETRI:def 3 :
TrivialPetriNet
=
PT_net_Str
(#
{
{}
}
,
{
{}
}
,
(
[#]
(
{
{}
}
,
{
{}
}
)
)
,
(
[#]
(
{
{}
}
,
{
{}
}
)
)
#);
registration
cluster
TrivialPetriNet
->
non
empty
non
void
strict
with_S-T_arc
with_T-S_arc
;
coherence
(
TrivialPetriNet
is
with_S-T_arc
&
TrivialPetriNet
is
with_T-S_arc
&
TrivialPetriNet
is
strict
& not
TrivialPetriNet
is
empty
& not
TrivialPetriNet
is
void
)
;
end;
registration
cluster
non
empty
non
void
strict
with_S-T_arc
with_T-S_arc
for
PT_net_Str
;
existence
ex
b
1
being
PT_net_Str
st
( not
b
1
is
empty
& not
b
1
is
void
&
b
1
is
with_S-T_arc
&
b
1
is
with_T-S_arc
&
b
1
is
strict
)
proof
end;
end;
registration
let
N
be
with_S-T_arc
PT_net_Str
;
cluster
the
S-T_Arcs
of
N
->
non
empty
;
coherence
not the
S-T_Arcs
of
N
is
empty
by
Def1
;
end;
registration
let
N
be
with_T-S_arc
PT_net_Str
;
cluster
the
T-S_Arcs
of
N
->
non
empty
;
coherence
not the
T-S_Arcs
of
N
is
empty
by
Def2
;
end;
definition
mode
Petri_net
is
non
empty
non
void
with_S-T_arc
with_T-S_arc
PT_net_Str
;
end;
:: Place, Transition, and Arc (s->t, t->s) Elements
definition
let
PTN
be
Petri_net
;
mode
place of
PTN
is
Element
of the
carrier
of
PTN
;
mode
places of
PTN
is
Element
of the
carrier
of
PTN
;
mode
transition of
PTN
is
Element
of the
carrier'
of
PTN
;
mode
transitions of
PTN
is
Element
of the
carrier'
of
PTN
;
mode
S-T_arc of
PTN
is
Element
of the
S-T_Arcs
of
PTN
;
mode
T-S_arc of
PTN
is
Element
of the
T-S_Arcs
of
PTN
;
end;
:: Redefinition of Relation for s->t Arcs
definition
let
PTN
be
Petri_net
;
let
x
be
S-T_arc
of
PTN
;
:: original:
`1
redefine
func
x
`1
->
place
of
PTN
;
coherence
x
`1
is
place
of
PTN
proof
end;
:: original:
`2
redefine
func
x
`2
->
transition
of
PTN
;
coherence
x
`2
is
transition
of
PTN
proof
end;
end;
:: Redefinition of Relation for t->s Arcs
definition
let
PTN
be
Petri_net
;
let
x
be
T-S_arc
of
PTN
;
:: original:
`1
redefine
func
x
`1
->
transition
of
PTN
;
coherence
x
`1
is
transition
of
PTN
proof
end;
:: original:
`2
redefine
func
x
`2
->
place
of
PTN
;
coherence
x
`2
is
place
of
PTN
proof
end;
end;
definition
let
PTN
be
Petri_net
;
let
S0
be
Subset
of the
carrier
of
PTN
;
func
*'
S0
->
Subset
of the
carrier'
of
PTN
equals
:: PETRI:def 4
{
t
where
t
is
transition
of
PTN
: ex
f
being
T-S_arc
of
PTN
ex
s
being
place
of
PTN
st
(
s
in
S0
&
f
=
[
t
,
s
]
)
}
;
coherence
{
t
where
t
is
transition
of
PTN
: ex
f
being
T-S_arc
of
PTN
ex
s
being
place
of
PTN
st
(
s
in
S0
&
f
=
[
t
,
s
]
)
}
is
Subset
of the
carrier'
of
PTN
proof
end;
correctness
;
func
S0
*'
->
Subset
of the
carrier'
of
PTN
equals
:: PETRI:def 5
{
t
where
t
is
transition
of
PTN
: ex
f
being
S-T_arc
of
PTN
ex
s
being
place
of
PTN
st
(
s
in
S0
&
f
=
[
s
,
t
]
)
}
;
coherence
{
t
where
t
is
transition
of
PTN
: ex
f
being
S-T_arc
of
PTN
ex
s
being
place
of
PTN
st
(
s
in
S0
&
f
=
[
s
,
t
]
)
}
is
Subset
of the
carrier'
of
PTN
proof
end;
correctness
;
end;
::
deftheorem
defines
*'
PETRI:def 4 :
for
PTN
being
Petri_net
for
S0
being
Subset
of the
carrier
of
PTN
holds
*'
S0
=
{
t
where
t
is
transition
of
PTN
: ex
f
being
T-S_arc
of
PTN
ex
s
being
place
of
PTN
st
(
s
in
S0
&
f
=
[
t
,
s
]
)
}
;
::
deftheorem
defines
*'
PETRI:def 5 :
for
PTN
being
Petri_net
for
S0
being
Subset
of the
carrier
of
PTN
holds
S0
*'
=
{
t
where
t
is
transition
of
PTN
: ex
f
being
S-T_arc
of
PTN
ex
s
being
place
of
PTN
st
(
s
in
S0
&
f
=
[
s
,
t
]
)
}
;
theorem
:: PETRI:1
for
PTN
being
Petri_net
for
S0
being
Subset
of the
carrier
of
PTN
holds
*'
S0
=
{
(
f
`1
)
where
f
is
T-S_arc
of
PTN
:
f
`2
in
S0
}
proof
end;
theorem
Th2
:
:: PETRI:2
for
PTN
being
Petri_net
for
S0
being
Subset
of the
carrier
of
PTN
for
x
being
object
holds
(
x
in
*'
S0
iff ex
f
being
T-S_arc
of
PTN
ex
s
being
place
of
PTN
st
(
s
in
S0
&
f
=
[
x
,
s
]
) )
proof
end;
theorem
:: PETRI:3
for
PTN
being
Petri_net
for
S0
being
Subset
of the
carrier
of
PTN
holds
S0
*'
=
{
(
f
`2
)
where
f
is
S-T_arc
of
PTN
:
f
`1
in
S0
}
proof
end;
theorem
Th4
:
:: PETRI:4
for
PTN
being
Petri_net
for
S0
being
Subset
of the
carrier
of
PTN
for
x
being
object
holds
(
x
in
S0
*'
iff ex
f
being
S-T_arc
of
PTN
ex
s
being
place
of
PTN
st
(
s
in
S0
&
f
=
[
s
,
x
]
) )
proof
end;
definition
let
PTN
be
Petri_net
;
let
T0
be
Subset
of the
carrier'
of
PTN
;
func
*'
T0
->
Subset
of the
carrier
of
PTN
equals
:: PETRI:def 6
{
s
where
s
is
place
of
PTN
: ex
f
being
S-T_arc
of
PTN
ex
t
being
transition
of
PTN
st
(
t
in
T0
&
f
=
[
s
,
t
]
)
}
;
coherence
{
s
where
s
is
place
of
PTN
: ex
f
being
S-T_arc
of
PTN
ex
t
being
transition
of
PTN
st
(
t
in
T0
&
f
=
[
s
,
t
]
)
}
is
Subset
of the
carrier
of
PTN
proof
end;
correctness
;
func
T0
*'
->
Subset
of the
carrier
of
PTN
equals
:: PETRI:def 7
{
s
where
s
is
place
of
PTN
: ex
f
being
T-S_arc
of
PTN
ex
t
being
transition
of
PTN
st
(
t
in
T0
&
f
=
[
t
,
s
]
)
}
;
coherence
{
s
where
s
is
place
of
PTN
: ex
f
being
T-S_arc
of
PTN
ex
t
being
transition
of
PTN
st
(
t
in
T0
&
f
=
[
t
,
s
]
)
}
is
Subset
of the
carrier
of
PTN
proof
end;
correctness
;
end;
::
deftheorem
defines
*'
PETRI:def 6 :
for
PTN
being
Petri_net
for
T0
being
Subset
of the
carrier'
of
PTN
holds
*'
T0
=
{
s
where
s
is
place
of
PTN
: ex
f
being
S-T_arc
of
PTN
ex
t
being
transition
of
PTN
st
(
t
in
T0
&
f
=
[
s
,
t
]
)
}
;
::
deftheorem
defines
*'
PETRI:def 7 :
for
PTN
being
Petri_net
for
T0
being
Subset
of the
carrier'
of
PTN
holds
T0
*'
=
{
s
where
s
is
place
of
PTN
: ex
f
being
T-S_arc
of
PTN
ex
t
being
transition
of
PTN
st
(
t
in
T0
&
f
=
[
t
,
s
]
)
}
;
theorem
:: PETRI:5
for
PTN
being
Petri_net
for
T0
being
Subset
of the
carrier'
of
PTN
holds
*'
T0
=
{
(
f
`1
)
where
f
is
S-T_arc
of
PTN
:
f
`2
in
T0
}
proof
end;
theorem
Th6
:
:: PETRI:6
for
PTN
being
Petri_net
for
T0
being
Subset
of the
carrier'
of
PTN
for
x
being
set
holds
(
x
in
*'
T0
iff ex
f
being
S-T_arc
of
PTN
ex
t
being
transition
of
PTN
st
(
t
in
T0
&
f
=
[
x
,
t
]
) )
proof
end;
theorem
:: PETRI:7
for
PTN
being
Petri_net
for
T0
being
Subset
of the
carrier'
of
PTN
holds
T0
*'
=
{
(
f
`2
)
where
f
is
T-S_arc
of
PTN
:
f
`1
in
T0
}
proof
end;
theorem
Th8
:
:: PETRI:8
for
PTN
being
Petri_net
for
T0
being
Subset
of the
carrier'
of
PTN
for
x
being
set
holds
(
x
in
T0
*'
iff ex
f
being
T-S_arc
of
PTN
ex
t
being
transition
of
PTN
st
(
t
in
T0
&
f
=
[
t
,
x
]
) )
proof
end;
theorem
:: PETRI:9
for
PTN
being
Petri_net
holds
*'
(
{}
the
carrier
of
PTN
)
=
{}
proof
end;
theorem
:: PETRI:10
for
PTN
being
Petri_net
holds
(
{}
the
carrier
of
PTN
)
*'
=
{}
proof
end;
theorem
:: PETRI:11
for
PTN
being
Petri_net
holds
*'
(
{}
the
carrier'
of
PTN
)
=
{}
proof
end;
theorem
:: PETRI:12
for
PTN
being
Petri_net
holds
(
{}
the
carrier'
of
PTN
)
*'
=
{}
proof
end;
:: Deadlock-like Attribute for Place Sets
definition
let
PTN
be
Petri_net
;
let
IT
be
Subset
of the
carrier
of
PTN
;
attr
IT
is
Deadlock-like
means
:: PETRI:def 8
*'
IT
is
Subset
of
(
IT
*'
)
;
end;
::
deftheorem
defines
Deadlock-like
PETRI:def 8 :
for
PTN
being
Petri_net
for
IT
being
Subset
of the
carrier
of
PTN
holds
(
IT
is
Deadlock-like
iff
*'
IT
is
Subset
of
(
IT
*'
)
);
:: With_Deadlocks Mode for Place\Transition Nets
definition
let
IT
be
Petri_net
;
attr
IT
is
With_Deadlocks
means
:: PETRI:def 9
ex
S
being
Subset
of the
carrier
of
IT
st
S
is
Deadlock-like
;
end;
::
deftheorem
defines
With_Deadlocks
PETRI:def 9 :
for
IT
being
Petri_net
holds
(
IT
is
With_Deadlocks
iff ex
S
being
Subset
of the
carrier
of
IT
st
S
is
Deadlock-like
);
registration
cluster
non
empty
non
void
V52
()
with_S-T_arc
with_T-S_arc
With_Deadlocks
for
PT_net_Str
;
existence
ex
b
1
being
Petri_net
st
b
1
is
With_Deadlocks
proof
end;
end;
:: Trap-like Attribute for Place Sets
definition
let
PTN
be
Petri_net
;
let
IT
be
Subset
of the
carrier
of
PTN
;
attr
IT
is
Trap-like
means
:: PETRI:def 10
IT
*'
is
Subset
of
(
*'
IT
)
;
end;
::
deftheorem
defines
Trap-like
PETRI:def 10 :
for
PTN
being
Petri_net
for
IT
being
Subset
of the
carrier
of
PTN
holds
(
IT
is
Trap-like
iff
IT
*'
is
Subset
of
(
*'
IT
)
);
:: With_Traps Mode for Place\Transition Nets
definition
let
IT
be
Petri_net
;
attr
IT
is
With_Traps
means
:: PETRI:def 11
ex
S
being
Subset
of the
carrier
of
IT
st
S
is
Trap-like
;
end;
::
deftheorem
defines
With_Traps
PETRI:def 11 :
for
IT
being
Petri_net
holds
(
IT
is
With_Traps
iff ex
S
being
Subset
of the
carrier
of
IT
st
S
is
Trap-like
);
registration
cluster
non
empty
non
void
V52
()
with_S-T_arc
with_T-S_arc
With_Traps
for
PT_net_Str
;
existence
ex
b
1
being
Petri_net
st
b
1
is
With_Traps
proof
end;
end;
definition
let
A
,
B
be non
empty
set
;
let
r
be non
empty
Relation
of
A
,
B
;
:: original:
~
redefine
func
r
~
->
non
empty
Relation
of
B
,
A
;
coherence
r
~
is non
empty
Relation
of
B
,
A
proof
end;
end;
:: Duality Definitions and Theorems for Place/Transition Nets
definition
let
PTN
be
PT_net_Str
;
func
PTN
.:
->
strict
PT_net_Str
equals
:: PETRI:def 12
PT_net_Str
(# the
carrier
of
PTN
, the
carrier'
of
PTN
,
(
the
T-S_Arcs
of
PTN
~
)
,
(
the
S-T_Arcs
of
PTN
~
)
#);
correctness
coherence
PT_net_Str
(# the
carrier
of
PTN
, the
carrier'
of
PTN
,
(
the
T-S_Arcs
of
PTN
~
)
,
(
the
S-T_Arcs
of
PTN
~
)
#) is
strict
PT_net_Str
;
;
end;
::
deftheorem
defines
.:
PETRI:def 12 :
for
PTN
being
PT_net_Str
holds
PTN
.:
=
PT_net_Str
(# the
carrier
of
PTN
, the
carrier'
of
PTN
,
(
the
T-S_Arcs
of
PTN
~
)
,
(
the
S-T_Arcs
of
PTN
~
)
#);
registration
let
PTN
be
Petri_net
;
cluster
PTN
.:
->
non
empty
non
void
strict
with_S-T_arc
with_T-S_arc
;
coherence
(
PTN
.:
is
with_S-T_arc
&
PTN
.:
is
with_T-S_arc
& not
PTN
.:
is
empty
& not
PTN
.:
is
void
)
proof
end;
end;
theorem
:: PETRI:13
for
PTN
being
Petri_net
holds
(
PTN
.:
)
.:
=
PT_net_Str
(# the
carrier
of
PTN
, the
carrier'
of
PTN
, the
S-T_Arcs
of
PTN
, the
T-S_Arcs
of
PTN
#) ;
theorem
:: PETRI:14
for
PTN
being
Petri_net
holds
( the
carrier
of
PTN
=
the
carrier
of
(
PTN
.:
)
& the
carrier'
of
PTN
=
the
carrier'
of
(
PTN
.:
)
& the
S-T_Arcs
of
PTN
~
=
the
T-S_Arcs
of
(
PTN
.:
)
& the
T-S_Arcs
of
PTN
~
=
the
S-T_Arcs
of
(
PTN
.:
)
) ;
definition
let
PTN
be
Petri_net
;
let
S0
be
Subset
of the
carrier
of
PTN
;
func
S0
.:
->
Subset
of the
carrier
of
(
PTN
.:
)
equals
:: PETRI:def 13
S0
;
coherence
S0
is
Subset
of the
carrier
of
(
PTN
.:
)
;
end;
::
deftheorem
defines
.:
PETRI:def 13 :
for
PTN
being
Petri_net
for
S0
being
Subset
of the
carrier
of
PTN
holds
S0
.:
=
S0
;
definition
let
PTN
be
Petri_net
;
let
s
be
place
of
PTN
;
func
s
.:
->
place
of
(
PTN
.:
)
equals
:: PETRI:def 14
s
;
coherence
s
is
place
of
(
PTN
.:
)
;
end;
::
deftheorem
defines
.:
PETRI:def 14 :
for
PTN
being
Petri_net
for
s
being
place
of
PTN
holds
s
.:
=
s
;
definition
let
PTN
be
Petri_net
;
let
S0
be
Subset
of the
carrier
of
(
PTN
.:
)
;
func
.:
S0
->
Subset
of the
carrier
of
PTN
equals
:: PETRI:def 15
S0
;
coherence
S0
is
Subset
of the
carrier
of
PTN
;
end;
::
deftheorem
defines
.:
PETRI:def 15 :
for
PTN
being
Petri_net
for
S0
being
Subset
of the
carrier
of
(
PTN
.:
)
holds
.:
S0
=
S0
;
definition
let
PTN
be
Petri_net
;
let
s
be
place
of
(
PTN
.:
)
;
func
.:
s
->
place
of
PTN
equals
:: PETRI:def 16
s
;
coherence
s
is
place
of
PTN
;
end;
::
deftheorem
defines
.:
PETRI:def 16 :
for
PTN
being
Petri_net
for
s
being
place
of
(
PTN
.:
)
holds
.:
s
=
s
;
definition
let
PTN
be
Petri_net
;
let
T0
be
Subset
of the
carrier'
of
PTN
;
func
T0
.:
->
Subset
of the
carrier'
of
(
PTN
.:
)
equals
:: PETRI:def 17
T0
;
coherence
T0
is
Subset
of the
carrier'
of
(
PTN
.:
)
;
end;
::
deftheorem
defines
.:
PETRI:def 17 :
for
PTN
being
Petri_net
for
T0
being
Subset
of the
carrier'
of
PTN
holds
T0
.:
=
T0
;
definition
let
PTN
be
Petri_net
;
let
t
be
transition
of
PTN
;
func
t
.:
->
transition
of
(
PTN
.:
)
equals
:: PETRI:def 18
t
;
coherence
t
is
transition
of
(
PTN
.:
)
;
end;
::
deftheorem
defines
.:
PETRI:def 18 :
for
PTN
being
Petri_net
for
t
being
transition
of
PTN
holds
t
.:
=
t
;
definition
let
PTN
be
Petri_net
;
let
T0
be
Subset
of the
carrier'
of
(
PTN
.:
)
;
func
.:
T0
->
Subset
of the
carrier'
of
PTN
equals
:: PETRI:def 19
T0
;
coherence
T0
is
Subset
of the
carrier'
of
PTN
;
end;
::
deftheorem
defines
.:
PETRI:def 19 :
for
PTN
being
Petri_net
for
T0
being
Subset
of the
carrier'
of
(
PTN
.:
)
holds
.:
T0
=
T0
;
definition
let
PTN
be
Petri_net
;
let
t
be
transition
of
(
PTN
.:
)
;
func
.:
t
->
transition
of
PTN
equals
:: PETRI:def 20
t
;
coherence
t
is
transition
of
PTN
;
end;
::
deftheorem
defines
.:
PETRI:def 20 :
for
PTN
being
Petri_net
for
t
being
transition
of
(
PTN
.:
)
holds
.:
t
=
t
;
theorem
Th15
:
:: PETRI:15
for
PTN
being
Petri_net
for
S
being
Subset
of the
carrier
of
PTN
holds
(
S
.:
)
*'
=
*'
S
proof
end;
theorem
Th16
:
:: PETRI:16
for
PTN
being
Petri_net
for
S
being
Subset
of the
carrier
of
PTN
holds
*'
(
S
.:
)
=
S
*'
proof
end;
theorem
:: PETRI:17
for
PTN
being
Petri_net
for
S
being
Subset
of the
carrier
of
PTN
holds
(
S
is
Deadlock-like
iff
S
.:
is
Trap-like
)
proof
end;
theorem
:: PETRI:18
for
PTN
being
Petri_net
for
S
being
Subset
of the
carrier
of
PTN
holds
(
S
is
Trap-like
iff
S
.:
is
Deadlock-like
)
proof
end;
theorem
:: PETRI:19
for
PTN
being
Petri_net
for
t
being
transition
of
PTN
for
S0
being
Subset
of the
carrier
of
PTN
holds
(
t
in
S0
*'
iff
*'
{
t
}
meets
S0
)
proof
end;
theorem
:: PETRI:20
for
PTN
being
Petri_net
for
t
being
transition
of
PTN
for
S0
being
Subset
of the
carrier
of
PTN
holds
(
t
in
*'
S0
iff
{
t
}
*'
meets
S0
)
proof
end;