StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>Your claim is violated in the initial state (before the <code>init</code> use of <code>atomic</code>). Here is a SPIN verification run (<code>pan -a</code>) with output from the trail file:</p> <pre><code>ebg@ebg$ spin -a foo.pml ltl ltl_0: (M[0]) U (M[1]) ebg@ebg$ gcc -o pan pan.c ebg@ebg$ ./pan -a pan:1: assertion violated !(( !(M[0])&& !(M[1]))) (at depth 0) pan: wrote foo.pml.trail (Spin Version 6.2.4 -- 21 November 2012) Warning: Search not completed + Partial Order Reduction Full statespace search for: never claim + (ltl_0) assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 36 byte, depth reached 6, errors: 1 4 states, stored (7 visited) 1 states, matched 8 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 0.290 actual memory usage for states 128.000 memory used for hash table (-w24) 0.534 memory used for DFS stack (-m10000) 128.730 total actual memory usage pan: elapsed time 0 seconds ebg@ebg$ spin -p -t foo.pml ltl ltl_0: (M[0]) U (M[1]) starting claim 2 using statement merging spin: _spin_nvr.tmp:5, Error: assertion violated spin: text of failed assertion: assert(!((!(M[0])&&!(M[1])))) Never claim moves to line 5 [D_STEP] spin: trail ends after 1 steps #processes: 1 M[0] = 0 M[1] = 0 T[0] = 0 T[1] = 0 1: proc 0 (:init:) foo.pml:18 (state 3) 1: proc - (ltl_0) _spin_nvr.tmp:3 (state 6) 1 processes created </code></pre> <p>you can see that the <code>ltl</code> was translated to: <code>assert(!(( !(M[0])&& !(M[1]))))</code> which is:</p> <pre><code> !(( !0 && !0)) !(( 1 && 1)) !(( 1 )) 0 </code></pre> <p>and thus the assertion is violated.</p> <p>The easiest way to avoid the problem is to change your arrays to just separate variables. Since your arrays are just size 2 it is easy to do:</p> <pre><code>int M0 = 1; int M1 = 0; int T0 = 0; int T1 = 0; /* then use as appropriate. */ </code></pre> <p>With this, you can skip the <code>init</code> and just make the <code>net</code> proctype declared as <code>active proctype net ()</code></p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload