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
]]>