class Philosopher module Philosophers {
  var left: Fork;
  var right: Fork;
  
  method init(f1: Fork, f2: Fork) 
    requires f1!=null && f2!=null;
    requires acc(this.*);
    ensures valid;
    ensures getLeft()==f1 && getRight()==f2;
  {
    left := f1;
    right := f2;
    fold valid;
  }

  method run()
    requires valid;
    requires acc(getLeft().mu, 10);
    requires acc(getRight().mu, 10);
    requires waitlevel << getLeft().mu;
    requires waitlevel << getRight().mu;
    requires getLeft().mu << getRight().mu;
  {
    while(true)
      invariant valid && acc(getLeft().mu, 10) && acc(getRight().mu, 10) && waitlevel << getLeft().mu && waitlevel << getRight().mu && getLeft().mu << getRight().mu;
    {
      unfold valid;
      acquire left;
      acquire right;
      //eat
      release left;
      release right;
      fold valid;
    }
  }

  function getLeft(): Fork 
    requires valid;
    ensures result!=null;
  {
    unfolding valid in left
  }

  function getRight(): Fork 
    requires valid;
    ensures result!=null;
  {
    unfolding valid in right
  }

  predicate valid {
    acc(left) && acc(right) && left!=null && right!=null
  }
}

class Fork module Dining {
  invariant true;
}

class Program module Main {
  method main(){
    // create forks
    var f1 := new Fork;
    var f2 := new Fork;
    var f3 := new Fork;

    share f1;
    share f2 above f1;
    share f3 above f1, f2;

    // create philosophers
    var aristotle := new Philosopher;
    call aristotle.init(f1, f2);

    var plato := new Philosopher;
    call plato.init(f2, f3);

    var kant := new Philosopher;
    call kant.init(f1, f3);
    
    assert f2.mu << f3.mu;

    // start eating
    fork tk0 := aristotle.run();
    fork tk1 := plato.run();
    fork tk2 := kant.run();

    // everyone's done
    join tk0;
    join tk1;
    join tk2;
  }
}