I want to be able to construct files containing each of the reachable states within my model, with the valuations of the variables in each state. The formatting doesn’t matter and I’m only using global variables but I’m imagining something like this (maybe in a .csv format instead):

State # | var1 | var2 | var 3 | ...
0| 5 | 3 | 1
1| 5 | 2 | 1
2| 4 | 3 | 1
3| 4 | 2 | 1
...

Ideally, with an accompanying file that lists the transitions between the listed states. Maybe something like this:
Pre-transition state # | Post-transition state #
0 | 1
0 | 2
1 | 3
2 | 3

I appreciate that this could quickly generate massive files that become unruly, but I’m trying to use it on small examples with a few hundred states and transitions. Is this an option somewhere, or is this not something that SPIN can do?

I’ve tried: spin -g -l which seems to do the valuation part for simulation runs but not for exhaustive searches. pan -d gives me state numbers and transitions within the process automata but it’s just the actions at each transition, instead of the valuations that result from them. Aside from that, I’m not seeing anything obvious in the Spin reference book.