model-checking - SPIN で状態空間を表示する方法

Question

iSpin (v. 1.1.4) の "Automata View" は、正確には何を示していますか? 1つのプロセスの制御フローの単なるグラフのようです。

システムの完全な状態空間を取得するにはどうすればよいですか?

たとえば、Ben-Ari: Spin Model Checker の原理では、図 4.1 が必要です。または概要では、図1が必要です。