///////////////////////////////////////
// CIRCAL Dining Philosophers Excersise

// Joel Kelso 2008

// Excersise 2 - Dining Philosophers

// Based on "Hardware Description and Verification Using the
// Circal System", George A. McCaskill and George J. Milne.
// Technical Report CIS-94-25, University of South Australia.
// pp 17-19

Process Fork(Event leftPhilosopherTakes,
                   leftPhilosopherDrops,
                   rightPhilosopherTakes,
                   rightPhilosopherDrops) {
  static Event lpt, lpd, rpt, rpd
  static Process Frk {
    Frk <- lpt lpd Frk + rpt rpd Frk
  }
  return Frk[leftPhilosopherTakes/lpt,
             leftPhilosopherDrops/lpd,
             rightPhilosopherTakes/rpt,
             rightPhilosopherDrops/rpd]
}

int n=2                  // number of philosophers

int Inc(int i) {         // modulo n increment
  return (i+1) % n
}

Process F[n]
Event lpt[n], lpd[n], rpt[n], rpd[n]
// These events are from the fork's point of view.
// We could equally have used events from the
// philosophers' point of view.

for(i=0;i<n;i++) // instantiate n forks
  F[i] <- Fork(lpt[i],lpd[i],rpt[i],rpd[i])