#define N 10

#define NORMAL 0
#define SLEEP 1
#define ENLIGHTENED 2

chan forks[N] = [1] of { int };
chan nudge[N] = [0] of { int };
int silverware[N];
int state[N];

int inactive = 0;

hidden int nil;

inline maybe_sleep() {
  if
  :: skip;
  :: atomic {
      nudge_neigbors();
      printf("Fell asleep\n");
      state[me] = SLEEP;
      inactive++;
      nudge[me]?1;
      inactive--;
      state[me] = NORMAL;
      printf("Woken up\n");
    }
  fi
}

inline nudge_neigbors() {
  atomic {
    //printf("Nudging neigbors\n");
    printf("%d < > %d\n", state[left], state[right]);
    if
    :: (state[left] == SLEEP) -> nudge[left]!nil;
    :: else;
    fi
    if
    :: (state[right] == SLEEP) -> nudge[right]!nil;
    :: else;
    fi
    //printf("Finished nudging\n");
  }
}

active [N] proctype philosopher() {
  int left = _pid - 1;
  if
  :: (left < 0) -> left = left + N;
  :: else;
  fi
  int right = (_pid + 1) % N;
  int me = _pid;

  int left_handed = me == 0;

  do
  :: {

      // think
      printf("Thinking\n");
      if
      :: skip;
      :: {
          state[me] = ENLIGHTENED;
          printf("Became enlightened\n");
        }
      fi
      maybe_sleep();

      // hungry
      printf("Hungry\n");
      maybe_sleep();

      int fork1, fork2 = -1;

      if
      :: (state[me] == ENLIGHTENED) -> {
          int i;
          printf("Looking for forks\n");

          // take first fork
          silverware[me]++;
          inactive++;
          do
          :: (fork1 == -1) -> {
              for (i in forks) {
                atomic {
                  if
                  :: (full(forks[i])) -> {
                      forks[i]?nil;
                      inactive--;
                      silverware[me]++;
                      fork1 = i;
                      printf("Took fork %d\n", fork1);
                      break;
                    }
                  :: (nfull(forks[i])) -> break;
                  fi
                }
              }
             nudge_neigbors();
            }
          :: else -> break;
          od

          // take second fork
          do
          :: (fork2 == -1) -> {
              for (i in forks) {
                atomic {
                  if
                  :: (nfull(forks[i]) && fork1 == i) -> skip;
                  :: (full(forks[i]) && fork1 != i) -> {
                      forks[i]?nil;
                      inactive--;
                      silverware[me]++;
                      fork2 = i;
                      printf("Took fork %d\n", fork2);
                      break;
                    }
                  :: (nfull(forks[i]) && fork1 != i) -> break;
                  fi
                }
              }
              nudge_neigbors();
            }
          :: else -> break;
          od
        }
      :: else -> {
          printf("Picking up nearby forks\n");
          if
          :: (left_handed) -> {

              atomic {
                // take right fork
                silverware[me]++;
                inactive++;
                forks[right]?nil;
                inactive--;
                fork2 = right;
                printf("Took fork %d\n", fork2);
              }

              atomic {
                // take left fork
                silverware[me]++;
                inactive++;
                forks[me]?nil;
                inactive--;
                fork1 = me;
                printf("Took fork %d\n", fork1);
                silverware[me]++;
              }
            }
          :: else -> {
              atomic {
                // take left fork
                silverware[me]++;
                inactive++;
                forks[me]?nil;
                inactive--;
                fork1 = me;
                printf("Took fork %d\n", fork1);
              }

              atomic {
                // take right fork
                silverware[me]++;
                inactive++;
                forks[right]?nil;
                inactive--;
                fork2 = right;
                printf("Took fork %d\n", fork2);
                silverware[me]++;
              }
            }
          fi
        }
      fi

      // eat
      printf("Eating\n")

      // return forks
      forks[fork1]!1;
      silverware[me]--;
      printf("Returned fork %d\n", fork1);
      forks[fork2]!1;
      silverware[me]--;
      printf("Returned fork %d\n", fork2);
      silverware[me]--;
      maybe_sleep();
    }
  od
}

init {
  atomic {
    int i;
    for (i in forks) {
      forks[i]!1;
      silverware[i] = -1;
      state[i] = NORMAL;
    }
  }
  do
  :: {
    //printf("inactive: %d\n", inactive);
    assert(inactive < N);
  }
  od
}