verif/md/pan.otl

   1 #define p       (write_off - read_off >= 0)
   2 #define q       (write_off - read_off < HALF_UCHAR)
   3
   4         /*
   5          * Formula As Typed: [] (p && q)
   6          * The Never Claim Below Corresponds
   7          * To The Negated Formula !([] (p && q))
   8          * (formalizing violations of the original)
   9          */
  10
  11 never {    /* !([] (p && q)) */
  12 T0_init:
  13         if
  14         :: (((! ((p))) || (! ((q))))) -> goto accept_all
  15         :: (1) -> goto T0_init
  16         fi;
  17 accept_all:
  18         skip
  19 }
  20
  21 #ifdef NOTES
  22 Use Load to open a file or a template.
  23 #endif
  24 #ifdef RESULT
  25 warning: for p.o. reduction to be valid the never claim must be stutter-invariant
  26 (never claims generated from LTL formulae are stutter-invariant)
  27 depth 0: Claim reached state 5 (line 321)
  28 Running verification -- waiting for output
  29         (kill background process 'pan' to abort run)
  30         (use /bin/ps to find pid; then: kill -2 pid)
  31
  32 #endif