Spinroot

A forum for Spin users

You are not logged in.

#1 2012-10-08 17:10:56

maryam
Member
Registered: 2012-03-27
Posts: 16

access to execution trace

Can anyone tell me if there is a straightforward way to gain a trace of an execution or not?

Offline

#2 2012-10-08 17:17:33

maryam
Member
Registered: 2012-03-27
Posts: 16

Re: access to execution trace

forgot to say that I use spin version 6.2.2 and ispin version 1.1.0.

Offline

#3 2012-10-09 05:26:53

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

Re: access to execution trace

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

#4 2012-10-09 15:49:42

maryam
Member
Registered: 2012-03-27
Posts: 16

Re: access to execution trace

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

#5 2012-10-09 16:05:26

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

Re: access to execution trace

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

#6 2012-10-09 16:57:44

maryam
Member
Registered: 2012-03-27
Posts: 16

Re: access to execution trace

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

#7 2012-10-09 18:15:54

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

Re: access to execution trace

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

#8 2012-10-09 20:40:49

maryam
Member
Registered: 2012-03-27
Posts: 16

Re: access to execution trace

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

#9 2012-10-10 03:35:35

theo.ruys
Administrator
Registered: 2010-11-18
Posts: 11

Re: access to execution trace

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

Board footer

Powered by FluxBB