Posts by Mara

Mara · General

Sorry if I insist, but the generated counterexamples are not in the final states. Only three counterexamples are generated at timeout, since in this model only three deadlock (final) states exist.

However, the assert is fired also in non-deadlock conditions, and this is really strange, since the instruction
timeout -> assert(..)
in my understanding should be fired ONLY at timeout not ALSO at timeout. Indeed, if you run the program searching for assert violations you obtain also the errors that are not corresponding to the timeout condition, i.e. the assert is fired also when the system is not in the deadlock state, and generates counterexample in all the intermediate states that lead to the deadlock ones.

I hope that I have been more clear on what I would like to know. I don't want to know why the assert is fired at timeout, I understand that the surrounding atomic clause is ignored at timeout, to avoid the deadlock. But I do not understand why the assert is executed also when timeout is false and the instruction timeout -> assert(..) should not be executed.

Thank you very much for your patience,

Mara

Mara · General

Ok, and this explains why the timeout is fired also inside the atomic sequence, even if it is blocked.

However it is still not clear to me why it generates as many counterexample as if the timeout was not there.
I mean, if you remove the timeout, you obtain 658 counterexamples, that are generated in the intermediate states between the initial and the final (i.e. timeout) ones.
And if you put the timeout clause directly into the do cycle, you obtain only the 3 counterexamples corresponding to the final, timeout states.

So, why the assert is executed also in all the intermediate states if there is the timeout guard before?

Sorry if I insist, but reasoning in Promela is quite different than reasoning in a "normal" imperative language.

Thank you, very much

Mara

Mara · General

Dear Spin Gurus,
I wrote a Promela program in which I placed into an atomic instruction some variable modification. Since I wanted to generate as much counterexamples as possible for the invariant (LC00007 <= 2) I placed, as I usually do, an assert clause right after the variable modifications.
If I execute the program I obtain 658 traces.

After I wanted to check the same invariant at timeout. I (erroneously) placed the timeout clause just before the assert, as shown in the code below. I know that the best way to do it is placing it as an alternative choice in the do clause, but I decided to see what was coming out from this.

I was expecting to find nothing: since each timeout is in a guarded sequence that will not be executable at timeout I expected that the timeout should never be fired.
At my surprise, this program generates exactly the same traces of the one without the timeout.
How is it possible? What I'm missing? Why the sequence
timeout -> assert (LC00007 <= 2)
is executed also when the timeout clause is false?

Please help me in understanding what I'm missing.
Mara

/* THE (GLOBAL) VARIABLES*/
 byte LC00001 = 2;
 byte LC00002 = 0;
 byte LC00003 = 2;
 byte LC00004 = 2;
 byte LC00005 = 2;
 byte LC00006 = 2;
 byte LC00007 = 2;

/* */

