The abstract of the Mizar article:

Basic Petri Net Concepts

by

Pauline N. Kawamoto,

Yasushi Fuwa, and

Yatsuka Nakamura

Received November 27, 1992

MML identifier: PETRI

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_1, NET_1, MCART_1, ARYTM_3, BOOLE, PETRI;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, MCART_1,
      DOMAIN_1;
 constructors RELSET_1, DOMAIN_1, MEMBERED, XBOOLE_0;
 clusters RELSET_1, PRELAMB, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin

:: Redefinition of Element for Non-empty Relation
definition
  let A, B be non empty set;
  let r be non empty Relation of A, B;
  redefine mode Element of r -> Element of [:A,B:];
end;

:: Place/Transition Net Structure
definition
  struct PT_net_Str
    (# Places, Transitions -> non empty set,
       S-T_Arcs -> non empty Relation of the Places, the Transitions,
       T-S_Arcs -> non empty Relation of the Transitions, the Places #);
end;

reserve PTN for PT_net_Str;

:: Place, Transition, and Arc (s->t, t->s) Elements
definition
  let PTN;
  mode place of PTN is Element of the Places of PTN;
  mode places of PTN is Element of the Places of PTN;
  mode transition of PTN is Element of the Transitions of PTN;
  mode transitions of PTN is Element of the Transitions 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;
  let x be S-T_arc of PTN;
  redefine func x`1 -> place of PTN;

  func x`2 -> transition of PTN;
end;

:: Redefinition of Relation for t->s Arcs
definition
  let PTN;
  let x be T-S_arc of PTN;
  redefine

  func x`1 -> transition of PTN;

  func x`2 -> place of PTN;
end;

:: *S, S* Definitions and Theorems
reserve S0 for Subset of the Places of PTN;

definition
  let PTN, S0;
  func *'S0 -> Subset of the Transitions of PTN equals
:: PETRI:def 1

     { t where t is transition of PTN : ex f being T-S_arc of PTN,
      s being place of PTN st s in S0 & f = [t,s] };

  func S0*' -> Subset of the Transitions of PTN equals
:: PETRI:def 2

     { t where t is transition of PTN : ex f being S-T_arc of PTN,
      s being place of PTN st s in S0 & f = [s,t] };
end;

theorem :: PETRI:1
    *'S0 = {f`1 where f is T-S_arc of PTN : f`2 in S0};

theorem :: PETRI:2
  for x being set holds x in *'S0
    iff
  ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [x,s];

theorem :: PETRI:3
    S0*' = {f`2 where f is S-T_arc of PTN : f`1 in S0};

theorem :: PETRI:4
  for x being set holds x in S0*'
    iff
  ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,x];

:: *T, T* Definitions and Theorems
reserve T0 for Subset of the Transitions of PTN;

definition
  let PTN, T0;
  func *'T0 -> Subset of the Places of PTN equals
:: PETRI:def 3

     { s where s is place of PTN : ex f being S-T_arc of PTN,
      t being transition of PTN st t in T0 & f = [s,t] };

  func T0*' -> Subset of the Places of PTN equals
:: PETRI:def 4

     { s where s is place of PTN : ex f being T-S_arc of PTN,
      t being transition of PTN st t in T0 & f = [t,s] };
end;

theorem :: PETRI:5
    *'T0 = {f`1 where f is S-T_arc of PTN : f`2 in T0};

theorem :: PETRI:6
  for x being set holds x in *'T0
    iff
  ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [x,t];

theorem :: PETRI:7
    T0*' = {f`2 where f is T-S_arc of PTN : f`1 in T0};

theorem :: PETRI:8
  for x being set holds x in T0*'
    iff
  ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,x];

theorem :: PETRI:9
    *'{}the Places of PTN = {};

theorem :: PETRI:10
    ({}the Places of PTN)*' = {};

theorem :: PETRI:11
    *'{}the Transitions of PTN = {};

