Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#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
#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
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
#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