Spinroot

feng_lei_76

Member

Registered: 2011-05-13

Posts: 43

State Reduction using Equivalence Relation

Imagine a problem where the state is a set, where the order of the elements is irrelevant.  In Promela, however, we have to use a data array to represent the set.  Then different orders of the same group of data in the array are considered as different states by SPIN's searching algorithm.  For example, {1, 2, 3} and {3, 2, 1} are two different evaluations of the data array but identical as set.  The repetition will increase the space complexity of the verification process.

How can we avoid this type of redundancy in SPIN?  My feeling is that we must modify the program to detect if a state has been visited.  Can we customize the state comparison program in SPIN so that the user can define any type of equivalence relation on the data?

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: State Reduction using Equivalence Relation

Yes there is a way, but it does involve some work.
You have to declare the original state, or data array, as hidden, so that it is not stored in the state space.
Then you have to declare a separate data structure that you will populate with the abstracted values.
That data structured should be visible and tracked by spin. (If you define it in C, then you would use c_track
statements to track it).
Next, and this is the tricky part, on every state transition you have to call an atomic function (a C function with c_code {} is the simplest) to compute the abstract representation of the state.
The details are explained in this paper:

G.J. Holzmann and R. Joshi, Model-Driven Software Verification
Proc. 11th Spin Workshop, Barcelona, Spain, April 2004, Springer Verlag, LNCS 2989, pp. 77-92.

feng_lei_76

Member

Registered: 2011-05-13

Posts: 43

Re: State Reduction using Equivalence Relation

Thank you for the answer and the cited paper. I'll check this out.

BR

FooxSymn

Member

Registered: 2012-08-18

Posts: 1

Website

Re: State Reduction using Equivalence Relation

It completely agree with told all above.