スピンの「深さに達した」とはどのような状態と遷移が考えられますか？主張したことがない使用（IsPinを持つ）検証のために

Question

は、私は例えば、状態の数や遷移の数よりも多い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) 

私は少しわかりにくいことがわかります。 「深度に達した」というセマンティクスの正確な記述は、どこかで（pan's output format descriptionより徹底的に）存在しますか？たぶん

最長深さ優先探索パスの意味は、87のトランジション

51のトランジションを参照していない

が含まれていますが、で構成されるシステムオートマトンの遷移に主張することはありませんか？

Answer 1

はい、あなたは、それが無期限で構成されたシステムオートマトンの遷移を参照していると言いますと、（ある種の）権利です。それと同時に、検証されているシステム内のパスの長さです。これは、決して主張しないで構成されたシステムの1つのステップは、システムの一歩です。もちろん、システムが持っているより多くの、あるいは少ない移行を探求する必要があるかもしれないと主張することは決してありません。パスは必要なループなし（要求に応じて）でさえありませんし、最小でもありません（特別なオプションが設定されていない限り）。