Spinroot

A forum for Spin users

You are not logged in.

#1 2011-08-26 14:27:11

sk
Member
Registered: 2011-01-31
Posts: 4

Line numbers of the statements

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

#2 2011-08-27 00:25:30

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

Re: Line numbers of the statements

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

#3 2011-09-15 10:51:59

Alisenorry
Member
From: New York
Registered: 2011-09-15
Posts: 1
Website

Re: Line numbers of the statements

Actually I have the problem like yours too in the beginning...but now I think it's fine.

Offline

#4 2014-03-09 00:17:17

AkiraT
Member
Registered: 2014-03-09
Posts: 7

Re: Line numbers of the statements

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

#5 2014-03-09 01:56:06

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

Re: Line numbers of the statements

the patch will be made in the next release: version 6.2.8
thanks!

Offline

#6 2014-03-10 03:12:15

AkiraT
Member
Registered: 2014-03-09
Posts: 7

Re: Line numbers of the statements

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

#7 2014-05-07 03:06:02

AkiraT
Member
Registered: 2014-03-09
Posts: 7

Re: Line numbers of the statements

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

#8 2014-05-07 15:48:10

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

Re: Line numbers of the statements

Akira: sorry, my mistake -- will be corrected in 6.3.1

Offline

#9 2014-05-08 01:18:18

AkiraT
Member
Registered: 2014-03-09
Posts: 7

Re: Line numbers of the statements

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

#10 2014-05-08 21:44:00

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

Re: Line numbers of the statements

will do

Offline

Board footer

Powered by FluxBB