6

The "Automata View" in iSpin (v. 1.1.4) shows .. exactly what? It seems it is just a graph of the control flow of one process.

How would I get the full state space of the system?

E.g., in Ben-Ari: Principles of the Spin Model Checker, I want Figure 4.1.; or in Overview, I want Fig. 1.

d8d0d65b3f7cf42
  • 2,597
  • 15
  • 28

2 Answers2

0

The generated pan program supports the -d and -D command-line arguments, which print state tables in ASCII resp. dot.

chelmuth
  • 124
  • 3
  • Have you tried this on the examples I mentioned? (I did, before I asked here.) These options produce nothing like the pictures I cited. Instead, it looks like a control flow diagram of an individual process. – d8d0d65b3f7cf42 Nov 06 '15 at 14:56
0

The book mentions (in Appendix 2) a tool spinSpider which is part of jspin. I could compile it from source, but did not manage to run it successfully (error messages are unhelpful and the book does not explain usage)

Anyway, spinSpider seems deprecated in favour of VMC in Erigone. It is not clear whether it has the same functionality (draw the complete state graph).

I could compile it but not run, as VMC seems specific to Erigone, and incompatible with Spin, e.g. it says "Can't find file check.pml.trc" - is this the ".trail" file?

d8d0d65b3f7cf42
  • 2,597
  • 15
  • 28