私のモデル チェック コードでは、特定の変数の最大値を見つけることにのみ関心があります。私が今採用している手順は、assert ステートメントを持ちassert( var < MAX_VALUE )、MAX_VALUE を二分探索方式で変更し続けることです。ただし、SPIN が実際に 1 回の実行で変数の最大可能値を与える方法を持っていれば、はるかに優れています。supUPPAALにはそのためのオペレーターがあることを知っています。SPINに同等のものはありますか?
私のモデル チェック コードでは、特定の変数の最大値を見つけることにのみ関心があります。私が今採用している手順は、assert ステートメントを持ちassert( var < MAX_VALUE )、MAX_VALUE を二分探索方式で変更し続けることです。ただし、SPIN が実際に 1 回の実行で変数の最大可能値を与える方法を持っていれば、はるかに優れています。supUPPAALにはそのためのオペレーターがあることを知っています。SPINに同等のものはありますか?