/*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[1]==FREE)
#define p3 (fork[2]==FREE && fork[2]==FREE)
#define p4 (fork[3]==FREE && fork[3]==FREE)

/*ltl e1 {[]<>(p1||p2||p3||p4)}*/
ltl e2 {[](!(fork[1]||fork[3])) -> <>fork[0]}

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

proctype Philosopher(byte i) {
   do
   :: atomic {
        ((fork[i]==FREE) && (fork[NEXT(i)]==FREE)) ;
        fork[i] = i ;
        fork[NEXT(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
   }
}