A forum for Spin users
You are not logged in.
Pages: 1
Hi. I have a problem on using Spin 6.1.0.
1 int g;
2
3 inline test(a)
4 {
5 g = g + 3;
6 if
7 :: ((a) % 2) == 0 ->
8 select(g: 12..19)
9 :: ((a) % 2) == 1 ->
10 g = 20
11 :: else ->
12 assert(0)
13 fi
14 }
15
16 active proctype f()
17 {
18 g = 5;
19 do
20 :: g >= 10 -> test(g-10)
21 :: g < 10 -> test(g+10)
22 od
23 }
When I run this example, the following results.
There's something wrong with the line number of the several statements.
$ spin -p -s -r -v -g -u1000 linenum.pml
0: proc - (:root:) creates proc 0 (f)
1: proc 0 (f) linenum.pml:18 (state 1) [g = 5] <- correct
g = 5
2: proc 0 (f) linenum.pml:23 (state 37) [.(goto)] <- What is this for? line 23?
3: proc 0 (f) linenum.pml:19 (state 36) [((g<10))] <- line 19 is "do". may be line 21.
4: proc 0 (f) linenum.pml:14 (state 35) [g = (g+3)] <- line 14 is the bottom of inline test(). may be line 5.
g = 8
5: proc 0 (f) linenum.pml:6 (state 33) [((((g+10)%2)==0))] <- line 6 is "if". may be line 7.
6: proc 0 (f) linenum.pml:8 (state 22) [g = 12] <- select
g = 12
7: proc 0 (f) linenum.pml:9 (state 27) [.(goto)] <- What is this for? inside of select in line 8?
8: proc 0 (f) linenum.pml:8 (state 26) [((g<19))] <- select
9: proc 0 (f) linenum.pml:8 (state 24) [g = (g+1)] <- select
g = 13
10: proc 0 (f) linenum.pml:9 (state 27) [.(goto)] <- ditto
11: proc 0 (f) linenum.pml:8 (state 26) [goto :b2] <- select?
12: proc 0 (f) linenum.pml:19 (state 36) [((g>=10))] <- line 19 is "do". may be line 20.
13: proc 0 (f) linenum.pml:14 (state 18) [g = (g+3)] <- ditto
g = 16
:
I'm actually dealing with bigger code, then I get confused when running track that is incorrect line numbers.
Can you fix the line numbers to get exact ones?
Thank you.
Offline
the .goto lines you can ignore -- it's the internal plumbing spin uses to get the control flow for do..od and if..fi constructs correct -- they probably shouldn't appear in the printouts, but it can be useful to know about these steps sometimes
it is notoriously hard to get yacc to maintain accurate linenumber references -- and clearly spin only partially succeeds -- sorry about that
Offline
Actually I have the problem like yours too in the beginning...but now I think it's fine.
Offline
I have investigated spin's source code ver 6.2.6.
I think this problem is not yacc, it seems to relate some lines which are the output line number in sched() function.
The below is my patch to get correct line number.
Could you please confirm this patch?
========== from here =========
--- sched.c 2014-03-08 18:54:24.290349786 +0900
+++ sched_mod.c 2014-03-08 18:15:49.418870958 +0900
@@ -625,9 +625,11 @@
&& ((verbose&32) || (verbose&4)))
{ if (X == oX)
if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
- { p_talk(X->pc, 1);
- printf(" [");
+ {
+ /* A.Tanaka, 2014.2.13 */
if (!LastStep) LastStep = X->pc;
+ p_talk(LastStep, 1);
+ printf(" [");
comment(stdout, LastStep->n, 0);
printf("]\n");
}
========== to here =========
Offline
I'm glad to be of help.
Patch files doesn't work by cut and paste.
So, I would like to re-post patch by using code-tag.
Patch:
--- sched.c 2014-03-08 18:54:24.290349786 +0900
+++ sched_mod.c 2014-03-08 18:15:49.418870958 +0900
@@ -625,9 +625,11 @@
&& ((verbose&32) || (verbose&4)))
{ if (X == oX)
if (!(e->status & D_ATOM) || (verbose&32)) /* no talking in d_steps */
- { p_talk(X->pc, 1);
- printf(" [");
+ {
+ /* A.Tanaka, 2014.2.13 */
if (!LastStep) LastStep = X->pc;
+ p_talk(LastStep, 1);
+ printf(" [");
comment(stdout, LastStep->n, 0);
printf("]\n");
}
Offline
I have checked latest version 6.3.0.
But It can not work well.
I think file sched.c-line 637
p_talk(X->pc, 1)
should be changed to
p_talk(LastStep, 1);
BTW, you may delete comment
/* A. Tanaka, changed order */
Thank you.
Offline
Thank you for quick response.
OK, I understand it will be fixed version 6.3.1.
And if you have time, could you check other my posted article,
"Line number of the statement No.2", also?
Thank you.
Offline
Pages: 1