Spinroot

A forum for Spin users

You are not logged in.

#1 2013-02-28 23:57:48

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Tricks to reduce space complexity

Of paramount in effectively using SPIN is to reduce the number of states. In short, a state includes the set of global variables, channels, the set of local variables and process states of the processes, and others.  The state space can be reduced if we can reduce the number of any of these elements.

There are many tricks to reduce the sizes of these elements but SPIN does not directly supports them.  For example, a process often contains many local temporary variables used to obtain other important results. There variables have no effect on the system properties.  For example, the following is a code section for finding the maximal element in a data array of size 10.

x_max = x[0]
for (i : 1 .. 9)
{
  x_max = (x_max < x[i] -> x[i] : x_max)
}

Evidently the local variable i needn't be counted in the system state. Does SPIN have any control to suppress i from the system state?  I know that this is possible for global variables with the "hidden" prefix, but can we do the same thing for local variables?

Another trick is about the process states. If a process contains a long sequence of serial operations without branch or cycle, i.e., the incoming and outgoing transitions at every state are both 1.  Graphically, these states construct a simple chain of operations. Then we don't need to record all these process states in the set of visited states, because they may not be repeated in the future. 

More general, we only need to remember the process states which have either multiple outgoing transitions or multiple incoming transitions. Only these process states need to be recorded in the visited states set, because if the system model revisits a visited state, it must enter those with multiple incoming transitions.

This principle can be extended to the system with multiple processes. My suggestion is that a markup keyword like "hidden" should be defined for hiding non-critical process states. If the state of a process does not have multiple outgoing or incoming transitions, we can maintain the last such one visited by the process and only store them in the visited state set. Therefore, we can reduce the size the visited states set, which retains all the re-entrant states of the system model.

This is still a fuzzy idea. I hope you can understand and find it helpful for the improvement of SPIN.

Offline

#2 2013-03-01 15:32:40

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

Re: Tricks to reduce space complexity

You can use d_step sequences for both cases.

Offline

Board footer

Powered by FluxBB