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) 2023 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 CSPM
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 ⬚‹fixrec› Package›

text ‹The ⬚‹fixrec› package of \<^session>‹HOLCF› provides a more readable syntax
      (essentially, it allows us to "get rid of ‹μ›" in equations like \<^term>‹μ X. P X›).›

text ‹First, we need to see \<^typ>‹nat› as \<^class>‹cpo›.›

instantiation nat :: discrete_cpo
begin

definition below_nat_def:
  "(x::nat) ⊑ y ⟷ x = y"

instance proof
qed (rule below_nat_def)

end

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     RPHIL  :: ‹nat → dining_event process›
       and LPHIL0 :: ‹dining_event process›
       and FORK   :: ‹nat → dining_event process›
where 
   RPHIL_rec [simp del] :
   ‹RPHIL⋅i = (picks i i → (picks i (i-1) → 
              (putsdown i (i-1) → (putsdown i i → RPHIL⋅i))))›
 | LPHIL0_rec[simp del] :
   ‹LPHIL0 = (picks 0 (N-1) → (picks 0 0 → 
              (putsdown 0 0 → (putsdown 0 (N-1) → LPHIL0))))›
 | FORK_rec  [simp del] :
   ‹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 (λi. RPHIL⋅i) [1..<N])). P›
definition ‹FORKS ≡ ❙|❙|❙| P ∈# mset (map (λi. FORK⋅i) [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