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.
I have one more question.
I tried to use 'embedded c code' in SPIN version 6.
active proctype ex1()
{ int x;
do
:: c_expr { Pex1->x < 10 } ->
c_code { Pex1->x++; }
:: x < 10 -> x++
:: else -> break
od
}% spin -a -v ccode.pml
% gcc -o pan pan.c
In file included from pan.c:5259:
pan.m: In function ‘do_transit’:
pan.m:22: error: ‘P0’ has no member named ‘x’
pan.m:31: error: ‘P0’ has no member named ‘x’In pan.h file, variable x is prefixed by '_1_'.
typedef struct P0 { /* ex1 */
unsigned _pid : 8; /* 0..255 */
unsigned _t : 2; /* proctype */
unsigned _p : 5; /* state */
int _1_x;
} P0;That is effected by the new scoping rule, I'm just guessing.
When SPIN runs with the option -O, it compiles successfully.
Is such a reference 'Pex1->x' in c_code unavailable in SPIN6's new scoping rule?
I understand how to avoid the problem.
But the ltl formulae seem convenient, so I look forward to a newer version for fixed it.
Thank you.
Hi. I have a question.
I have the following problem.
mtype = {CASE_NO_I, CASE_NO_II, CASE_NO_III, CASE_NO_IV, CASE_NO_V}
mtype a[3];
active proctype func ()
{
byte i;
do
:: true ->
if :: i = 0 :: i = 1 :: i = 2 fi;
if :: a[i] = CASE_NO_I
:: a[i] = CASE_NO_II
:: a[i] = CASE_NO_III
:: a[i] = CASE_NO_IV
:: a[i] = CASE_NO_V
fi
od
}
ltl {
always (a[1] != CASE_NO_V)
}% spin -a -v mtypearray.pml
ltl ltl_0: [] ((a[1]!=CASE_NO_V))
tl_spin: expected ']', saw '1'
tl_spin: !([] ((a[1]!=CASE_NO_V)))
------------------^Why does the error occur? Is there anything wrong with the ltl clause?
Pages: 1