verification - Spin の "到達深度" は、どのような状態と遷移を考慮しますか?

Question

never クレームを使用する (ispin を使用した) 検証でdepth reachedは、状態の数と遷移の数よりも多くの出力が得られます。たとえば、次のようになります。

Full statespace search for:
    never claim             + (REQ5)
    assertion violations    + (if within scope of claim)
    cycle checks        - (disabled by -DSAFETY)
    invalid end states  - (disabled by never claim)

State-vector 60 byte, depth reached 87, errors: 1
       41 states, stored
       10 states, matched
       51 transitions (= stored+matched)
        9 atomic steps
hash conflicts:         0 (resolved)

それは少し直感的ではありません。どこかに「到達深度」のセマンティクスの正確な説明がありますか (パンの出力形式の説明よりも完全です)? たぶん意味は

最長の深さ優先検索パスには 87 個の遷移が含まれていました

は 51 遷移ではなく、never クレームで構成されたシステム オートマトンの遷移を指しますか?