/*ltl p1 {[]<>(eating[0]) && []<>(eating[1])&& []<>(eating[2])&& []<>(eating[3])}*/

#define N 4
#define FREE  N
#define TRUE  1
#define FALSE 0
#define NEXT(i) (i+1)%N

#define p1 {fork[0]==FREE && <>(fork[1]==Free)}
#define p2 {fork[1]==FREE && <>(fork[0]==Free)}
#define p3 {fork[2]==FREE && <>(fork[3]==Free)}
#define p4 {fork[3]==FREE && <>(fork[2]==Free)}


//No deadlock
ltl e3 {[](p1&&p2&&p3&&p4)}*/

byte fork[N] ;
bool eating[N] ;

proctype Philosopher(byte i) {
   do
   :: (i%2==0) -> 
      atomic {
        (fork[i]==FREE) ;
        fork[i] = i ;
      }
      atomic {
        (fork[NEXT(i)]==FREE) ;
        fork[NEXT(i)] = i
      }
      /* prove that here we do indeed have the forks: */
      assert (fork[i]==i) && (fork[NEXT(i)]==i) ;
      eating[i] = TRUE ;
      printf("%u\n",i) ;
      eating[i] = FALSE ;
      fork[i] = FREE ;
      fork[NEXT(i)] = FREE
   :: (i%2==1) -> 
      atomic {
        (fork[NEXT(i)]==FREE) ;
        fork[NEXT(i)] = i
      }
      atomic {
        (fork[i]==FREE) ;
        fork[i] = i ;
      }
      /* prove that here we do indeed have the forks: */
      assert (fork[i]==i) && (fork[NEXT(i)]==i) ;
      eating[i] = TRUE ;
      eating[i] = FALSE ;
      fork[i] = FREE ;
      fork[NEXT(i)] = FREE
   od
}

init {
   byte k = 0 ;
   /* initially, all forks are free */
   do
   :: k<N  -> fork[k] = FREE ; k++
   :: k==N -> break
   od
   k = 0 ;
   /* create the philosophers and run them: */
   atomic {
     do
     :: k<N  -> run Philosopher(k) ; k++
     :: k==N -> break
     od
   }
}