:: The Formalization of Decision Free {P}etri Net
::  by Pratima K. Shah , Pauline N. Kawamoto and Mariusz Giero
:: 
:: Received March 31, 2014
:: Copyright (c) 2014-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 PETRI_DF, NUMBERS, XBOOLE_0, FUNCT_1, SUBSET_1, RELAT_1, TARSKI,
      PETRI, FUNCT_2, ARYTM_3, FINSEQ_1, PARTFUN1, XXREAL_0, CARD_1, CARD_3,
      ORDINAL4, NAT_1, ARYTM_1, BOOLMARK, STRUCT_0, PNPROC_1, ZFMISC_1, INT_1,
      FINSET_1, AOFA_I00, NET_1, FINSEQ_4, RFINSEQ, FINSEQ_6, JORDAN23;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
      FUNCT_1, PARTFUN1, FUNCT_2, DOMAIN_1, XXREAL_0, STRUCT_0, ZFMISC_1,
      RELSET_1, FINSEQ_1, PARTIT_2, PETRI, FINSET_1, NAT_D, WSIERP_1, RLAFFIN3,
      NET_1, FINSEQ_6, FINSEQ_4, JORDAN23, RFINSEQ;
 constructors PARTIT_2, NAT_D, WSIERP_1, RLAFFIN3, NET_1, FINSEQ_4, FINSEQ_6,
      RFINSEQ, JORDAN23;
 registrations XXREAL_0, XREAL_0, FINSEQ_1, ORDINAL1, CARD_1, RELSET_1,
      STRUCT_0, XBOOLE_0, SUBSET_1, XTUPLE_0, FINSET_1, NAT_1, MEMBERED,
      VALUED_0, PETRI;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Preliminaries

reserve N for PT_net_Str, PTN for Petri_net, i for Nat;

theorem :: PETRI_DF:1
  for x,y be Nat, f be FinSequence st
  f/^1 is one-to-one & 1 < x & x <= len f & 1 < y & y <= len f & f.x = f.y
  holds x = y;

theorem :: PETRI_DF:2
  for D be non empty set, f be non empty FinSequence of D
  st f is circular holds f.1 = f.len f;

registration
  let D be non empty set;
  let a,b be Element of D;
  cluster <*a,b,a*> -> circular for FinSequence of D;
end;

theorem :: PETRI_DF:3
  for a,b be object st a <> b holds <*a,b,a*> is almost-one-to-one;

definition
  let X be set;
  let Y be non empty set;
  let P be finite Subset of X;
  let M0 be Function of X,Y;
  mode Enumeration of M0, P -> FinSequence of Y means
:: PETRI_DF:def 1

  len it = len the Enumeration of P &
  for i st i in dom it holds
  it.i = M0.((the Enumeration of P).i) if P is non empty
  otherwise it = <*>Y;
end;

definition
  func PetriNet -> Petri_net equals
