--** Santa Claus: partial barrier processes.
--
--  These are for the solutions discussed in Sections 4.2 (and Appendix C)
--  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).


PROC p.bar (VAL INT n, CHAN BOOL a?, b?)
  WHILE TRUE
    SEQ
      SEQ i = 0 FOR n    -- gather in the right number of offers
        BOOL any:
        a ? any
      SEQ i = 0 FOR n    -- all offers received: let everyone go
        BOOL any:
        b ? any
:

PROC sync (SHARED CHAN BOOL a!, b!)
  SEQ
    CLAIM a ! TRUE       -- make ofer to syncronise on barrier
    CLAIM b ! TRUE       -- wait for everyone else
:

PROC xp.bar (VAL INT n, CHAN BOOL a?, b?, ping!)
  WHILE TRUE
    SEQ
      SEQ i = 0 FOR n    -- gather in the right number of offers
        BOOL any:
        a ? any
      ping ! TRUE        -- trigger some special process 
                         --   (enough clients are ready)
      SEQ i = 0 FOR n    -- complete partial barrier
        BOOL any:        --   (let the clients go)
        b ? any
: