Model Checking: why does LTL logic "<>" not produce correct counter-example in Spin

Question

Update

There are two problems in my previous attempt. By fixing them I successfully get the expected answer.

• The LTL specified using the -f option from command line will be negated. Instead, I use the inline LTL by adding ltl { <> p} into the Promela program.

• Second, when executing pan, seems that we need to use -a to "find acceptance cycles". I'm not completely sure what this means, my guess is that Spin will try to identify infinite schedules.

Original Question

I'm new to model checking and Spin. I am having trouble with the following example.

• I specify the claim '<> p' that every schedule will eventually lead to p, in my case SUM > BOUND

• In my understanding, if there exist an infinite schedule that p is always false, in my case SUM is always less than or equal to BOUND, spin will report that as a counter example.

• However, when I run spin, the counter example I get is one that p is true.

Specifically, the commands, the Promela code and the trail are as follow.

In this trail, the result is that p is satisfied, as SUM is indeed bigger than BOUND. I could not understand why Spin give me an counter example that satisfies p?

./spin649_linux64 -f '<> p' -a sample.pml
gcc -o pan pan.c
./pan -i 
./spin649_linux64 -p -t sample.pml

#define UPDATE(c) if :: ch[c]>sz[c] -> sz[c] = ch[c] :: else fi
#define PRODUCE(c, n) ch[c] = ch[c] + n; UPDATE(c)
#define CONSUME(c, n) ch[c] = ch[c] - n
#define WAIT(c, n) ch[c] >= n

int ch[2]; int sz[2];

#define BOUND 6 
#define SUM (sz[0] + sz[1])
#define p (SUM > BOUND)

// Actor_a <==1==> Actor_b <==2==> Actor_c

// Actor_a produces 2 tokens to channel 1
// Actor_b consumes 3 tokens from channel 1 and produces 1 token to channel 2
// Actor_c consumes 2 tokens from channel 2
// sz[i] records the highest capacity seen for channel[i]
// There exist an infinite schedule that sz[0] + sz[1] is at most 6 at any moment

proctype Actor_a() {
  do 
  :: atomic{ PRODUCE(0, 2); printf("a")}
  od
}

proctype Actor_b() {
  do :: atomic { WAIT(0,3) -> CONSUME(0, 3); PRODUCE(1, 1); printf("b") }
  od
}

proctype Actor_c() {
  do :: atomic {WAIT(1, 2) -> CONSUME(1, 2); printf("c")}
  od
}

init {
  atomic {
    run Actor_a();
    run Actor_b();
    run Actor_c();
  }
}

starting claim 4
spin: couldn't find claim 4 (ignored)
Starting Actor_a with pid 2
  2:    proc  0 (:init::1) sample.pml:30 (state 1)      [(run Actor_a())]
Starting Actor_b with pid 3
  3:    proc  0 (:init::1) sample.pml:31 (state 2)      [(run Actor_b())]
Starting Actor_c with pid 4
  4:    proc  0 (:init::1) sample.pml:32 (state 3)      [(run Actor_c())]
  6:    proc  1 (Actor_a:1) sample.pml:14 (state 1)     [ch[0] = (ch[0]+2)]
  7:    proc  1 (Actor_a:1) sample.pml:14 (state 2)     [((ch[0]>sz[0]))]
  7:    proc  1 (Actor_a:1) sample.pml:14 (state 3)     [sz[0] = ch[0]]
              a  7:     proc  1 (Actor_a:1) sample.pml:14 (state 7)     [printf('a')]
  9:    proc  1 (Actor_a:1) sample.pml:14 (state 1)     [ch[0] = (ch[0]+2)]
 10:    proc  1 (Actor_a:1) sample.pml:14 (state 2)     [((ch[0]>sz[0]))]
 10:    proc  1 (Actor_a:1) sample.pml:14 (state 3)     [sz[0] = ch[0]]
              a 10:     proc  1 (Actor_a:1) sample.pml:14 (state 7)     [printf('a')]
 12:    proc  1 (Actor_a:1) sample.pml:14 (state 1)     [ch[0] = (ch[0]+2)]
 13:    proc  1 (Actor_a:1) sample.pml:14 (state 2)     [((ch[0]>sz[0]))]
 13:    proc  1 (Actor_a:1) sample.pml:14 (state 3)     [sz[0] = ch[0]]
              a 13:     proc  1 (Actor_a:1) sample.pml:14 (state 7)     [printf('a')]
 15:    proc  1 (Actor_a:1) sample.pml:14 (state 1)     [ch[0] = (ch[0]+2)]
 16:    proc  1 (Actor_a:1) sample.pml:14 (state 2)     [((ch[0]>sz[0]))]
 16:    proc  1 (Actor_a:1) sample.pml:14 (state 3)     [sz[0] = ch[0]]
              a 16:     proc  1 (Actor_a:1) sample.pml:14 (state 7)     [printf('a')]
spin: trail ends after 17 steps
#processes: 4
                ch[0] = 8
                ch[1] = 0
                sz[0] = 8
                sz[1] = 0
 17:    proc  3 (Actor_c:1) sample.pml:24 (state 5)
 17:    proc  2 (Actor_b:1) sample.pml:19 (state 11)
 17:    proc  1 (Actor_a:1) sample.pml:13 (state 9)
 17:    proc  0 (:init::1) sample.pml:34 (state 5) <valid end state>
4 processes created

Thanks a lot if you can help!

Answer 1

There are two problems in the original attempt. By fixing them I successfully get the expected answer.

• The LTL specified using the -f option from command line will be negated. Instead, I use the inline LTL by adding ltl { <> p} into the Promela program.

• Second, when executing pan, seems that we need to use -a to "find acceptance cycles". I'm not completely sure what this means, my guess is that Spin will try to identify infinite schedules.