type Matches = ... {- type representing matches -} type Paper = ... {- type representing paper -} type Tobacco = ... {- type representing tobacco -} {- -} {- the table is represented by three different replicated processes -} {- one for each pair of thing that the arbiter can put on it -} def tableTP [item1:Tobacco item2:Paper TPchan:^^[Tobacco Paper]] = TPchan?sendTP = sendTP![item1 item2] def tablePM ..... def table TM ..... new chooseSmokerMatch:^[^[Tobacco Paper] ^[]] {- channel connecting arbiter and smoker with matches -} new chooseSmokerPaper:^[^[Tobacco Matches] ^[]] new chooseSmokerTobacco:^[^[Paper Matches] ^[]] def smokerMatch init:[] {- smoker with matches -} (new getTP:^[Tobacco Paper] new tableempty:^[] new ack:^[] ( chooseSmokerMatch![getTP tableempty] |getTP?[tobacco paper] = (tableempty![] | MAKEacigaretteAndSMOKE {-send [] on ack when finished -} |ack?[] = smokerMatch![] ) ) def matches giveamatch:^Matches = {- the matches of the smoker with matches -} (new takeamatch:^Match TAKEamatch {- a match is taken from the matches and sent on takeamatch -} |takeametch?amatch = giveamatch!amatch) def smokerPaper init:[] = ..... def paper get:^Paper = ... def smokerTobacco init:[] = ..... def tobacco get:^Tobacco = ... def arbiter init:Int = (new br:^Bool ==![init 0 (rchan br)] {- if init is 0 then arbiter enables the smoker with matches to smoke-} |br?b = if b then (new gettobacco:^Tobacco new getpaper:^Paper (tobacco!gettobacco |gettobacco?sometobacco= (paper!getpaper |getpaper?somepaper = (tableTP![sometobacco somepaper smokerMatcheschan] |chooseSmokerMatch?v@[getTP tableempty] = |smokerMatchescan!getTP |tableempty?[] = arbiter!{- the value ((init+1) mod 3) -} else .... {- if init is 1 then arbiter chooses the smocker with tobacco etc. -} ... ) run arbiter!0 run smokerMatch![] run smokerTobacco![] run smokerPaper![]