A forum for Spin users
You are not logged in.
Pages: 1
Thank you so much for the quick response and information.
I immediately read your book!
Dear Professor Gerard J. Holzmann,
May I ask one additional question?
>>>For instance, first test for the priority 1 case and only if that fails test for the priority 2 case.
>>This is defined by the Promela specification, isn't it?
>yes it is
You told me that SPIN chooses the first executable clause on a do
loop, and explores the execution trace first (The others are
postponed). This is not an implementation-matter but defined by
a specification.
Could you tell me how I should cite the fact in my paper? I
appreciate if you would tell me some literature/document. I am
writing a paper about developing a software which uses SPIN as
backend engine.
# If no document is published (confidential), I would like to
# cite the SPIN forum, that is, to write ``I have confirmed the
# specification by the developer at the SPIN forum'' in my paper.
Tatsuya
Thank you! My questions have been completely resolved.
Dear Professor Gerard J. Holzmann,
Thank you so much for the quick response.
I got it. I manually lift up a clause according to a
counterexample which I expect, as follows:
do
:: atomic { i<2 -> i++; }
:: atomic { i<1 -> i++; x=1; }
:: else -> break;
od;
assert(x==1);
>>However, this method depends on implementation of Spin.
I am wondering if I was wrong.
>For instance, first test for the priority 1 case and only if that fails test for the priority 2 case.
This is defined by the Promela specification, isn't it?
Tatsuya
Hello,
I am Tatsuya, a Spin user. I am wondering if there exists a way
to control choices of executable clauses through Promela codes.
The following (named as foo.pml):
active proctype main() {
int i=0;
int x=0;
do
:: atomic { i<1 -> i++; x=1; }
:: atomic { i<2 -> i++; }
:: else -> break;
od;
assert(x==1);
}
has two executions:
the first clause; the second clause; break; ... , and
the second clause; the second clause; break; ... .
since there exist two executable clauses at first.
The assertion is violated. Actually,
$ spin -a foo.pml; gcc -O0 -w -g -DSAFETY pan.c; ./a.out -c1
pan:1: assertion violated (x==1) (at depth 3)
pan: wrote foo.pml.trail
(Spin Version 6.4.6 -- 2 December 2016)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 20 byte, depth reached 5, errors: 1
9 states, stored
0 states, matched
9 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
The latter execution is a counterexample. Next, I modify the
Promela code by exchanging the first and second clauses. Of
course, Spin returns the same counterexample. However, the
number of states is reduced as follows:
State-vector 20 byte, depth reached 3, errors: 1
4 states, stored
0 states, matched
4 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
I guess that the exploration strategy in the current version is
to choose the first clause if there exist multiple executable
clauses. In this sense, I can control explorations of executions
by Spin through Promela codes. However, this method depends on
implementation of Spin.
Could you tell me if there exists a way to control choices of
executable clauses through Promela codes? For example,
do
#pragma priority(2)
:: atomic { i<1 -> i++; x=1; }
#pragma priority(1)
:: atomic { i<2 -> i++; }
:: else -> break;
od;
This looks useful for me because I often model algorithms while
expecting specific counterexamples. Of course, if there is a
better way, could you tell me that?
Thank you in advance.
Tatsuya
# Although I have searched similar questions at this forum by
# using ``executable'', ``exploration'', ``clause'', etc., I
# could not find that. If a similar question was asked, could
# you direct me to the thread?
#
# I also referred to some papers at SPIN workshops which proposed
# new partial order reductions, e.g.,
# D. Bosnacki and G.J. Holzmann ``Improving Spin's Partial-Order Reduction for Breadth-First Search''.
# However, they modify Spin itself, and are beyond my skill.
Thank you so much for the detailed explanation.
As you completely understand,
1. I use c_code {...} and c_expr {...}, and
2. I designate too large MA size.
I am afraid if my experiments (under overflow condition) would be
stresses to Spin. I try to re-consider design of my tool
(to return better Promela codes).
At the end of the post, let me explain why I did the above 1 and 2.
I would be glad if they are useful to development of Spin.
Thank you,
Tatsuya
1.
My tool generates Promela codes that contain a large size of
guards (for if/do statements). Spin translates the Promela codes
into C codes. However, it seems that GCC is not good at
compiling the C codes, and GCC requires much time (e.g., two hours)
to compile the C codes.
Therefore, I brushed up my tool. My tool generates C codes that
contain functions corresponding to the guards, and generated
Promela codes that call the functions written in C.
To include the C codes, my tool writes c_code {...} in Promela
codes. To call the functions in the C codes, my tool writes
c_expr {...} in Promela codes.
GCC can compile the C codes into which Spin translates the
Promela code with c_expr {...}, compile the C codes that
contain functions corresponding to the guards, and link them in a
few minutes. Results of verifications (for a test suite that I
developed) are exactly the same.
2.
In my previous post, it sounds that not size of Promela code but
size of MA (that I designated) raises the trouble.
Let me explain why I designated too large MA while the small
code (53KiB) can be correctly verified under -DMA=98765.
The original code that I would like to verify is so large (around
6MiB). When I first tried to check the code as follows:
$ spin -a a_Sequential.pml
$ gcc -O0 -w -g -DVERBOSE -DVECTORSZ=645678 -DMEMLIM=6144 -DMA=500000 -DSAFETY -o a_Sequential.exe a_Sequential_guards.c a_Sequential_asserts.c pan.c
...
Spin returned the following:
0: Down - program non-accepting [pids 0-0]
pan: error, MA too small, recompile pan.c with -DMA=N with N>511925
pan:1: aborting (at depth 0)
pan: wrote a_Sequential.pml.trail
...
Therefore, I executed the following command:
$ spin -a a_Sequential.pml
$ gcc -O0 -w -g -DVERBOSE -DVECTORSZ=645678 -DMEMLIM=6144 -DMA=511926 -DSAFETY -o a_Sequential.exe a_Sequential_guards.c a_Sequential_asserts.c pan.c
and found the trouble since Spin returned the following:
0: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 2239
0: proc 0 exec 2239, 1 to 2, hs_req_at_0_on_0 = 0 non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
on-stack
1: Up - program
1: proc 0 reverses 2239, 1 to 2
hs_req_at_0_on_0 = 0 [abit=0,adepth=0,tau=0,0]
0: zapping
old state
(Spin Version 6.4.4 -- 1 November 2015)
+ Partial Order Reduction
+ Graph Encoding (-DMA=511926)
+ FullStack Matching
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 512044 byte, depth reached 0, errors: 0
Minimized Automaton: 106349 nodes and 159524 edges
1 states, stored
1 states, matched
0 matches within stack
2 transitions (= stored+matched)
0 atomic steps
stackframes: 0/0
...
Thank you so much for the quick response, information, and
proposal to check my code.
After I submitted my question to the forum, I tried to find the
smallest in my codes that raises the same trouble.
I found such a small code (code size: 53KiB, lines: 1219,
state-vector: 3KiB).
I.
>You can also try to see why it stops after one state by
>compiling with -DVERBOSE and check the output of the run.
I applied it (compiling with -DVERBOSE) to the small code.
A result is as follows. Any suggestion is welcome.
$ gcc -O0 -w -g -mcmodel=large -DVERBOSE -DVECTORSZ=45678 -DMEMLIM=6144 -DMA=3408748 -DSAFETY -o sequential_tso_diff_Sequential.exe sequential_tso_diff_Sequential_guards.c sequential_tso_diff_Sequential_asserts.c pan.c
...
0: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 188
0: proc 0 exec 188, 1 to 2, x_at_0_on_0 = 0 non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
on-stack
1: Up - program
1: proc 0 reverses 188, 1 to 2
x_at_0_on_0 = 0 [abit=0,adepth=0,tau=0,0]
0: zapping
old state
(Spin Version 6.4.4 -- 1 November 2015)
+ Partial Order Reduction
+ Graph Encoding (-DMA=3408748)
+ FullStack Matching
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 3356 byte, depth reached 0, errors: 0
MA stats: -DMA=3238 is sufficient
Minimized Automaton: 1753 nodes and 2629 edges
1 states, stored
1 states, matched
0 matches within stack
2 transitions (= stored+matched)
0 atomic steps
stackframes: 0/0
stats: fa 0, fh 0, zh 0, zn 0 - check 0 holds 0
stack stats: puts 0, probes 0, zaps 0
Stats on memory usage (in Megabytes):
0.003 equivalent memory usage for states (stored*(State-vector + overhead))
4.356 actual memory usage for states
106.812 memory used for DFS stack (-m2000000)
111.168 total actual memory usage
cf. decrease size of -DMA
$ gcc -O0 -w -g -mcmodel=large -DVERBOSE -DVECTORSZ=45678 -DMEMLIM=6144 -DMA=98765 -DSAFETY -o sequential_tso_diff_Sequential.exe sequential_tso_diff_Sequential_guards.c sequential_tso_diff_Sequential_asserts.c pan.c
...
0: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 188
0: proc 0 exec 188, 1 to 2, x_at_0_on_0 = 0 non-accepting [tau=0]
1: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 189
1: proc 0 exec 189, 2 to 3, mem_at_0_on_0[x_at_0_on_0] = 0 non-accepting [tau=0]
2: Down - program non-accepting [pids 0-0]
new state
Pr: 0 Tr: 190
2: proc 0 exec 190, 3 to 4, x_at_1_on_0 = 0 non-accepting [tau=0]
...(167266 lines)...
468: Down - program non-accepting [pids 1-1]
Pr: 1 Tr: 107
468: proc 1 exec 107, 171 to 1162, kind_counter = 0 non-accepting [tau=8]
469: Down - program non-accepting [pids 2-0]
on-stack
469: Up - program
469: proc 1 reverses 107, 171 to 1162
kind_counter = 0 [abit=0,adepth=0,tau=0,8]
468: Up - program
468: proc 1 reverses 2, 173 to 171
else [abit=0,adepth=0,tau=8,8]
...(167265 lines)...
3: zapping
old state
3: Up - program
3: proc 0 reverses 190, 3 to 4
x_at_1_on_0 = 0 [abit=0,adepth=0,tau=64,64]
2: zapping
old state
2: Up - program
2: proc 0 reverses 189, 2 to 3
mem_at_0_on_0[x_at_0_on_0] = 0 [abit=0,adepth=0,tau=64,64]
1: zapping
old state
1: Up - program
1: proc 0 reverses 188, 1 to 2
x_at_0_on_0 = 0 [abit=0,adepth=0,tau=64,64]
0: zapping
old state
(Spin Version 6.4.4 -- 1 November 2015)
+ Partial Order Reduction
+ Graph Encoding (-DMA=98765)
+ FullStack Matching
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 3372 byte, depth reached 2262, errors: 0
MA stats: -DMA=3242 is sufficient
Minimized Automaton: 123986 nodes and 216099 edges
255 states, stored
174 states, matched
0 matches within stack
429 transitions (= stored+matched)
49062 atomic steps
stackframes: 3/12
stats: fa 0, fh 0, zh 0, zn 0 - check 10 holds 6
stack stats: puts 0, probes 0, zaps 0
Stats on memory usage (in Megabytes):
0.829 equivalent memory usage for states (stored*(State-vector + overhead))
81.942 actual memory usage for states
106.812 memory used for DFS stack (-m2000000)
4.019 memory lost to fragmentation
184.783 total actual memory usage
II.
>Would it be possible to send a version of this model, so that I
>can check what happens in this case?
Sure. My code (the small code that raises the same problem) is public.
The code is generated by my open-source tool McSPIN.
https://bitbucket.org/abet/mcspin/
How should I send the code?
i. Should I simply send a set of codes (and a tiny shell script to run Spin)?
The code is generated, but I guess that it is not impossible to be read.
Can I attach it with a reply on this forum? (although I do not know how to do)
ii. Or, should I send an instruction to start to use my tool McSPIN?
I guess that it is not better since installation of some softwares
(GHC, GHC libraries, etc.) are required.
Best,
Tatsuya
Hello,
I am Tatsuya, a Spin user. Now I am wondering how to use the
-DMA option. I would be glad to hear how to use it.
I am trying to verify large Promela codes. To decrease memory
sizes to be consumed by Spin, I started to use the -DMA option
while I have used the -DCOLLAPSE option only.
For some small Promela codes, it seeems that I succeeded in using
the -DMA option correctly as follows:
$ gcc -O0 -w -g -DVECTORSZ=5678 -DMEMLIM=6144 -DMA=98765 -DSAFETY pan.c
...
(Spin Version 6.4.4 -- 1 November 2015)
+ Partial Order Reduction
+ Graph Encoding (-DMA=98765)
...
State-vector 4708 byte, depth reached 2263, errors: 0
MA stats: -DMA=4578 is sufficient
Minimized Automaton: 151982 nodes and 272208 edges
257 states, stored
176 states, matched
433 transitions (= stored+matched)
49062 atomic steps
cf.
$ gcc -O0 -w -g -DVECTORSZ=5678 -DMEMLIM=6144 -DCOLLAPSE -DSAFETY pan.c
...
(Spin Version 6.4.4 -- 1 November 2015)
+ Partial Order Reduction
+ Compression
...
State-vector 4708 byte, depth reached 2263, errors: 0
254 states, stored
170 states, matched
424 transitions (= stored+matched)
49062 atomic steps
hash conflicts: 0 (resolved)
However, for a large Promela code, it seems that I failed to run
Spin correctly as follows:
$ gcc -O0 -w -g -mcmodel=large -DVECTORSZ=521098 -DMEMLIM=131900 -DMA=429531 -DSAFETY pan.c
...
(Spin Version 6.4.4 -- 1 November 2015)
+ Partial Order Reduction
+ Graph Encoding (-DMA=429531)
...
State-vector 419644 byte, depth reached 0, errors: 0
MA stats: -DMA=419531 is sufficient
Minimized Automaton: 72631 nodes and 108947 edges
1 states, stored
1 states, matched
2 transitions (= stored+matched)
0 atomic steps
Stats on memory usage (in Megabytes):
0.400 equivalent memory usage for states (stored*(State-vector + overhead))
99.287 actual memory usage for states
26.703 memory used for DFS stack (-m500000)
125.990 total actual memory usage
cf.
$ gcc -O0 -w -g -mcmodel=large -DVECTORSZ=521098 -DMEMLIM=131900 -DCOLLAPSE -DSAFETY pan.c
...
(Spin Version 6.4.4 -- 1 November 2015)
+ Partial Order Reduction
+ Compression
...
State-vector 419660 byte, depth reached 174976, errors: 0
87594 states, stored
94087 states, matched
181681 transitions (= stored+matched)
2.3812352e+08 atomic steps
hash conflicts: 351 (resolved)
Stats on memory usage (in Megabytes):
35059.787 equivalent memory usage for states (stored*(State-vector + overhead))
32761.915 actual memory usage for states (compression: 93.45%)
state-vector as stored = 392152 byte + 36 byte overhead
128.000 memory used for hash table (-w24)
26.703 memory used for DFS stack (-m500000)
185.697 memory lost to fragmentation
32759.338 total actual memory usage
I cannot find any error/warning message that Spin returns.
Could you give me any help?
Best,
Tatsuya
I appreciate your quick response every time. I understand that spin
has no limit about it, but a back-end C compiler may returns the error.
And, thank you so much for the proposal to use assertions. I'll try it!
Hi,
I am wondering if there is a limit on the number of statements at
a clause in never claim. I cannot find any description about the
number of statements at a clause in a never claim.
A never claim in my code is
never {
T0_init:
if
:: a[0]==1 || ... || a[N]==1 -> goto accept_all
:: else -> goto T0_init;
fi;
accept_all:
skip
}
# Since statements with side effects are not allowed in never {},
# I do not use a loop statement with an increment statement, and
# expand a[i] to a[0]...a[N]. Could you tell me anything better?
When N<10000, I succeeded in checking acceptance about never claim.
But, when e.g., N==15000, "spin -a" returns "Segmentation fault".
Thank you so much for the quick response.
I will try "spin -I" and check it.
Hi,
Since my question is similar to miss_mare's, I post my question here. I use Spin 6.2.6.
As he said, I pass a whole array and meet "spin: test.pml:11, Error: missing array index for ...".
int a[3];
inline foo(b) {
printf("a[1]==%d\n",b[1]);
}
active proctype main() {
a[0]=0;
a[1]=1;
a[2]=2;
foo(a);
}
But, Spin looks to run normally with the error message in simulation mode.
a[1]==1
1 process created
and generate pan.c in verification mode.
Also, I see a specification
http://spinroot.com/spin/Man/inline.html
A whole array looks to be passed for me.
Could you tell me which I shouldn't pass a whole array in current version?
(To pass a whole array is so useful.)
If I can use it with the error message, is there anything I should take care of?
Thank you for the reply. I seemed to remember it wrong.
I remember that Promela in a previous version had a limit "256"
of the number of array members, which I confirmed it to see
pangen(?).c. But, Spin 6.2.6 seems to be able to generate pan.c
and pan from a Prolema code including arrays of a huge number of
members.
I cannot find any description about the limit in Changelog and
source codes in version 6.2.6. Could you tell me whether the
limit is removed or not? I would like to confirm that the pan.c
and pan are generated correctly.
Pages: 1