問題タブ [spin]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
154 問題
0
投票する
1
に答える
130
参照
verification - Spin の "到達深度" は、どのような状態と遷移を考慮しますか?
never クレームを使用する (ispin を使用した) 検証でdepth reachedは、状態の数と遷移の数よりも多くの出力が得られます。たとえば、次のようになります。
それは少し直感的ではありません。どこかに「到達深度」のセマンティクスの正確な説明がありますか (パンの出力形式の説明よりも完全です)? たぶん意味は
最長の深さ優先検索パスには 87 個の遷移が含まれていました
は 51 遷移ではなく、never クレームで構成されたシステム オートマトンの遷移を指しますか?