Spinroot

A forum for Spin users

You are not logged in.

#1 2012-03-30 12:59:34

Beth
Member
Registered: 2012-03-19
Posts: 11

Interpretation of the contents of a generated trail file

I modeled a simple cryptographic protocol, an intruder process and specified secrecy properties to be satisfied by the protocol in LTL. I later verified the model and got a violation to the specification as expected. SPIN automatically generated a trail fail corresponding to the error as shown below. The thing is, what does the numbers separated by the colons mean?? How do i interpret the below trail??


              -2:3:-2
              -4:-4:-4
               1:0:592
               2:2:100
               3:0:598

Offline

#2 2012-03-31 01:17:55

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

Re: Interpretation of the contents of a generated trail file

you replay it with spin:  spin -t -p model
spin reads the trail file and turns it into something sensible....

Offline

#3 2012-03-31 10:39:26

Beth
Member
Registered: 2012-03-19
Posts: 11

Re: Interpretation of the contents of a generated trail file

Thanks alot.

Offline

Board footer

Powered by FluxBB