Prolog で実装するモデル検査器の心臓部 - Qiita

この記事では Prolog を使ったモデル検査器の実装を紹介します。 モデル検査器は、プログラムやアルゴリズムについて主に次の2つの性質の検証を目的としています: 望ましい状態にいつかなる たとえば、いつかロックを獲得できる、い...