Spinroot

A forum for Spin users

You are not logged in.

#1 2012-05-31 06:20:48

Mara
Member
Registered: 2012-05-30
Posts: 24

Different order in the processes run make spin behave very different.

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:

/* 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 R4(); run R7(); run R9(); run R10(); run R2(); run R3(); run R5(); run R6(); run R8(); run assert_proc();}
}

4) Here the output for the version at point 2

spin -a  reaction_assert_v1.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -w -o pan pan.c
./pan -m10000  -E -c1
Pid: 3003
Depth=     231 States=    1e+06 Transitions= 5.27e+06 Memory=   116.954    t=   4.28 R=   2e+05
Depth=     235 States=    2e+06 Transitions= 1.11e+07 Memory=   231.407    t=   10.1 R=   2e+05
pan: resizing hashtable to -w21..  done
Depth=     238 States=    3e+06 Transitions= 1.72e+07 Memory=   353.469    t=   15.7 R=   2e+05
Depth=     239 States=    4e+06 Transitions= 2.31e+07 Memory=   467.922    t=   21.2 R=   2e+05
Depth=     241 States=    5e+06 Transitions= 2.95e+07 Memory=   582.376    t=   27.2 R=   2e+05
pan: resizing hashtable to -w23..  done
Depth=     242 States=    6e+06 Transitions= 3.55e+07 Memory=   726.876    t=     33 R=   2e+05
pan:1: assertion violated (BM<15) (at depth 234)
pan: wrote reaction_assert_v1.pml.trail

(Spin Version 6.0.1 -- 16 December 2010)
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    - (disabled by -E flag)

State-vector 108 byte, depth reached 242, errors: 1
  6234765 states, stored
30669043 states, matched
36903808 transitions (= stored+matched)
       10 atomic steps
hash conflicts:  28950632 (resolved)

  753.731    memory usage (Mbyte)


pan: elapsed time 34.1 seconds
To replay the error-trail, goto Simulate/Replay and select "Run"

5) Here the output for the version at point 3 (with 2048 Mb)

spin -a  reaction_assert_v2.pml
gcc -DMEMLIM=2048 -O2 -DXUSAFE -DSAFETY -w -o pan pan.c
./pan -m10000  -E
Pid: 3044
Depth=     218 States=    1e+06 Transitions= 5.18e+06 Memory=   116.954    t=   4.21 R=   2e+05
Depth=     221 States=    2e+06 Transitions=  1.1e+07 Memory=   231.407    t=   10.3 R=   2e+05
pan: resizing hashtable to -w21..  done
Depth=     222 States=    3e+06 Transitions= 1.67e+07 Memory=   353.469    t=   15.5 R=   2e+05
Depth=     224 States=    4e+06 Transitions= 2.29e+07 Memory=   467.922    t=   21.2 R=   2e+05
Depth=     225 States=    5e+06 Transitions=  2.9e+07 Memory=   582.376    t=   27.3 R=   2e+05
pan: resizing hashtable to -w23..  done
Depth=     226 States=    6e+06 Transitions= 3.53e+07 Memory=   726.876    t=   33.2 R=   2e+05
Depth=     226 States=    7e+06 Transitions= 4.11e+07 Memory=   841.426    t=   38.1 R=   2e+05
Depth=     226 States=    8e+06 Transitions= 4.73e+07 Memory=   955.879    t=   43.3 R=   2e+05
Depth=     227 States=    9e+06 Transitions= 5.36e+07 Memory=  1070.333    t=   48.8 R=   2e+05
Depth=     228 States=    1e+07 Transitions= 6.02e+07 Memory=  1184.883    t=   54.5 R=   2e+05
Depth=     228 States=  1.1e+07 Transitions= 6.66e+07 Memory=  1299.337    t=   60.4 R=   2e+05
Depth=     229 States=  1.2e+07 Transitions= 7.32e+07 Memory=  1413.790    t=   67.4 R=   2e+05
Depth=     229 States=  1.3e+07 Transitions= 7.98e+07 Memory=  1528.340    t=   76.3 R=   2e+05
Depth=     230 States=  1.4e+07 Transitions= 8.64e+07 Memory=  1642.794    t=   87.3 R=   2e+05
Depth=     230 States=  1.5e+07 Transitions= 9.22e+07 Memory=  1757.247    t=   98.5 R=   2e+05
Depth=     230 States=  1.6e+07 Transitions= 9.84e+07 Memory=  1871.797    t= 2.97e+03 R=   5e+03
Depth=     230 States=  1.7e+07 Transitions= 1.05e+08 Memory=  1986.251    t= 1.15e+04 R=   1e+03
pan: resizing hashtable to -w25.. pan: reached -DMEMLIM bound
    2.08273e+09 bytes used
    1.34218e+08 bytes more needed
    2.14748e+09 bytes limit
hint: to reduce memory, recompile with
  -DCOLLAPSE # good, fast compression, or
  -DMA=108   # better/slower compression, or
  -DHC # hash-compaction, approximation
  -DBITSTATE # supertrace, approximation

(Spin Version 6.0.1 -- 16 December 2010)
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    - (disabled by -E flag)

State-vector 108 byte, depth reached 230, errors: 0
17000000 states, stored
87765780 states, matched
1.0476578e+08 transitions (= stored+matched)
       10 atomic steps
hash conflicts:  81410885 (resolved)

1986.251    memory usage (Mbyte)


pan: elapsed time 1.15e+04 seconds
No errors found -- did you verify all claims?

Offline

#2 2012-05-31 09:54:29

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Different order in the processes run make spin behave very different.

I tested your code with SPIN 6.2.1 and had the same result as reported.

My understanding is that this is so large problem that exhaustive search is almost impossible. Even for the successful Promela model, if you try to search the shortest error trail by reducing the depth or using BFS, you will still get out of the memory.  It seems that the state-transition model of the problem is very wide as a great deal of possible transitions may occur at the state.

The order of initializing the processes does influence the searching computation, because the sequence of selecting the next executable statement is different.  Then the model checker needs to verify a lot of paths before it luckily hits the error state.

For the 2nd version of the Promela code, you can find the error with bitstate method.

Let's wait for the official answer from Spinroot.

Offline

#3 2012-05-31 21:44:18

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

Re: Different order in the processes run make spin behave very different.

yes, the order of process initialization can make a difference -- but only for models that cannot be verified exhaustively.  it determines where the search starts and how it proceeds.
by the way, in your case, because all transitions are basically atomic -- you could lower the complexity by combining all transitions in a single proctype:

proctype R()
    {    do
            :: atomic{((A > 0) && (ATP > 0))  -> A=A-1; ATP=ATP-1; B=B+1}    /* R1 */
            :: atomic{((B > 0))  -> B=B-1; ATP=ATP+2; C=C+2; NADH=NADH+3}    /* R2 */
            :: atomic{((B > 0))  -> B=B-1; F=F+1}     /* R3 */
            :: etc.....
        od
    }

