Spinroot

A forum for Spin users

You are not logged in.

#1 2016-09-07 15:27:18

mlfv
Member
Registered: 2013-04-29
Posts: 28

poll operations in assignments; hidden variable + d_step inside atomic

Hi,

According to the online Promela Manual and Grammar, the channel poll operations "can be used freely in expressions or even assignments". As the model below shows, these operations can indeed be used in expressions but a compilation error is produced if they are used in assignments. In addition, it seems that in the former case, the semantics of the operation ??[] in a random simulation is not same as in verification. In a random simulation with ispin, the execution is blocked at line 10; but in a safety verification no error is reported.

1    chan d = [5] of {byte, byte}
2   
3    init{
4    d !! 1,1
5    d !! 4,0
6    d !! 2,1
7    d !  3,2
8    int a, b = 1, c = 2
9    (d?? [ _,0]) +1 > 1 && b -> b = a
10    (d?? [ _,0]) +1 > 2 && c -> c = a
11   
12     /* a = d?? [ _,0]+1     /* This is an error */
13    }


I noticed this because I am trying to reduce the state space of certain models and the use of embedded C-code is not helping (besides the random simulations are not allowed). After several tests, I realized that in my case, the best solution would be if the operator ??[] 

1) returns the number of messages in the channel matching the pattern and
2) can be used in assignments.

I looked into the pan files and the semantics of ??[] in verification (Q_has function) returns zero or the position of the first message (true and false in simulations). Therefore, I believe that few changes are required in order to allows 1) without changing the underlying goal, i.e. testing  the executability of the receive statement. I think that 2) may be harder to deal with; but since now the error that it produces is not a syntax error, the compiler would not require a major modification but a local one. Is it possible to consider the inclusion of these features into the language? I believe it would be very helpful to other SPIN users too.

A second issue is the combination of hidden variables and d_steps inside atomic regions. I used them in a model (see https://www.dropbox.com/s/l9w4k1cqhsacovj/prosecutionExImpDsteps.pml?dl=0), but when trying to verify the property I got an unexpected error. When replaying the error trail several warnings are shown ("d_step inside atomic") and also a "transition failed" message at step 145. It looks like the value of the variable (lt) from the previous step was mysteriously changed. Nevertheless, if e.g. the variable is not hidden or the d_steps inside atomic are removed or the assignment lt=0 is added after line 133, then the property is verified.

Offline

#2 2016-09-08 01:52:41

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

Re: poll operations in assignments; hidden variable + d_step inside atomic

on line 10 are you trying to use an expression on the left hand side of an assignment?
that's not going to work, independent of what type of expression it is

Offline

#3 2016-09-08 16:12:25

mlfv
Member
Registered: 2013-04-29
Posts: 28

Re: poll operations in assignments; hidden variable + d_step inside atomic

No, it's just a guarded assignment as line 9.

Offline

#4 2016-09-08 16:52:52

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

Re: poll operations in assignments; hidden variable + d_step inside atomic

Okay -- you have a good point.  Yes, that is a check that was added later, which isn't necessary in this case.
It will be fixed in version 6.4.6.
If you want to make the fix earlier, you can do so by adding one additional
clause to the condition on line 683 in file mesg.c:  || n->ntyp == 'R'
(the if-statement has the comment in front of it that says:
/* ok on the rhs of an assignment: */

Offline

#5 2016-09-08 17:28:08

mlfv
Member
Registered: 2013-04-29
Posts: 28

Re: poll operations in assignments; hidden variable + d_step inside atomic

This fix allows the use of poll operations in rhs, isn't it?

Offline

#6 2016-09-08 17:30:58

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

Re: poll operations in assignments; hidden variable + d_step inside atomic

yes

Offline

#7 2016-09-08 17:35:55

mlfv
Member
Registered: 2013-04-29
Posts: 28

Re: poll operations in assignments; hidden variable + d_step inside atomic

Thanks for the quick response!

Offline

Board footer

Powered by FluxBB