Spinroot

A forum for Spin users

You are not logged in.

#1 2011-03-08 17:04:37

ines.md
Member
Registered: 2011-03-08
Posts: 7

Signification of the counter-example (file .trail)

Good morning,
When you get an error checking, an counter-example is created  (file .trail), it contains 3-numbers (positive or negative) in each of its lines, separated by a colon ":".
I can not understand what expresses each of these three number???

Thank you

Offline

#2 2011-03-09 05:27:24

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

Re: Signification of the counter-example (file .trail)

it's not meant to be human readable, but only a short-hand encoding of the error trail that spin can use to replay the error scenario with as much or as little detail as you choose
(e.g., say: spin -p -t model.pml)
but if you're curious anyway: the first number is the step number (with a few special encodings of cycle-points etc.), the second number is the pid of the process making the transition, and the third number is the transition number.

Offline

#3 2011-03-09 10:06:52

ines.md
Member
Registered: 2011-03-08
Posts: 7

Re: Signification of the counter-example (file .trail)

Why and in which cases we find negative numbers? especially for the number of stages and the number of transitions?? especially for the number of steps and the number of transitions?

It's Not Meant to Be human readable. Why?
I am trying to develop a tool to model workflow net, translate language Promela and finally check whether the workflow net I modeled verif the 3 properties: termination, propre termination and Liveliness (here comes the spin's role ).
In the case where a property is not checked, the counter-example shown to the user. What I looking for is to decode the counter-example to be readable and understandable by any user.Is it possible to do this? if it's possible, can you help me to do it Please?

Thus, when a property is not verified, can we correct our model, based on the counter-example, to verify that the property is well checked?

Offline

#4 2011-03-10 01:51:40

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

Re: Signification of the counter-example (file .trail)

The negative numbers are part of the extra encodings -- to indicate cycle points and to indicate whether or not a never claim was used.
The trail-file is not meant to be human readable because it is an encoding meant to be read by Spin in the reconstruction of the counter-example. It could also have been written in a binary encoding, for instance.
To postprocess a counter-example the best method is to use the Spin output when it reads the trail-file, not the trailfile itself. Reason: Spin knows how to lookup the process pids and the transition ids -- it would be very difficult for another application to reconstruct all the required information.

The judgment how a model should be modified to remove the possibility of a counter-example is probably fundamentally human and unlikely to be automated.

Offline

Board footer

Powered by FluxBB