2019-06-29から1日間の記事一覧
PROMELAで記述したモデルから検証器を生成する際にnever claimが2つ以上になると、どれか一つを選択して欲しい旨と-searchオプションを指定する例が出力されます。本などには以下の流れで記載されていますが、何か違いがあったりするのでしょうか。 検証器の…
PROMELAで記述したモデルから検証器を生成する際にnever claimが2つ以上になると、どれか一つを選択して欲しい旨と-searchオプションを指定する例が出力されます。本などには以下の流れで記載されていますが、何か違いがあったりするのでしょうか。 検証器の…