A forum for Spin users
You are not logged in.
Pages: 1
Can anyone tell me if there is a straightforward way to gain a trace of an execution or not?
Offline
forgot to say that I use spin version 6.2.2 and ispin version 1.1.0.
Offline
Spin can do random simulation, and will then generate a trace for you.
If using verification, it will generate a trace for failing executions. So to orce a trace, simply force a failure, e.g. With a strategically placed assert(false) statement...
Offline
thanks for reply. I think I didn't ask the right question, actually I need to access to some variables traces, or their variation while simulation or verification. So, I cant access to the trace through promela model while simulation or verification, can I?
Offline
when you invoke spin from the command line (for a simulation, or when replaying a trace from the verifier),
you can enable tracking of local and global variables with the flags -l and -g, and you can add -v for extra verbosity.
this will print the value of a variable each time it changes (but not at every step -- only for steps where the value changes).
i think there's also a way to enable this in iSpin, but i'd have to look it up....
Offline
I should say that ,yes there is an option named "track data values" in iSpin that does the same work. But as you said, this will just <i>print</i> the value of a variable each time it changes, and what I need is to have these changes, may be as an array (or what ever) and use them at the end of execution. may be I could do this using embedded c code? or... find some other way.
Offline
EInteresting -- yes, you could do that with the help of embedded code and storing data in a hidden array (not part of the state vector).
I would recommend that you ask Theo Ruys (one of the moderators on this forum) for advice. He is an expert on this technique, and can alert you to things you'd have to worry about if you take this route.
Offline
yes, in fact spin is a tremendous tool and working with that is realy interesting. Ok, definitely I'll ask him for advice, and I realy appreciate your help, it was so helpful.
Offline
Yes, as spinroot already indicated, it is possible to store these changes in a hidden array using embedded C code.
But I do not yet understand what you want to do with these values "at the end of the execution".
If you only need a trace of the changed values, it is easier to filter the output of SPIN, e.g., using a tool like grep, awk, etc.
Offline
Pages: 1