Обновлять

В моей предыдущей попытке есть две проблемы. Исправив их, я успешно получаю ожидаемый ответ.

• LTL, указанный с помощью параметра -f из командной строки, будет инвертирован. Вместо этого я использую встроенный LTL, добавляя ltl { <> p} в программу Promela.

• Во-вторых, при выполнении pan кажется, что нам нужно использовать -a для поиска приемочных циклов. Я не совсем уверен, что это значит, я предполагаю, что Spin попытается идентифицировать бесконечные расписания.

Оригинальный вопрос

Я новичок в проверке моделей и Spin. У меня возникли проблемы со следующим примером.

• Уточняю утверждение '<> p', что каждое расписание в итоге приведет к p, в моем случае SUM > BOUND

• Насколько я понимаю, если существует существует бесконечное расписание, в котором p всегда ложно, в моем случае SUM всегда меньше или равно BOUND, спин сообщит об этом как о контрпримере.

• Однако, когда я запускаю spin, я получаю встречный пример, в котором p верно.

В частности, команды, код Promela и трейл следующие.

В этом следе результатом является то, что p удовлетворяется, так как SUM действительно больше, чем BOUND. Я не мог понять, почему Spin приводит мне контрпример, удовлетворяющий 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

Большое спасибо, если вы можете помочь!