The abstract of the Mizar article:

Basic Concepts for Petri Nets with Boolean Markings

by

Pauline N. Kawamoto,

Yasushi Fuwa, and

Yatsuka Nakamura

Received October 8, 1993

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
  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: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
  holds Sd is Deadlock-like
    iff
  for M0 being Boolean_marking of PTN st M0.:Sd = {FALSE}
    for Q being FinSequence of the Transitions of PTN
      st Q is_firable_on M0
  holds Firing(Q,M0).:Sd = {FALSE};