A forum for Spin users
You are not logged in.
Pages: 1
Hi,
I'm new with Spin and the output of ./pan give me this :
State-vector 36 byte, depth reached 3267, errors: 1
14478 states, stored
19167 states, matched
33645 transitions (= stored+matched)
0 atomic steps
hash conflicts: 81 (resolved)
So, I d'ont understand whats are the states stores and matched and what are the differences between them,
Thanks,
Offline
According to the book "Spin Model Checker, The Primer and Reference Manual", "states stored" indicates the total number of unique global system states stored in the state space; "states matched" indicates how many times the search returns to a previously visited state in the search tree.
BR
Offline
newer versions have the number of visited too, which is different from stored and matched. I cannot understand what does "visited" indicate? for example, (335 visited) in the following.
197 states, stored (335 visited)
448 states, matched
783 transitions (= visited+matched)
many thanks in advance
Offline
the visited count only shows up when you do a search for cycles (or liveness properties).
since a state can now be visited twice (but always stored only once), the visited count gives extra information about the search complexity
Offline
thank you very much for your helpful response.
Offline
Pages: 1