#define NPROCSB 20
#define LEFT(rank) ((rank) > 0 ? (rank) - 1 : nprocs - 1)
//@ ghost int sc[NPROCSB], rc[NPROCSB], sizes[NPROCSB];
int nprocs, nsteps;
/* note that inv0 and inv5 is not needed for proving the deadlock-freedom condition */
/*@ axiomatic FDL {
  @ 
  @ predicate inv1 = \forall integer i; 0 <= i < nprocs ==> 0 <= sizes[i] <= 1;
  @ predicate inv2 = \forall integer i; 0 <= i < nprocs ==> 0 <= sc[i] <= nsteps;
  @ predicate inv3 = \forall integer i; 0 <= i < nprocs ==> 0 <= rc[i] <= nsteps;
  @ predicate inv4 = \forall integer i; 0 <= i < nprocs ==> rc[i]==sc[LEFT(i)]-sizes[LEFT(i)];
  @ predicate inv6 = \forall integer i; 0 <= i < nprocs ==> (sc[i]-rc[i]==0) || (sc[i]-rc[i]==1);
  @ predicate fdl = \exists integer i; 0 <= i < nprocs && ((sc[i]-rc[i]==0 && sizes[i]==0) ||
  @                            (sc[i]-rc[i]==1 && sizes[LEFT(i)]==1));
  @
  @  lemma bounded_free_of_deadlock : inv1 && inv2 && inv3 && inv4 && inv6 && 0<nprocs<=NPROCSB 
  @                                   ==> fdl; 
  @ } */