proctype R_proc()
	{
	do
	:: atomic{((LC00001 > 0))  -> (LC00001=LC00001-1; LC00002=LC00002+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 1: 1 LC00001-->1 LC00002*/
	:: atomic{((LC00002 > 0))  -> (LC00002=LC00002-1; LC00003=LC00003+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 2: 1 LC00002-->1 LC00003*/
	:: atomic{((LC00003 > 0) && (LC00004 > 0))  -> (LC00003=LC00003-1; LC00004=LC00004-1; LC00005=LC00005+1; LC00006=LC00006+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 3: 1 LC00003 + 1 LC00004-->1 LC00005+1 LC00006*/
	:: atomic{((LC00005 > 0))  -> (LC00005=LC00005-1; LC00003=LC00003+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 4: 1 LC00005-->1 LC00003*/
	:: atomic{((LC00003 > 0))  -> (LC00003=LC00003-1; LC00007=LC00007+1; timeout -> assert (LC00007 <= 2))} /* REACTION NUMBER 5: 1 LC00003-->1 LC00007*/

	od
	}

	
/* start the process*/
	init{
			run R_proc()
	}

Mara · General

Thank you very much!!

Mara · General

I'm also very interested in it: we perform verification on very large models using a swarm approach based essentially on randomized searches. I noticed that sometimes the searches were not terminating, and remained stuck for days. I decided to write you to ask your opinion, but I'm lucky and I already get the answer. However it would be very nice if the bug will be fixed ASAP.
Thank you

Mara

Mara · General

Yes, you were right, I can control the behaviour of the remaining scripts simply compiling swarm with the -e flag. But as you pointed out, the already running ones are not affected.
Thank you, as usual
Mara

Mara · General

Hi all!
I'm using swarm to perform the verification of a very large model. I was expecting that when a trail file (i.e. a counterexample) was found all the executions should stop.
But this is not happening. This is a little weird, because if I specify 10h of search, and I'm done after 3 hours why keep searching?
Is there some parameters that I can change to change the swarm behaviour? If not, are you planning to modify swarm in this sense? Or I have to manually modify the .pml.swarm file manually to manage this situation (for instance checking for the presence of trail file as a condition to break the execution wait loop)?

Thank you

Mara

Mara · General

Thank you very much for the answer! I will try separating the compilation part from the execution part (but I still think that a parallel-safe version of Spin/Swarm would be of great interest).

Mara · General

Dear Spin experts,
I've run into an error message during the run of a bunch of swarm jobs. I am on a cluster and so I can run several swarm jobs at the same time. I already know that I have to use different directories for each spin call (i.e for each swarm job) and so I did. But if I try to run together all the jobs, for some of them I get the error message I attach below. Please note that if I run the single swarm job alone I don't get any error message.
My hypothesis is that maybe, when running a huge amount (about 1500) of swarm jobs each of them generating the pan.* files, some kind of race conditions happens in the access to some library or similar. I would like to hear your opinion on that... maybe there is something that I'm missing?
BTW, are you planning to release a parallel-safe version of Spin in the future?

Thanks,
Mara

here begins the error, is only a (very) small part of the whole output:

In file included from /usr/include/stdio.h:28,
                 from pan.c:7:
/usr/include/features.h:361:25: error: /usr/include/sys/cdefs.h: Input/output error
In file included from /usr/include/stdio.h:34,
                 from pan.c:7:
/usr/lib/gcc/x86_64-redhat-linux/4.4.7/include/stddef.h:211: error: expected '=', ',', ';', 'asm' or '__attribute__' before 'ty
pedef'
In file included from pan.c:7:
/usr/include/stdio.h:49: error: expected '=', ',', ';', 'asm' or '__attribute__' before 'typedef'
/usr/include/stdio.h:54: error: expected '=', ',', ';', 'asm' or '__attribute__' before '__USING_NAMESPACE_STD'
In file included from /usr/include/stdio.h:75,
                 from pan.c:7:
/usr/include/libio.h:332: error: expected specifier-qualifier-list before 'size_t'
/usr/include/libio.h:364: error: expected declaration specifiers or '...' before 'size_t'
/usr/include/libio.h:373: error: expected declaration specifiers or '...' before 'size_t'
/usr/include/libio.h: In function '_IO_feof':
/usr/include/libio.h:462: error: expected declaration specifiers before '__THROW'
/usr/include/libio.h:463: error: expected '=', ',', ';', 'asm' or '__attribute__' before '__THROW'
/usr/include/libio.h:465: error: storage class specified for parameter '_IO_peekc_locked'
/usr/include/libio.h:471: error: expected '=', ',', ';', 'asm' or '__attribute__' before '__THROW'
/usr/include/libio.h:472: error: expected '=', ',', ';', 'asm' or '__attribute__' before '__THROW'
/usr/include/libio.h:473: error: expected '=', ',', ';', 'asm' or '__attribute__' before '__THROW'
/usr/include/libio.h:491: error: storage class specified for parameter '_IO_vfscanf'
/usr/include/libio.h:493: error: storage class specified for parameter '_IO_vfprintf'
/usr/include/libio.h:494: error: storage class specified for parameter '_IO_padn'
/usr/include/libio.h:495: error: expected '=', ',', ';', 'asm' or '__attribute__' before '_IO_sgetn'
/usr/include/libio.h:497: error: storage class specified for parameter '_IO_seekoff'
/usr/include/libio.h:498: error: storage class specified for parameter '_IO_seekpos'
/usr/include/libio.h:500: error: expected '=', ',', ';', 'asm' or '__attribute__' before '__THROW'

Mara · General

Yes, creating a different directory is the only way.
Thank you very much for the answer

Mara

Mara · General

Hi all!
I'm trying to convert a huge amount of trail files, all contained in a single directory, and I'm working in a distributed environment.

I was simply calling spin in this way, for each trail:

spin -p -k trail_name.trail -c pml_pgm_name.pml > txt_trail_file_name.txt

However, when working with different concurrent jobs, these translation fails, because different jobs may call spin at the same time, generating different pan files overwriting each other.

So my question is: there exist a compilation option that allows to change the name pan to something else?

Thank you very much,
Mara

Mara · General

Perfect. Thank you again!

Mara · General

Thank you for all the support!

Mara

Mara · General

Hi all again,
forgive me, but I have another question. I'm running my model in bitstate mode:

gcc -o pan pan.c -DNOFAIR -DSAFETY -DBITSTATE -DSPACE -DUSE_DISK -DSC -DMEMLIM=8192 -DVMAX=88
pan -E -e -v -w27

The verification is going, but I got the message
pan: warning, stack incomplete
what does it mean? Is there some parameter I did not correctly specified?

Thank you

Mara

Mara · General

Thank you very much for your extensive attention!
This is really a delicate point. At the moment I'm simply checking an invariant (an assert) at timeout. The idea behind it, is that I'm interested in the biggest number of counterexamples, since they can contain biologically "normal" execution and "strange" (interesting) ones. From here my need of "all" traces. Having the possibility of indicating how much often a "strange" execution occurs would have be for me really important. I think that I'll explore the bitstate option, as you suggest.

In the meantime - I report it for the sake of chronicle - I 've tried using the minimal automata representation....it is very very very slow, but until now is not run out of memory.

I'll try also to simplify the model, but I think the only space left for this, in my case, is reducing the initial values of my variables. This should have a sensible effect on the states to explore, right?

Thank you again,
Mara

Mara · General

Hi, thank you for your answers!

I tried with this reduced version of my pml program, and still gives me the same messages.
BTW, I have checked my shared memory (I had already followed the instruction on the site) and is kernel.shmmax = 8589934592, confirmed also by the message in first error cpu00: largest shared memory segment: 8160 MB . I can change it up to 14Gb, ma I have no more than this. Is this quantity you're referring to or mabe you're talking about the 672.033 total shared memory usage?
Thank you again

Mara
Here follows the code (this is a reduced version, i removed a lot of atomic steps, but I did not removed all the contained variables, so the variable list is bigger than the really needed one.)

 byte HC00011_c = 5;
 byte HC00011_s = 10; 
 byte HC00012_c = 5; 
 byte HC00013_c = 5;
 byte HC00014_c = 5;
 byte HC00015_c = 5;
 byte HC00016_c = 5;
 byte HC00017_c = 10;
 byte HC00017_s = 5;
 byte HC00018_c = 10;
 byte HC00019_c = 10;
 byte HC00021_b = 5;
 byte HC00021_c = 5; 
 byte HC00023_c = 5;
 byte HC00023_n = 5;
 byte HC00032_c = 5;
 byte HC00032_p = 5;
 byte HC00034_c = 5;
 byte HC00036_c = 5;
 byte HC00040_c = 5;
 byte HC00040_s = 10;
 byte HC00045_c = 5;
 byte HC00056_c = 5;
 byte HC00066_c = 5;
 byte HC00066_n = 5;
 byte HC00068_c = 5;
 byte HC00083_c = 5;
 byte HC00083_p = 5;
 byte HC00088_c = 5;
 byte HC00094_c = 5;
 byte HC00097_c = 5;
 byte HC00102_c = 5;
 byte HC00109_c = 5;
 byte HC00116_c = 5;
 byte HC00125_c = 5;
 byte HC00126_c = 5;
 byte HC00126_n = 5;
 byte HC00140_c = 5;
 byte HC00163_c = 5;
 byte HC00186_c = 5;
 byte HC00212_c = 5;
 byte HC00214_c = 5;
 byte HC00235_c = 5;
 byte HC00244_c = 5;
 byte HC00244_n = 5;
 byte HC00360_c = 5;
 byte HC00436_c = 5;
 byte HC00460_c = 5;
 byte HC00662_c = 5;
 byte HC01115_c = 5;
 byte HC01162_c = 5;
 byte HC01522_c = 5;
 byte HC02129_c = 5;

/*
Only two processes are generated.
proctype R_proc contains all the reactions, 
proctype assert_proc contains the assert invariant to be checked
*/

proctype R_proc()
	{
	do
	:: atomic{((HC00014_c > 0) && (HC00125_c > 0))  -> HC00014_c=HC00014_c-1; HC00125_c=HC00125_c-1; HC00013_c=HC00013_c+1; HC00056_c=HC00056_c+2} /* REACTION NUMBER 21: 1 HC00014_c + 1 HC00125_c-->1 HC00013_c+2 HC00056_c*/
	:: atomic{((HC00036_c > 0) && (HC00056_c > 1))  -> HC00036_c=HC00036_c-1; HC00056_c=HC00056_c-2; HC00011_c=HC00011_c+2; HC00125_c=HC00125_c+1} /* REACTION NUMBER 87: 1 HC00036_c + 2 HC00056_c-->2 HC00011_c+1 HC00125_c*/
	:: atomic{((HC00094_c > 0))  -> HC00094_c=HC00094_c-1; HC00088_c=HC00088_c+1} /* REACTION NUMBER 192: 1 HC00094_c-->1 HC00088_c*/
	:: atomic{((HC00012_c > 0) && (HC00097_c > 0))  -> HC00012_c=HC00012_c-1; HC00097_c=HC00097_c-1; HC00018_c=HC00018_c+1; HC00662_c=HC00662_c+1} /* REACTION NUMBER 206: 1 HC00012_c + 1 HC00097_c-->1 HC00018_c+1 HC00662_c*/
	:: atomic{((HC00015_c > 0) && (HC00021_c > 0) && (HC00102_c > 0))  -> HC00015_c=HC00015_c-1; HC00021_c=HC00021_c-1; HC00102_c=HC00102_c-1; HC00011_c=HC00011_c+1; HC00016_c=HC00016_c+1; HC00212_c=HC00212_c+1} /* REACTION NUMBER 227: 1 HC00015_c + 1 HC00021_c + 1 HC00102_c-->1 HC00011_c+1 HC00016_c+1 HC00212_c*/
	:: atomic{((HC00011_c > 0) && (HC00045_c > 0) && (HC00140_c > 0))  -> HC00011_c=HC00011_c-1; HC00045_c=HC00045_c-1; HC00140_c=HC00140_c-1; HC00068_c=HC00068_c+1; HC00102_c=HC00102_c+1} /* REACTION NUMBER 230: 1 HC00011_c + 1 HC00045_c + 1 HC00140_c-->1 HC00068_c+1 HC00102_c*/
	:: atomic{((HC00109_c > 0))  -> HC00109_c=HC00109_c-1; HC00116_c=HC00116_c+1} /* REACTION NUMBER 243: 1 HC00109_c-->1 HC00116_c*/
	:: atomic{((HC00013_c > 0) && (HC00019_c > 0) && (HC00116_c > 0))  -> HC00013_c=HC00013_c-1; HC00019_c=HC00019_c-1; HC00116_c=HC00116_c-1; HC00014_c=HC00014_c+1; HC00214_c=HC00214_c+1} /* REACTION NUMBER 253: 1 HC00013_c + 1 HC00019_c + 1 HC00116_c-->1 HC00014_c+1 HC00214_c*/
	:: atomic{((HC00014_c > 0) && (HC00017_c > 0) && (HC00126_c > 0))  -> HC00014_c=HC00014_c-1; HC00017_c=HC00017_c-1; HC00126_c=HC00126_c-1; HC00011_c=HC00011_c+1; HC00013_c=HC00013_c+1; HC01162_c=HC01162_c+1} /* REACTION NUMBER 267: 1 HC00014_c + 1 HC00017_c + 1 HC00126_c-->1 HC00011_c+1 HC00013_c+1 HC01162_c*/
	:: atomic{((HC00066_n > 0) && (HC00244_n > 0))  -> HC00066_n=HC00066_n-1; HC00244_n=HC00244_n-1; HC00023_n=HC00023_n+1; HC00126_n=HC00126_n+1} /* REACTION NUMBER 269: 1 HC00066_n + 1 HC00244_n-->1 HC00023_n+1 HC00126_n*/
	:: atomic{((HC00015_c > 0) && (HC00360_c > 0))  -> HC00015_c=HC00015_c-1; HC00360_c=HC00360_c-1; HC00016_c=HC00016_c+1; HC00140_c=HC00140_c+1} /* REACTION NUMBER 293: 1 HC00015_c + 1 HC00360_c-->1 HC00016_c+1 HC00140_c*/
	od
	}

proctype assert_proc()
{

	timeout -> assert(HC00012_c < 6);
}


	
/* start the two processes*/
	init{
			atomic{run R_proc(); run assert_proc();}
	}

Mara · General

Thank you for your answer, as always.
I'm just thinking:

1) when I'm not using an approximated approach, and when Spin does not block at the first counterexample, I assumed that - theoretically speaking, without memory and time constraints - it would be able to explore the whole computation space. And while doing this, it will provide me all the traces. So, is this assumption wrong?

And if it is wrong (and this maybe is connected with my other question about the measure of the portion of the explored space) is possible to know how Spin behaves during the generation of the counterexamples? Can you maybe direct me to a paper or publication in which I can find details about this subject?

2) If I got it well, I have no hope of getting benefit from a multicore machine since the problem is inherently connected with the dimension of the computation space of my model. So it's better to use one single core with all the available memory, independently from the storage model or the hashing method. Is this right

3) You're suggesting me to use an approximate hashing methods, that is not guaranteed to find some counteraxmples. Also in this case is there no measure of the portion of computation space that is spanned? Is there same literature on the subject?

I know that I'm asking "strange" things and doing a "strange" use of Spin, but I'm working on verification of biological models that really differs from the ones Spin was designed to.

Thank you very much for all attention

Mara

Mara · General

Hi,
thank you very much for your answer. I read of the -DBFS_DISK otion on the online page:
http://spinroot.com/spin/multicore/bfs.html
in the section New Directives. Maybe will be useful to specify also there that this option is not yet supported.
BTW the link Preprint of Spin 2012 Workshop paper in the same page is broken. Is this paper downloadable elsewere?
Thank you

Mara

Mara · General

Hi again.
I'm trying to run my verification qith the BFS approach on a multicore machine.

gcc -o pan pan.c -O2 -DBFS_PAR -DNOFAIR -DSAFETY -DBFS_DISK
./pan -E -e -v -u4

The message I get is "diskread: No space left on device" (see below for details).
If instead I specify the DMEMLIM flag

gcc -o pan pan.c -O2 -DBFS_PAR -DMEMLIM=2048 -DNOFAIR -DSAFETY -DBFS_DISK
./pan -E -e -v -u4

I get another error: "diskread: No such file or directory" (see 2nd error, below, for details).

What I'm doing wrong?
Thank you VERY MUCH for all the answers,

Mara

--------- first error
cpu00: largest shared memory segment: 8160 MB
pan: using 4 cores
diskread: No space left on device
cpu03: pan:1: aborting (at depth 0)
cpu03: stop (bfs_Uerror)
cpu00: states sent 1 recvd 0 stored 1 sleeps: 0, 0, 761
cpu01: stop (early termination)
cpu02: stop (early termination)

(Spin Version 6.2.2 -- 6 June 2012)
+ Multi-Core (using 4 cores)
+ Breadth-First Search
+ Partial Order Reduction

Hash-Compact 4 search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by -E flag)

State-vector 68 byte, depth reached 0, errors: 1
1 states, stored
1 nominal states (stored-atomic)
0 states, matched
1 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
128.000 shared memory used for hash table (-w24)
0.391 total non-shared memory usage

672.033 total shared memory usage

------------------------ second error
gcc -o pan pan.c -O2 -DBFS_PAR -DMEMLIM=2048 -DNOFAIR -DSAFETY -DBFS_DISK
./pan -E -e -v -u4
cpu00: largest shared memory segment: 2048 MB
pan: using 4 cores
diskread: No such file or directory
cpu03: pan:1: aborting (at depth 0)
cpu03: stop (bfs_Uerror)
cpu00: states sent 1 recvd 0 stored 1 sleeps: 0, 0, 1834
cpu01: stop (early termination)
cpu02: stop (early termination)

(Spin Version 6.2.2 -- 6 June 2012)
+ Multi-Core (using 4 cores)
+ Breadth-First Search
+ Partial Order Reduction

Hash-Compact 4 search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states - (disabled by -E flag)

State-vector 68 byte, depth reached 0, errors: 1
1 states, stored
1 nominal states (stored-atomic)
0 states, matched
1 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
128.000 shared memory used for hash table (-w24)
0.391 total non-shared memory usage

672.033 total shared memory usage

Mara · General

Hi all,
I'm trying to run my verification on a multicore machine (11Gb of free RAM, 8 cores). I've changed the shmmax and shmall as suggested on spin website.
And then:

gcc -o pan pan.c -DMEMLIM=8192 -DNOFAIR -DSAFETY -DNCORE=4 -DVMAX=88 -DUSE_DISK -DFULL_TRAIL -DCOLLAPSE
pan -E -e -v -w27

I need the full traces, and I need all the traces. The -DVMAX=88 is suggested by pan.

When I compile pan without the -DUSE_DISK flag, the memory is very rapidly consumed, so I specified -DUSE_DISK flag. The point is that 70Gb of disk memory are very fast consumed, without providing me with better results (in terms of obtained traces and portion of explored tree) than a single processor run with only 2Gb RAM!
I tried specifying the -DCOLLAPSE flag, but no sensible changes happens.

Is there something that I'm missing in memory or flags specification? Or is this the normal behavior due to overhead of multicore run?
Thanks in advance for your attention

Mara

---------------------------------------------

cpu0: step 0: -DMEMLIM=8192 Mb minus hashtable+workqs (1024 + 128.043 Mb) leaves 7039.33 Mb
cpu0: step 1: allocate shared hastable 1024 Mb
cpu0: step 2: pre-allocate shared state memory 7039.33 Mb
cpu0: setting segsize to 1759.83 MB
cpu0: step 2+: pre-allocate memory arena 0 of 1.8e+03 Mb
cpu0: step 2+: pre-allocate memory arena 1 of 1.8e+03 Mb
cpu0: step 2+: pre-allocate memory arena 2 of 1.8e+03 Mb
cpu0: step 2+: pre-allocate memory arena 3 of 1.8e+03 Mb
cpu0: step 3: allocate shared workqueues 128.043 MB
cpu0: step 4: calling fork()
cpu1: starting core_id 1 -- pid 27806
cpu0: starting core_id 0 -- pid 27805
cpu0: local heap 1759 MB
cpu2: starting core_id 2 -- pid 27807
cpu2: local heap 1759 MB
cpu3: starting core_id 3 -- pid 27808
cpu1: local heap 1759 MB
cpu3: local heap 1759 MB
cpu0: created temporary diskfile Q000_000.tmp
cpu2: created temporary diskfile Q000_002.tmp
cpu3: created temporary diskfile Q000_003.tmp
cpu1: created temporary diskfile Q000_001.tmp
cpu0: created temporary diskfile Q001_000.tmp
cpu2: created temporary diskfile Q001_002.tmp
cpu3: created temporary diskfile Q001_003.tmp
cpu1: created temporary diskfile Q001_001.tmp
cpu0: created temporary diskfile Q002_000.tmp
cpu2: created temporary diskfile Q002_002.tmp
cpu3: created temporary diskfile Q002_003.tmp
cpu1: created temporary diskfile Q002_001.tmp
cpu0: created temporary diskfile Q003_000.tmp
cpu2: created temporary diskfile Q003_002.tmp
cpu1: created temporary diskfile Q003_001.tmp
cpu3: created temporary diskfile Q003_003.tmp
cpu0: created temporary diskfile Q004_000.tmp
cpu1: created temporary diskfile Q004_001.tmp
cpu2: created temporary diskfile Q004_002.tmp
cpu2: created temporary diskfile Q005_002.tmp
cpu0: created temporary diskfile Q005_000.tmp
cpu3: created temporary diskfile Q004_003.tmp
cpu1: created temporary diskfile Q005_001.tmp
cpu3: created temporary diskfile Q005_003.tmp
cpu2: created temporary diskfile Q006_002.tmp
cpu0: created temporary diskfile Q006_000.tmp
cpu1: created temporary diskfile Q006_001.tmp
cpu3: created temporary diskfile Q006_003.tmp
cpu2: created temporary diskfile Q007_002.tmp
cpu0: created temporary diskfile Q007_000.tmp
cpu3: created temporary diskfile Q007_003.tmp
cpu2: created temporary diskfile Q008_002.tmp
cpu0: created temporary diskfile Q008_000.tmp
cpu1: created temporary diskfile Q007_001.tmp
cpu3: created temporary diskfile Q008_003.tmp
cpu2: created temporary diskfile Q009_002.tmp
cpu1: created temporary diskfile Q008_001.tmp
cpu0: created temporary diskfile Q009_000.tmp
cpu3: created temporary diskfile Q009_003.tmp
cpu0: created temporary diskfile Q010_000.tmp
cpu1: created temporary diskfile Q009_001.tmp
cpu2: created temporary diskfile Q010_002.tmp
cpu3: created temporary diskfile Q010_003.tmp
cpu1: created temporary diskfile Q010_001.tmp
cpu0: created temporary diskfile Q011_000.tmp
cpu2: created temporary diskfile Q011_002.tmp
cpu3: created temporary diskfile Q011_003.tmp
cpu1: created temporary diskfile Q011_001.tmp
cpu0: created temporary diskfile Q012_000.tmp
cpu2: created temporary diskfile Q012_002.tmp
cpu3: created temporary diskfile Q012_003.tmp
cpu1: created temporary diskfile Q012_001.tmp
cpu0: created temporary diskfile Q013_000.tmp
cpu3: created temporary diskfile Q013_003.tmp
cpu2: created temporary diskfile Q013_002.tmp
cpu0: created temporary diskfile Q014_000.tmp
cpu1: created temporary diskfile Q013_001.tmp
cpu3: created temporary diskfile Q014_003.tmp
cpu2: created temporary diskfile Q014_002.tmp
cpu0: created temporary diskfile Q015_000.tmp
cpu1: created temporary diskfile Q014_001.tmp
cpu3: created temporary diskfile Q015_003.tmp
cpu2: created temporary diskfile Q015_002.tmp
cpu1: created temporary diskfile Q015_001.tmp
cpu0: created temporary diskfile Q016_000.tmp
cpu3: created temporary diskfile Q016_003.tmp
cpu2: created temporary diskfile Q016_002.tmp
cpu3: created temporary diskfile Q017_003.tmp
cpu0: created temporary diskfile Q017_000.tmp
cpu2: created temporary diskfile Q017_002.tmp
cpu1: created temporary diskfile Q016_001.tmp
cpu0: created temporary diskfile Q018_000.tmp
cpu3: created temporary diskfile Q018_003.tmp
cpu1: created temporary diskfile Q017_001.tmp
cpu2: created temporary diskfile Q018_002.tmp
cpu0: created temporary diskfile Q019_000.tmp
cpu1: created temporary diskfile Q018_001.tmp
cpu3: created temporary diskfile Q019_003.tmp
cpu2: created temporary diskfile Q019_002.tmp
cpu2: Depth= 40 States= 1e+06 Transitions= 4.74e+06 Memory= 106.812 t= 365 R= 3e+03
cpu3: Depth= 40 States= 1e+06 Transitions= 4.78e+06 Memory= 106.812 t= 374 R= 3e+03
cpu0: created temporary diskfile Q020_000.tmp
cpu1: Depth= 40 States= 1e+06 Transitions= 5.1e+06 Memory= 106.812 t= 379 R= 3e+03
cpu3: created temporary diskfile Q020_003.tmp
cpu2: created temporary diskfile Q020_002.tmp
cpu1: created temporary diskfile Q019_001.tmp
cpu0: created temporary diskfile Q021_000.tmp
cpu3: created temporary diskfile Q021_003.tmp
cpu1: created temporary diskfile Q020_001.tmp
cpu2: created temporary diskfile Q021_002.tmp
cpu0: created temporary diskfile Q022_000.tmp
cpu2: created temporary diskfile Q022_002.tmp
cpu3: created temporary diskfile Q022_003.tmp
cpu1: created temporary diskfile Q021_001.tmp
cpu0: created temporary diskfile Q023_000.tmp
cpu2: created temporary diskfile Q023_002.tmp
cpu1: created temporary diskfile Q022_001.tmp
cpu3: created temporary diskfile Q023_003.tmp
cpu0: created temporary diskfile Q024_000.tmp
cpu2: created temporary diskfile Q024_002.tmp
cpu1: created temporary diskfile Q023_001.tmp
cpu3: created temporary diskfile Q024_003.tmp
cpu0: Depth= 20 States= 1e+06 Transitions= 4.32e+06 Memory= 1259.486 t= 474 R= 2e+03
cpu1: created temporary diskfile Q024_001.tmp
cpu3: created temporary diskfile Q025_003.tmp
cpu0: created temporary diskfile Q025_000.tmp
cpu2: created temporary diskfile Q025_002.tmp
cpu0: created temporary diskfile Q026_000.tmp
cpu1: created temporary diskfile Q025_001.tmp
cpu2: created temporary diskfile Q026_002.tmp
cpu3: created temporary diskfile Q026_003.tmp
cpu0: created temporary diskfile Q027_000.tmp
cpu1: created temporary diskfile Q026_001.tmp
cpu2: created temporary diskfile Q027_002.tmp
cpu3: created temporary diskfile Q027_003.tmp
cpu0: created temporary diskfile Q028_000.tmp
cpu1: created temporary diskfile Q027_001.tmp
cpu2: created temporary diskfile Q028_002.tmp
cpu3: created temporary diskfile Q028_003.tmp
cpu0: created temporary diskfile Q029_000.tmp
cpu1: created temporary diskfile Q028_001.tmp
cpu2: created temporary diskfile Q029_002.tmp
cpu3: created temporary diskfile Q029_003.tmp
cpu0: created temporary diskfile Q030_000.tmp
cpu1: created temporary diskfile Q029_001.tmp
cpu3: created temporary diskfile Q030_003.tmp
cpu2: created temporary diskfile Q030_002.tmp
cpu1: created temporary diskfile Q030_001.tmp
cpu0: created temporary diskfile Q031_000.tmp
cpu2: created temporary diskfile Q031_002.tmp
cpu3: created temporary diskfile Q031_003.tmp
cpu1: created temporary diskfile Q031_001.tmp
cpu0: created temporary diskfile Q032_000.tmp
cpu3: created temporary diskfile Q032_003.tmp
cpu2: created temporary diskfile Q032_002.tmp
cpu0: created temporary diskfile Q033_000.tmp
cpu1: created temporary diskfile Q032_001.tmp
cpu2: created temporary diskfile Q033_002.tmp
cpu3: created temporary diskfile Q033_003.tmp
cpu0: created temporary diskfile Q034_000.tmp
cpu2: created temporary diskfile Q034_002.tmp
cpu1: created temporary diskfile Q033_001.tmp
cpu3: created temporary diskfile Q034_003.tmp
cpu0: created temporary diskfile Q035_000.tmp
cpu2: created temporary diskfile Q035_002.tmp
cpu1: created temporary diskfile Q034_001.tmp
cpu3: created temporary diskfile Q035_003.tmp
cpu0: created temporary diskfile Q036_000.tmp
cpu2: created temporary diskfile Q036_002.tmp
cpu1: created temporary diskfile Q035_001.tmp
cpu3: created temporary diskfile Q036_003.tmp
cpu0: created temporary diskfile Q037_000.tmp
cpu1: created temporary diskfile Q036_001.tmp
cpu2: created temporary diskfile Q037_002.tmp
cpu1: pan:1: aborting -- disk write failed (disk full?) (at depth 41)
cpu2: pan:1: aborting --pan: wrote prova_meta1_low_values.pml1.trail
cpu0: pan: wrote trailfile
pan: wrote prova_meta1_low_values.pml1.cpu1_trail
cpu1: pan: wrote trailfile
pan: wrote prova_meta1_low_values.pml1.cpu2_trail
cpu2: pan: wrote trailfile
cpu1: stop - Uerror
cpu1: termination initiated (4)
cpu1: wrapup -- 1 error(s)
cpu0: stop - Uerror
cpu0: termination initiated (4)
cpu0: wrapup -- 1 error(s)
cpu2: stop - Uerror
cpu2: termination initiated (4)
cpu2:
(Spin Version 6.2.2 cpu1: dsk_written 36120271 states in 37 files
cpu1: dsk_drained 0 states
cpu2: dsk_written 37095175 states in 38 files
cpu2: dsk_drained 0 states
1512419 states, stored
5484542 states, matched
6996961 transitions (= stored+matched)
1 atomic steps
hash conflicts: 221721 (resolved)

Stats on memory usage (in Megabytes):
150.005 equivalent memory usage for states (stored*(State-vector + overhead))
7039.325 shared memory reserved for state storage
in 4 local heaps of 1759.831 MB each

161.642 actual memory usage for states
1024.000 memory used for hash table (-w27)
0.534 memory used for DFS stack (-m10000)
128.043 shared memory used for work-queues
in 4 queues of 0.011 MB each + a global q of 128.000 MB
1314.219 total actual memory usage

nr of templates: [ 0:globals 1:chans 2:procs ]
collapse counts: [ 0:7373641 2:1 3:1 4:2 ]
unreached in proctype R_proc
prova_meta1_low_values.pml:104, state 199, "-end-"
(1 of 199 states)
unreached in proctype assert_proc
prova_meta1_low_values.pml:109, state 2, "assert((HC00012_c<6))"
prova_meta1_low_values.pml:110, state 3, "-end-"
(2 of 3 states)
unreached in init
(0 of 4 states)
cpu0: dsk_written 37419599 states in 38 files
cpu0: dsk_drained 0 states
cpu0: done, 0 Mb of shared state memory left
cpu0: done -- got 0 states from queue

cpu0: elapsed time 749 seconds (1.51242e+06 states visited)
cpu0: rate 2020.46 states/second

Mara · General

Hi to all!
I'm running the verification of my model, that use 53 byte variables and has 34 different instructions, executable or not depending on the value (of one or more) of the variables.
I'm searching for all the execution trails in which a simple assertion is not verified at timeout (i.e. I've got two processes running, the one with my instructions and another one with the timeout->assert() instruction). The assertion takes into account the value of a single variable being < predefined number.

Obviously the execution tree is huge, and since I need all the traces (i.e. all the counterexamples) in which my assert is not valid, I have a lot of issues with memory usage.
Hence I tried the minimal automaton representation compiling Pan with -DMA option.
My verification is still running after a day, and the verbose output reports:

Depth= 382 States= 1e+06 Transitions= 5.4e+06 Nodes= 9902 Memory= 0.929 t= 21.2 R= 5e+04
...
...
Depth= 446 States= 3.08e+09 Transitions= 2.32e+10 Nodes= 753462 Memory= 46.340 t= 8.67e+04 R= 4e+04
....

Now the questions:
1) the Depth of the search is always increasing? Or eventually in the future this value will decrease when backtracking? This will be a very loose indication of the time I should wait for the verification of the longest branches of the tree...

2) It is possible to "measure" the extent of the explored portion of the execution tree from the information on Depth, Transitions, and Nodes? It will be interesting knowing how much it has been exhaustively explored and what is the extent of the remaining part. It will be for me a "degree of confidence" on the obtained counterexamples.

Thanks in advance for your attention,

Mara

Mara · General

Thank you for your answer feng_lei_76, and thanks to the Spin team for the official answer.
If I get it correctly, the "problem" arise only for very complex systems, where the tree is so big that it's (quite) impossible do an exhaustive search. In that case the run order matters.

Thank you also for the suggestion on how rewrite the code !! It's really precious for me, also because gives me another solution: if I need to instantiate more than 255 reaction in this way I can.

Mara · General

Hi to all the community members!

I'm not so expert in model checking, and I'm trying to use Spin and Promela for modeling a metabolic network and verifying that some (simple) properties hold.
Each reaction between metabolites is represented as a distinct process that (atomically) reads and modifies the values of ( some of) the global variables (the metabolites).

I want to verify that the value of a variable (namely BM, in the code you find attached below) is always lower than a fixed value (in the example I report: BM < 15).
The ten processes corresponding to the ten reactions of my (toy) metabolic network are run in the init process.

BUT the really STRANGE thing is that the order in which the processes are RUN, changes deeply the response in SPIN, either using an assert (assert BM < 15) or using an LTL formula (always BM < 15).
Indeed if the init is:

{run R1(); run R2(); run R3(); run R4(); run R5(); run R6(); run R7(); run R8(); run R9(); run R10(); assert (BM < 15)}

the verification ends with a "Warning: Search not completed" and (the correct) assertion violation

In turn with this init:

{run R1(); run R4(); run R7(); run R9(); run R10(); run R2(); run R3(); run R5(); run R6(); run R8(); assert (BM < 15)}

the verification process ends without any error but with the message "Warning: Search not completed". I increased the memory but the result is the same. At the end I raised the memory up to 2048 Mb but after more than one hour I stopped the process (it was at the maximum of the memory usage, but not writing any line on the output screen. I decided to put everithing into an "atomic", and then to be sure that the assert is correctly interleaved I created a process for the assert and instantiated it (the code attached below is the latter version). Obviously the elaboration time increased but the results are the same. I tried also with an LTL formula, and the same happens.

How is it possible such a different behaviour? It seems that the order of the runs affects deeply the way in which the verification process is performed. Or there is something wrong that i don't get? And, b.t.w., why the process does not stop at the first error as specified in the Error Trapping Options, in the first case?.
Thanks in advance for your attention !

Mara

----------- code and info.

1) I'm using Spin Version 6.0.1 and iSpin 1.0.4 under Ubuntu 10.04
2) Here is the code (this is the one with the assert, but with LTL is exactly the same)

/* THE (GLOBAL) VARIABLES*/

int A = 40;
int F = 40;
int D = 40;
int E = 40;
int H = 40;
int O2 = 40;
int ATP = 20;
int B = 20;
int C = 20;
int NADH = 20;
int CA = 20;
int OXO = 20;
int BM = 0;

/* REACTION NUMBER 1: 1 A + 1 ATP-->1 B*/
proctype R1()
{ do
:: atomic{((A > 0) && (ATP > 0)) -> A=A-1; ATP=ATP-1; B=B+1}
od
}

/* REACTION NUMBER 2: 1 B-->2 ATP+2 C+3 NADH*/
proctype R2()
{ do
:: atomic{((B > 0)) -> B=B-1; ATP=ATP+2; C=C+2; NADH=NADH+3}
od
}

/* REACTION NUMBER 3: 1 B-->1 F*/
proctype R3()
{ do
:: atomic{((B > 0)) -> B=B-1; F=F+1}
od
}

/* REACTION NUMBER 4: 1 C + 1 OXO-->1 CA*/
proctype R4()
{ do
:: atomic{((C > 0) && (OXO > 0)) -> C=C-1; OXO=OXO-1; CA=CA+1}
od
}

/* REACTION NUMBER 5: 1 CA-->3 ATP+3 NADH+1 OXO*/
proctype R5()
{ do
:: atomic{((CA > 0)) -> CA=CA-1; ATP=ATP+3; NADH=NADH+3; OXO=OXO+1}
od
}

/* REACTION NUMBER 6: 1 C-->3 D+2 ATP*/
proctype R6()
{ do
:: atomic{((C > 0)) -> C=C-1; D=D+3; ATP=ATP+2}
od
}

/* REACTION NUMBER 7: 1 C + 4 NADH-->3 E*/
proctype R7()
{ do
:: atomic{((C > 0) && (NADH > 3)) -> C=C-1; NADH=NADH-4; E=E+3}
od
}

/* REACTION NUMBER 8: 1 ATP + 2 NADH + 1 CA-->1 H*/
proctype R8()
{ do
:: atomic{((ATP > 0) && (NADH > 1) && (CA > 0)) -> ATP=ATP-1; NADH=NADH-2; CA=CA-1; H=H+1}
od
}

/* REACTION NUMBER 9: 1 O2 + 1 NADH-->1 ATP*/
proctype R9()
{ do
:: atomic{((O2 > 0) && (NADH > 0)) -> O2=O2-1; NADH=NADH-1; ATP=ATP+1}
od
}

/* REACTION NUMBER 10: 1 F + 1 H + 10 ATP + 1 C-->1 BM*/
proctype R10()
{ do
:: atomic{((F > 0) && (H > 0) && (ATP > 9) && (C > 0)) -> F=F-1; H=H-1; ATP=ATP-10; C=C-1; BM=BM+1}
od
}

/* The assert we want to be verified. We forced it to be verified at the end (in deadlock state) */
proctype assert_proc()
{
timeout-> assert(BM < 15);
}

/* the init*/
init{

atomic{run R1(); run R2(); run R3(); run R4(); run R5(); run R6(); run R7(); run R8(); run R9(); run R10(); run assert_proc();}
}

3) Here the other one: