 | Re: Exercise 4 (July 5) |
|
Dear students, some more tips for solving the SPIN part of Exercise 4. Generally, please keep your state space as small as possible, otherwise model checking will fail: 1) Please use only channels of size 1, i.e. if a message is in the channel, another attempt to send a message blocks the process. 2) I overlooked that in the theoretical model the counter of a process can get arbitrarily large, since it can send messages forever. Please introduce a (small) constant MAXCOUNTER such that a process can only send a message if the counter is less than the constant. On the other side, if MAXCOUNTER and the number of processes N is given, it is easy to calculate a lower bound B for the counter, such that the counter is in the range B..MAXCOUNTER. Check that this range is representable by the variable type. 3) Use "short" rather than "int" variables for representing signed values to save memory. I think with above changes model checking should work. If however, you still run out of memory, please note the following further optimization possibility. 3) Optional: model signed numbers not by limited "unsigned" values i.e. unsigned var: SIZE with SIZE as small as possible. The value of var then actually represents "v-2^(SIZE/2)" adjust your arithmetic correspondingly. Of course, you have to find an appropriate range of SIZE for your variables. Finally: if the model checking does not work for you, just return the SPIN model plus an explanation of the problem that occurred and your interpretation of what you think went wrong. Best regards, WS |
Formal Methods in Software Development (SS 2007)
|