theorem :: PETRI:12
    ({}the Transitions of PTN)*' = {};

begin

:: Deadlock-like Attribute for Place Sets
definition
  let PTN;
  let IT be Subset of the Places of PTN;
  attr IT is Deadlock-like means
:: PETRI:def 5
      *'IT is Subset of IT*';
end;

:: With_Deadlocks Mode for Place\Transition Nets
definition let IT be PT_net_Str;
  attr IT is With_Deadlocks means
:: PETRI:def 6
      ex S being Subset of the Places of IT st S is Deadlock-like;
end;

definition
  cluster With_Deadlocks PT_net_Str;
end;

begin

:: Trap-like Attribute for Place Sets
definition
  let PTN;
  let IT be Subset of the Places of PTN;
  attr IT is Trap-like means
:: PETRI:def 7
      IT*' is Subset of *'IT;
end;

:: With_Traps Mode for Place\Transition Nets
definition let IT be PT_net_Str;
  attr IT is With_Traps means
:: PETRI:def 8
      ex S being Subset of the Places of IT st S is Trap-like;
end;

definition
  cluster With_Traps PT_net_Str;
end;

definition
  let A, B be non empty set;
  let r be non empty Relation of A, B;
  redefine
    func r~ -> non empty Relation of B, A;
end;

begin

:: Duality Definitions and Theorems for Place/Transition Nets
definition
  let PTN;
  func PTN.: -> strict PT_net_Str equals
:: PETRI:def 9

     PT_net_Str (# the Places of PTN, the Transitions of PTN,
      (the T-S_Arcs of PTN)~, (the S-T_Arcs of PTN)~ #);
end;

theorem :: PETRI:13
  PTN.:.: = the PT_net_Str of PTN;

theorem :: PETRI:14
  the Places of PTN = the Places of PTN.:
    & the Transitions of PTN = the Transitions 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;
  let S0 be Subset of the Places of PTN;
  func S0.: -> Subset of the Places of PTN.: equals
:: PETRI:def 10

     S0;
end;

definition
  let PTN;
  let s be place of PTN;
  func s.: -> place of PTN.: equals
:: PETRI:def 11

     s;
end;

definition
  let PTN;
  let S0 be Subset of the Places of PTN.:;
  func .:S0 -> Subset of the Places of PTN equals
:: PETRI:def 12
       S0;
end;

definition
  let PTN;
  let s be place of PTN.:;
  func .:s -> place of PTN equals
:: PETRI:def 13

     s;
end;

definition
  let PTN;
  let T0 be Subset of the Transitions of PTN;
  func T0.: -> Subset of the Transitions of PTN.: equals
:: PETRI:def 14
       T0;
end;

definition
  let PTN;
  let t be transition of PTN;
  func t.: -> transition of PTN.: equals
:: PETRI:def 15
       t;
end;

definition
  let PTN;
  let T0 be Subset of the Transitions of PTN.:;
  func .:T0 -> Subset of the Transitions of PTN equals
:: PETRI:def 16
       T0;
end;

definition
  let PTN;
  let t be transition of PTN.:;
  func .:t -> transition of PTN equals
:: PETRI:def 17
       t;
end;

reserve S for Subset of the Places of PTN;

theorem :: PETRI:15
  S.:*' = *'S;

theorem :: PETRI:16
  *'(S.:) = S*';

theorem :: PETRI:17
    S is Deadlock-like iff S.: is Trap-like;

theorem :: PETRI:18
    S is Trap-like iff S.: is Deadlock-like;

theorem :: PETRI:19
    for PTN being PT_net_Str,
      t being transition of PTN,
      S0 being Subset of the Places of PTN
  holds t in S0*' iff *'{t} meets S0;

theorem :: PETRI:20
    for PTN being PT_net_Str,
      t being transition of PTN,
      S0 being Subset of the Places of PTN
  holds t in *'S0 iff {t}*' meets S0;