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