title: Promela: Why is not this atomic block equivalent to an assignment statement?
body: <p>I wrote following Promela code. This code simulates the situation where two processes increment a shared counter.</p>
  
  <p>I expected the <code>assert</code> in the code must be true, but SPIN says "assertion violated".  Strangely, when I replaced the <code>atomic</code> block with <code>count = count + 1</code>, the error has been gone.</p>
  
  <p>Why is not this atomic block equivalent to an assignment statement?</p>
  
  <pre><code>byte count = 0;
  bool finished[2];
  
  proctype Increment(byte index) {
      atomic {
          byte c = count;
          c = c + 1;
          count = c;
      }
      finished[index] = true;
  }
  
  init {
      run Increment(0);
      run Increment(1);
  
      (finished[0] &amp;&amp; finished[1]);
      assert(count == 2);
  }
  </code></pre>
  
  <p>Execution result:</p>
  
  <pre><code>$ spin -a counter.pml
  $ gcc -o pan pan.c
  $ ./pan
  pan:1: assertion violated (count==2) (at depth 9)
  pan: wrote counter.pml.trail
  
  (Spin Version 6.4.6 -- 2 December 2016)
  Warning: Search not completed
          + Partial Order Reduction
  
  Full statespace search for:
          never claim             - (none specified)
          assertion violations    +
          acceptance   cycles     - (not selected)
          invalid end states      +
  
  State-vector 36 byte, depth reached 11, errors: 1
         28 states, stored
          3 states, matched
         31 transitions (= stored+matched)
          0 atomic steps
  hash conflicts:         0 (resolved)
  
  Stats on memory usage (in Megabytes):
      0.002       equivalent memory usage for states (stored*(State-vector + overhead))
      0.292       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
  </code></pre>