--** Santa Claus: message structures (static network version).
--
--  These are for the solutions discussed in Sections 4-6 of the article:
--
--    "Santa Claus: Formal analysis of a process-oriented solution"
--    Welch, P. H. and Pedersen, J. B.
--    ACM Trans. Program. Lang. Syst. 32, 4, Article 14 (April 2010), 37 pages. 
--    DOI =10.1145/1734206.1734211 http:/doi.acm.org/10.1145/1734206.1734211
--
--  This version slightly extends that presented in Appendix B (to include
--  the "in the waiting room" elf message, introduced in Section 6).


PROTOCOL REINDEER.MSG
  CASE
    holiday; INT         -- start of vacation postcard; reindeer id
    deer.ready; INT      -- back from vacation; reindeer id
    deliver; INT         -- start of toy delivery; reindeer id
    deer.done; INT       -- return from toy delivery; reindeer id
:

PROTOCOL ELF.MSG
  CASE
    working; INT         -- start of work shift; elf id
    elf.ready; INT       -- want to consult Santa; elf id
    waiting; INT         -- in the waiting room; elf id  (chapter 6 / Appendix E)
    consult; INT         -- consulting; elf id
    elf.done; INT        -- end of consultation; elf id
:

PROTOCOL SANTA.MSG
  CASE
    reindeer.ready       -- woken up by reindeer
    harness; INT         -- harnessing this reindeer; id
    mush.mush            -- start of toy delivery
    woah                 -- end of toy delivery
    unharness; INT       -- unharnessing this reindeer; id
    elves.ready          -- woken up by party of elves
    greet; INT           -- greet this elf; id
    consulting           -- consulting with elves
    santa.done           -- end of consultation
    goodbye; INT         -- show elf the door; id
:

PROTOCOL MESSAGE EXTENDS REINDEER.MSG, ELF.MSG, SANTA.MSG: