K には、ルールがアクセスできるグローバル状態の概念がありますか? 例: 構成を言いますC => C'。C'探索済みの状態のセットに存在しない場合に遷移し、探索済みの状態のグローバル セットを追加C'して更新します。
プログラムの到達可能なすべての状態を非決定論的に ( --search オプションを使用して) 調査しようとしています。ただし、探索される各パスは独立しています。つまり、構成自体で探索されたセットを渡す場合、各パスは他のパスに見られる構成を認識しません。
グローバルな状態がない場合、この種の動作のベスト プラクティスは何ですか? それぞれの独立したパスがアクセスできるより大きな環境内で遷移を非決定論的に調査する方法はありますか?