:: PETRI_DF:def 2
  PT_net_Str(# {0},{1},[#] ({0},{1}),[#] ({1},{0}) #);
end;

notation
  let N;
  synonym places_and_trans_of N for Elements N;
end;

registration
  let PTN;
  cluster places_and_trans_of PTN -> non empty;
end;

reserve fs for FinSequence of places_and_trans_of PTN;

definition
  let PTN,fs;
  func places_of fs -> finite Subset of PTN equals
:: PETRI_DF:def 3
  { p where p is place of PTN : p in rng fs };
  func transitions_of fs -> finite Subset of the carrier' of PTN equals
:: PETRI_DF:def 4
  {t where t is transition of PTN : t in rng fs};
end;

begin :: The number of tokens in a circuit

:: Relation Between P and NAT
definition
  let N;
  func nat_marks_of N -> FUNCTION_DOMAIN of the carrier of N, NAT equals
:: PETRI_DF:def 5
  Funcs(the carrier of N, NAT);
end;

definition
  let N;
  mode marking of N is Element of nat_marks_of N;
end;

:: Generation of nat marking and summation of that
definition
  let N;
  let P be finite Subset of N;
  let M0 be marking of N;
  func num_marks(P, M0) -> Element of NAT equals
:: PETRI_DF:def 6
  Sum (the Enumeration of M0,P);
end;

begin
:: Decision-Free Petri Net Concept and Properties of Circuits in Petri Nets

definition
  let IT be Petri_net;
  attr IT is decision_free_like means
:: PETRI_DF:def 7
  for s being place of IT holds
  ((ex t being transition of IT st [t, s] in the T-S_Arcs of IT) &
  (for t1, t2 being transition of IT
  st [t1, s] in the T-S_Arcs of IT &
  [t2, s] in the T-S_Arcs of IT holds t1 = t2)) &
  ((ex t being transition of IT st
  [s, t] in the S-T_Arcs of IT) &
  (for t1, t2 being transition of IT
  st [s, t1] in the S-T_Arcs of IT &
  [s, t2] in the S-T_Arcs of IT holds t1 = t2));
end;

:: directed_path_like Attribute for
:: FinSequence of places_and_trans_of Petri_net

definition
  let PTN;
  let IT be FinSequence of places_and_trans_of PTN;
  attr IT is directed_path_like means
:: PETRI_DF:def 8

  len IT >= 3 & len IT mod 2 = 1 &
  (for i st i mod 2 = 1 & i + 1 < len IT holds
  [IT.i, IT.(i+1)] in the S-T_Arcs of PTN &
  [IT.(i+1),IT.(i+2)] in the T-S_Arcs of PTN)
  & IT.len IT in the carrier of PTN;
end;

theorem :: PETRI_DF:4
  for fs be FinSequence of places_and_trans_of PetriNet st fs = <*0,1,0*>
  holds fs is directed_path_like;

registration
  let PTN;
  cluster directed_path_like -> non empty
    for FinSequence of places_and_trans_of PTN;
end;

:: With_directed_path Mode for place\transition Nets
definition
  let IT be Petri_net;
  attr IT is With_directed_path means
:: PETRI_DF:def 9
  ex fs being FinSequence of places_and_trans_of IT st
    fs is directed_path_like;
end;

:: directed_circuit_like Attribute for FinSequence of
::  places_and_trans_of PetriNet

definition
  let PTN;
  attr PTN is With_directed_circuit means
:: PETRI_DF:def 10

  ex fs st fs is directed_path_like circular almost-one-to-one;
end;

registration
  cluster PetriNet -> decision_free_like With_directed_circuit Petri;
end;

registration
  cluster With_directed_circuit Petri decision_free_like for Petri_net;
end;

registration
  cluster With_directed_circuit -> With_directed_path for Petri_net;
end;

registration
  cluster With_directed_path for Petri_net;
end;

registration
  let Dftn be With_directed_path Petri_net;
  cluster directed_path_like for FinSequence of places_and_trans_of Dftn;
end;

 reserve Dftn for With_directed_path Petri_net;
 reserve dct for directed_path_like FinSequence of places_and_trans_of Dftn;

theorem :: PETRI_DF:5
  [dct.1, dct.2] in the S-T_Arcs of Dftn;

theorem :: PETRI_DF:6
  [dct.(len dct -1), dct.(len dct)] in the T-S_Arcs of Dftn;

reserve Dftn for With_directed_path Petri Petri_net,
  dct for directed_path_like FinSequence of places_and_trans_of Dftn;

theorem :: PETRI_DF:7
  dct.i in places_of dct & i in dom dct implies i mod 2 = 1;

theorem :: PETRI_DF:8
  dct.i in transitions_of dct & i in dom dct implies i mod 2 = 0;

theorem :: PETRI_DF:9
  dct.i in transitions_of dct & i in dom dct implies
  [dct.(i-1),dct.i] in the S-T_Arcs of Dftn
  & [dct.i,dct.(i+1)] in the T-S_Arcs of Dftn;

theorem :: PETRI_DF:10
  dct.i in places_of dct & 1 < i & i < len dct implies
  [dct.(i-2),dct.(i-1)] in the S-T_Arcs of Dftn
  & [dct.(i-1),dct.i] in the T-S_Arcs of Dftn
  & [dct.i,dct.(i+1)] in the S-T_Arcs of Dftn
  & [dct.(i+1),dct.(i+2)] in the T-S_Arcs of Dftn & 3 <= i;

begin :: Firable and Firing Conditions for Transitions with natural marking

reserve M0 for marking of PTN,
       t for transition of PTN,
       Q,Q1 for FinSequence of the carrier' of PTN;

definition
  let PTN,M0,t;
  pred t is_firable_at M0 means
:: PETRI_DF:def 11
  for m being Nat holds m in M0.:*'{t} implies m > 0;
end;

notation
  let PTN,M0,t;
  antonym t is_not_firable_at M0 for t is_firable_at M0;
end;

definition
  let PTN,M0,t;
  func Firing(t, M0) -> marking of PTN means
:: PETRI_DF:def 12

  for s being place of PTN holds
  (s in *'{t} & not s in {t}*' implies it.s = M0.s -1) &
  (s in {t}*' & not s in *'{t} implies it.s = M0.s + 1) &
  ((s in *'{t} & s in {t}*') or (not s in *'{t} & not s in {t}*')
  implies it.s = M0.s) if t is_firable_at M0
  otherwise it = M0;
end;

definition
  let PTN,M0,Q;
  pred Q is_firable_at M0 means
:: PETRI_DF:def 13
  Q = {} or
  ex M being FinSequence of nat_marks_of PTN st len Q = len M &
  Q/.1 is_firable_at M0 & M/.1 = Firing(Q/.1, M0) &
  for i st i < len Q & i > 0 holds
  Q/.(i+1) is_firable_at M/.i & M/.(i+1) = Firing(Q/.(i+1), M/.i);
end;

notation
  let PTN,M0,Q;
  antonym Q is_not_firable_at M0 for Q is_firable_at M0;
end;

definition
  let PTN,M0,Q;
  func Firing(Q, M0) -> marking of PTN means
:: PETRI_DF:def 14

  it = M0 if Q = {}
  otherwise
  ex M being FinSequence of nat_marks_of PTN st len Q = len M & it = M/.len M
  & M/.1 = Firing(Q/.1, M0)
  & for i st i < len Q & i > 0 holds M/.(i+1) = Firing(Q/.(i+1),M/.i);
end;

theorem :: PETRI_DF:11
  Firing(t, M0) = Firing(<*t*>, M0);

theorem :: PETRI_DF:12
  t is_firable_at M0 iff <*t*> is_firable_at M0;

theorem :: PETRI_DF:13
  Firing(Q^Q1, M0) = Firing(Q1, Firing(Q,M0));

theorem :: PETRI_DF:14
  Q^Q1 is_firable_at M0
  implies Q1 is_firable_at Firing(Q, M0) & Q is_firable_at M0;

begin
:: The theorem stating that the number of tokens in a circuit
:: remains the same after any firing sequence

theorem :: PETRI_DF:15
  for Dftn being With_directed_path Petri decision_free_like Petri_net,
  dct being directed_path_like FinSequence of places_and_trans_of Dftn,
  t being transition of Dftn st dct is circular
  & ex p1 being place of Dftn st p1 in places_of dct &
  ([p1, t] in the S-T_Arcs of Dftn or [t, p1] in the T-S_Arcs of Dftn)
  holds t in transitions_of dct;

definition
  mode Decision_free_PT is
    With_directed_circuit Petri decision_free_like Petri_net;
end;

registration
  let Dftn be With_directed_circuit Petri_net;
  cluster directed_path_like circular almost-one-to-one
    for FinSequence of places_and_trans_of Dftn;
end;

definition
  let Dftn be With_directed_circuit Petri_net;
  mode Circuit_of_places_and_trans of Dftn is
    directed_path_like circular almost-one-to-one
    FinSequence of places_and_trans_of Dftn;
end;

theorem :: PETRI_DF:16
  for Dftn being Decision_free_PT,
  dct being Circuit_of_places_and_trans of Dftn,
  M0 being marking of Dftn, t being transition of Dftn
  holds num_marks(places_of dct, M0) = num_marks(places_of dct, Firing(t, M0));

theorem :: PETRI_DF:17
  for Dftn being Decision_free_PT,
  dct being Circuit_of_places_and_trans of Dftn,
  M0 being marking of Dftn, Q being FinSequence of the carrier' of Dftn holds
  num_marks(places_of dct, M0) = num_marks(places_of dct, Firing(Q, M0));