trunk/verif/md/pan.ltl

   1 #define rwoff1 (write_off - read_off >= 0)
   2 #define rwoff2 (write_off - read_off < HALF_UCHAR)
   3
   4 #define wcsum1 (write_off - _commit_sum >= 0)
   5 #define wcsum2 (write_off - _commit_sum < HALF_UCHAR)
   6
   7 #define buffer_large_enough (NUMPROCS + NUMSWITCH <= BUFSIZE)
   8 #define have_events_lost (events_lost != 0)
   9 never {    /* !( buffer_large_enough -> ([](!have_events_lost))) */
  10 T0_init:
  11         if
  12         :: ((buffer_large_enough) && (have_events_lost)) -> goto accept_all
  13         :: ((buffer_large_enough)) -> goto T0_S3
  14         fi;
  15 T0_S3:
  16         if
  17         :: ((have_events_lost)) -> goto accept_all
  18         :: (1) -> goto T0_S3
  19         fi;
  20 accept_all:
  21         skip
  22 }