model-checkingpromelaspin

SPIN assert not triggered


I am trying to understand why the assert in this model isn't triggered.

ltl { !A@wa U B@sb && !B@wb U A@sa }

byte p = 0
byte q = 0
int  x = 0

inline signal(sem) { sem++ }
inline wait  (sem) { atomic { sem > 0 ; sem-- } }

proctype A() {
    x = 10*x + 1
    signal(p)
sa: wait(q)
wa: x = 10*x + 2
}

proctype B() {
    x = 10*x + 3
    signal(q)
sb: wait(p)
wb: x = 10*x + 4
}

init {
    atomic { run A(); run B() }
    _nr_pr == 1
    assert(x != 1324) 
}

Clearly, there is an order of operations that produces the final value x = 1324:


Solution

  • The assertion isn't triggered because it is "never reached" when the solver proves that the property

    ltl { !A@wa U B@sb && !B@wb U A@sa }
    

    is true.

    Take a look at the output that is given by the solver, it clearly states that:


    You can use the option -noclaim so to check the model only for the assertion, which is then easily proven false:

    ~$ spin -search -noclaim t.pml 
    ltl ltl_0: ((! ((A@wa))) U ((B@sb))) && ((! ((B@wb))) U ((A@sa)))
    pan:1: assertion violated (x!=1324) (at depth 13)
    pan: wrote t.pml.trail
    
    (Spin Version 6.4.8 -- 2 March 2018)
    Warning: Search not completed
        + Partial Order Reduction
    
    Full statespace search for:
        never claim             - (not selected)
        assertion violations    +
        cycle checks        - (disabled by -DSAFETY)
        invalid end states  +
    
    State-vector 36 byte, depth reached 15, errors: 1
           48 states, stored
            6 states, matched
           54 transitions (= stored+matched)
            1 atomic steps
    hash conflicts:         0 (resolved)
    
    Stats on memory usage (in Megabytes):
        0.003   equivalent memory usage for states (stored*(State-vector + overhead))
        0.286   actual memory usage for states
      128.000   memory used for hash table (-w24)
        0.534   memory used for DFS stack (-m10000)
      128.730   total actual memory usage
    
    
    
    pan: elapsed time 0 seconds