先ほど「SPIN にはNext-0Step 演算子 (X) はない？ - x76789の研究メモ」の続きです．色々調べると，SPIN でも Next-0Step 演算子 (X) が使えるそうです．Promela Reference -- ltlの下のほうのNoteに書いてありました．基本的に，SPINのLTL構文にはNext-0St…

SPIN では，Next Step Operator (X) は使えないらしい．以下はそのSPIN開発者らによる言及． Spin Run-Time Optionsによれば， Spin Run-Time Optionsによれば，SPINには，Next Step Operator (X) がないらしい．なんでも， partial order reduction と互換…