title: What are the steps to verify LTL with SPIN tool?
body: <p>I wrote a model in Spin. I want to check some LTL on the model.
  for example:</p>
  
  <pre><code>ltl L1 {&lt;&gt;[]Working}
  </code></pre>
  
  <p>in the Verification window i choose option "use claim"  and click "Run":</p>
  
  <pre><code>ltl L1: &lt;&gt; ([] (Working))
  gcc -DMEMLIM=1024 -O2 -DXUSAFE -w -o pan pan.c
  </code></pre>
  
  <p>at this point I have no idea what to do next...?
  I've tried to look for the answer with Google but there are no guides how to use Spin....</p>