| 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 |