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