Theory DiningPhilosophers

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSPM - Architectural operators for HOL-CSP
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff.
 *
 * This file       : Dining Philosophers example
 *
 * Copyright (c) 2025 Université Paris-Saclay, France
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 *     * Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *
 *     * Redistributions in binary form must reproduce the above
 *       copyright notice, this list of conditions and the following
 *       disclaimer in the documentation and/or other materials provided
 *       with the distribution.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
 * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
 * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
 * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 ******************************************************************************›
(*>*)


chapter‹ Example: Dining Philosophers ›

(*<*)
theory DiningPhilosophers                                               
  imports "HOL-CSPM" "HOL-CSP.GenFixrec-HOLCF" "GenFixrec-RS"
begin 
  (*>*)


section ‹Classic version›

text ‹We formalize here the Dining Philosophers problem with a locale.›


locale DiningPhilosophers =

fixes N::nat
assumes N_g1[simp] : ‹N > 1›  
  ―‹We assume that we have at least one right handed philosophers
    (so at least two philosophers with the left handed one).›

begin

text ‹We use a datatype for representing the dinner's events.›

datatype dining_event  = picks (phil:nat) (fork:nat) 
                       | putsdown (phil:nat) (fork:nat)


text ‹We introduce the right handed philosophers, the left handed philosopher and the forks.›

definition RPHIL:: ‹nat ⇒ dining_event process›
  where ‹RPHIL i ≡ μ X. (picks i i → (picks i ((i-1) mod N) →
                         (putsdown i ((i-1) mod N) → (putsdown i i → X))))›

definition LPHIL0:: ‹dining_event process›
  where ‹LPHIL0 ≡ μ X. (picks 0 (N-1) → (picks 0 0 →
                        (putsdown 0 0 → (putsdown 0 (N-1) → X))))›

definition FORK  :: ‹nat ⇒ dining_event process›
  where ‹FORK i ≡ μ X. (picks i i → (putsdown i i → X)) □ 
                        (picks ((i+1) mod N) i → (putsdown ((i+1) mod N) i → X))›


text ‹Now we use the architectural operators for modelling the interleaving of
      the philosophers, and the interleaving of the forks.›

definition ‹PHILS ≡ ❙|❙|❙| P ∈# add_mset LPHIL0 (mset (map RPHIL [1..< N])). P›
definition ‹FORKS ≡ ❙|❙|❙| P ∈# mset (map FORK [0..< N]). P›


corollary ‹N = 3 ⟹ PHILS = (LPHIL0 ||| RPHIL 1 ||| RPHIL 2)›
  ― ‹just a test›
  unfolding PHILS_def by (simp add: eval_nat_numeral upt_rec Sync_assoc)


text ‹Finally, the dinner is obtained by putting forks and philosophers in parallel.›

definition DINING :: ‹dining_event process›
  where   ‹DINING = (FORKS || PHILS)›


end


section ‹Formalization with the Fixrec package›

text ‹The ▩‹Fixrec› package provides a more readable syntax
      (essentially, it allows us to "get rid of ‹μ›" in equations like \<^term>‹μ X. P X›).
      In contrast to the ▩‹fixrec› package of \<^session>‹HOLCF›, it does not require
      continuous function spaces: the processes are ordinary (total) HOL functions, and no
      \<^class>‹cpo› instances of the argument types (like \<^typ>‹nat›) are needed.
      ▩‹Fixrec› works inside the locale, the equations may refer to its parameter ‹N›.›

locale DiningPhilosophers_fixrec =

fixes N::nat
assumes N_g1[simp] : ‹N > 1›  
  ―‹We assume that we have at least one right handed philosophers
    (so at least two philosophers with the left handed one).›

begin

text ‹We use a datatype for representing the dinner's events.›

datatype dining_event  =    picks (phil:nat) (fork:nat) 
                          | putsdown (phil:nat) (fork:nat)


text ‹We introduce the right handed philosophers, the left handed philosopher and the forks.›

Fixrec [RS, HOLCF]     
      RPHIL   :: ‹nat ⇒ dining_event process›
  and LPHIL0  :: ‹dining_event process›
  and FORK    :: ‹nat ⇒ dining_event process›
  where 
    RPHIL_rec  : ‹RPHIL i = (picks i i → (picks i (i-1) → 
                                 (putsdown i (i-1) → (putsdown i i → RPHIL i))))›
  | LPHIL0_rec : ‹LPHIL0 = (picks 0 (N-1) → (picks 0 0 → 
                                 (putsdown 0 0 → (putsdown 0 (N-1) → LPHIL0))))›
  | FORK_rec   : ‹FORK i  = (picks i i → (putsdown i i → FORK i)) □
                            (picks ((i+1) mod N) i → (putsdown ((i+1) mod N) i → FORK i))›


text ‹Now we use the architectural operators for modelling the interleaving of
      the philosophers, and the interleaving of the forks.›

definition ‹PHILS ≡ ❙|❙|❙| P ∈# add_mset LPHIL0 (mset (map RPHIL [1..<N])). P›
definition ‹FORKS ≡ ❙|❙|❙| P ∈# mset (map FORK [0..<N]). P›


corollary ‹N = 3 ⟹ PHILS = (LPHIL0 ||| RPHIL 1 ||| RPHIL 2)›
  ― ‹just a test›
  unfolding PHILS_def by (simp add: eval_nat_numeral upt_rec Sync_assoc)


text ‹Finally, the dinner is obtained by putting forks and philosophers in parallel.›

definition DINING :: ‹dining_event process›
  where   ‹DINING = (FORKS || PHILS)›


end

(*<*)
end
(*>*)