SPIN fails to find assertion violation with -run

[ericmercer]

Consider the following Promela:

init {
    run f()
}

active proctype f() {
    assert _pid == 1
}

The interpreter finds the assertion violation:

$ ./spin ../../../unexpected.pml
spin: ../../../unexpected.pml:6, Error: assertion violated
spin: text of failed assertion: assert((_pid==1))
#processes: 3
  2:    proc  2 (f:1) ../../../unexpected.pml:6 (state 1)
  2:    proc  1 (f:1) ../../../unexpected.pml:6 (state 1)
  2:    proc  0 (:init::1) ../../../unexpected.pml:3 (state 2) <valid end state>
3 processes created

But -run (-search) does not:

$ ./spin -run -safety ../../../unexpected.pml

(Spin Version 6.5.2 -- 21 June 2024)
        + 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 6, errors: 0
        7 states, stored
        0 states, matched
        7 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))
    0.292       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


unreached in init
        (0 of 2 states)
unreached in proctype f
        (0 of 2 states)

pan: elapsed time 0 seconds

I'm first found the issue on version 6.5.2 on a Visual Studio Code Python dev container (sudo apt install spin --assume-yes). I then recreated it with a build from source on this repository.

[ericmercer]

It occurred to me that the issue is likely related to the partial order reduction (maybe _pid isn't considered a dependency), so I tried spin -run -noreduce

$ spin -run -noreduce unexpected.pml
pan:1: assertion violated (_pid==1) (at depth 2)
pan: wrote unexpected.pml.trail

(Spin Version 6.5.2 -- 6 December 2019)
Warning: Search not completed

Full statespace search for:
        never claim             - (none specified)
        assertion violations    +
        cycle checks            - (disabled by -DSAFETY)
        invalid end states      +

State-vector 28 byte, depth reached 6, errors: 1
...

[nimble-code]

Yes, that was my first thought as well -- and I think you're right that the _pid number isn't considered a shared variable but a constant inside each process. Good to know. I'll keep it on a short list of things to look into when I get more time.

[c-kloukinas]

Should _pid be comparable to a constant in the first place? I'd have thought that all that's guaranteed is that running processes have different _pid's (that may be the same as some of processes that have terminated already).
Is there a reason to impose stricter constraints on it?