title: how to make a non-initialised variable in Spin?
body: <p>It seems that Promela initialises each variable (by default, to 0, or to the value that is given in the declaration). </p>
  
  <p>How can I declare a variable that is initialised by an unknown value?</p>
  
  <p>The documentation suggests <code>if :: p = 0 :: p = 1 fi</code> but I don't think
  that it works: Spin still verifies this claim</p>
  
  <pre><code>bit p 
  init {   if ::  p = 0 :: p = 1 fi }
  ltl {  ! p  }
  </code></pre>
  
  <p>(and falsifies <code>p</code>)</p>
  
  <p>So what exactly is the semantics of <code>init</code>? There still is some 
  "pre-initial" state? How can I work around this - and not confuse my students? </p>