SPIN にはNext-Step 演算子 (X) があった！
先ほど「SPIN にはNext-0Step 演算子 (X) はない？ - x76789の研究メモ」の続きです．
色々調べると，SPIN でも Next-0Step 演算子 (X) が使えるそうです．
Promela Reference -- ltlの下のほうのNoteに書いてありました．基本的に，SPINのLTL構文にはNext-0Step 演算子 (X)は使えないのですが，コンパイル時に「-DNXT」をつけると，使えるようになるそうです．
＃その場合には，半順序簡約を使わないらしいです．
原文は以下の通り
NOTES
If the Spin sources are compiled with the preprocessor directive -DNXT, the set of temporal operators is extended with one additional unary operator: X (next). The X operator asserts the truth of the subformula that follows it for the next system state that is reached. The use of this operator can void the validity of the partial order reduction algorithm that is used in Spin, if it changes the stutter invariance of an LTL formula. For the partial order reduction strategy to be valid, only LTL properties that are stutter invariant can be used. Every LTL property that does not contain the X operator is guaranteed to satisfy the required property. A property that is not stutter invariant can still be checked, but only without the application of partial order reduction.