Offline

#4 2012-06-01 09:04:14

Mara
Member
Registered: 2012-05-30
Posts: 24

Re: Different order in the processes run make spin behave very different.

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.

Offline

#5 2012-06-05 10:18:26

lz
Member
Registered: 2012-05-14
Posts: 9

Re: Different order in the processes run make spin behave very different.

Hello,

Is this a mistake or I misconfigured the verifier?
Normally the process M should not be executed before the end of H.
With my thanks, ...


byte cnt;
active proctype M() priority 5 {
   int temp;
   ...
   set_priority(0, get_priority(1));
   temp = cnt; temp++; cnt = temp;
}
active proctype H() priority 10 {
   int temp;
   temp = cnt; temp++; cnt = temp;
}
active proctype B() priority 1 {
   assert(_priority == 1 && cnt == 2);
}

spin -a  priorite1.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -DNOREDUCE -w -o pan pan.c
./pan -m10000  -E
Pid: 4584
pan:1: assertion violated ((_priority==1)&&(cnt==2)) (at depth 10)
pan: wrote priorite1.pml.trail

(Spin Version 6.2.1 -- 14 May 2012)

Offline

#6 2012-06-05 17:27:30

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

Re: Different order in the processes run make spin behave very different.

thanks for this very clear example.
you've hit a bug indeed
i'll prepare a fix for 6.2.2, and will add a note when the new version is available
thanks for the report!

Offline

#7 2012-09-25 11:24:04

BooBboff
Member
Registered: 2012-08-29
Posts: 1
Website

Re: Different order in the processes run make spin behave very different.

Infinite topic

Offline

Board footer

Powered by FluxBB