--** Santa Claus: basic display process.
--
--  This is 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
--
--  So long as this process services all incoming messages, its implementation
--  can be changed to alter the look-and-feel of the model *without* changing
--  the behaviour of the model.
--
--  A more interesting model animation needs separate message channels from each
--  player in the Santa Claus system (so that they can be animated concurrently).
--  This would require trivial changes to the occam-pi implementation of the
--  Santa Claus system.  Note: the CSP model would be unchanged - i.e. this
--  would not impact the formal analysis.


#INCLUDE "course.module"

PROC display (CHAN MESSAGE in?, CHAN BYTE screen!)
  WHILE TRUE
    INT id:
    in ? CASE
      holiday; id
        SEQ
          out.string ("*t*t*t*t*t*tReindeer ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (": on holiday ... wish you were here, :)*c*n", 0, screen!)
      deer.ready; id
        SEQ
          out.string ("*t*t*t*t*t*tReindeer ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (": back from holiday ... ready for work, :(*c*n", 0, screen!)
      deliver; id
        SEQ
          out.string ("*t*t*t*t*t*tReindeer ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (": delivering toys ... la-di-da-di-da-di-da, :)*c*n", 0, screen!)
      deer.done; id
        SEQ
          out.string ("*t*t*t*t*t*tReindeer: ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (": all toys delivered ... want a holiday, :(*c*n", 0, screen!)
      working; id
        SEQ
          out.string ("*t*t*tElf ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (": working, :)*c*n", 0, screen!)
      elf.ready; id
        SEQ
          out.string ("*t*t*tElf ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (": need to consult santa, :(*c*n", 0, screen!)
      waiting; id
        SEQ
          out.string ("*t*t*tElf ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (": in the waiting room ...*c*n", 0, screen!)
      consult; id
        SEQ
          out.string ("*t*t*tElf: ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (": about these toys ... ???*c*n", 0, screen!)
      elf.done; id
        SEQ
          out.string ("*t*t*tElf ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (": OK ... we*'ll build it, bye ... :)*c*n", 0, screen!)
      reindeer.ready
        out.string ("Santa: Ho-ho-ho ... the reindeer are back!*c*n", 0, screen!)
      harness; id
        SEQ
          out.string ("Santa: harnessing reindeer ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (" ... *c*n", 0, screen!)
      mush.mush
        out.string ("Santa: mush mush ...*c*n", 0, screen!)
      woah
        out.string ("Santa: woah ... we*'re back home!*c*n", 0, screen!)
      unharness; id
        SEQ
          out.string ("Santa: un-harnessing reindeer ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (" ... *c*n", 0, screen!)
      elves.ready
        out.string ("Santa: Ho-ho-ho ... some elves are here!*c*n", 0, screen!)
      greet; id
        SEQ
          out.string ("Santa: hello elf ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (" ... *c*n", 0, screen!)
      consulting
        out.string ("Santa: consulting with elves ...*c*n", 0, screen!)
      santa.done
        out.string ("OK, all done - thanks!*c*n", 0, screen!)
      goodbye; id
        SEQ
          out.string ("Santa: goodbye elf ", 0, screen!)
          out.int (id, 0, screen!)
          out.string (" ... *c*n", 0, screen!)
: