SPIN утверждать не сработало

Question

Я пытаюсь понять, почему утверждение в этой модели не вызвано.

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) 
}

Очевидно, существует порядок операций, который выдает окончательное значение x = 1324:

• Первоначально x = 0
• A наборы x = 10*0 + 1 = 1
• B наборы x = 10*1 + 3 = 13
• A и B позволяют друг другупродолжить
• A наборы x = 10*13 + 2 = 132
• B наборы x = 10*132 + 4 = 1324

Answer 1

Утверждение не срабатывает, поскольку оно "никогда не достигнуто" , когда решатель подтверждает, что свойство

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

истинно.

Посмотритена выходе, который задан решателем, он четко заявляет, что:

• он проверяет любое утверждение, но только если в рамках формулы:

  Full statespace search for:
      never claim             + (ltl_0)
      assertion violations    + (if within scope of claim)
  

• утверждение не достигнуто:

  unreached in init
      t.pml:27, state 5, "assert((x!=1324))"
      t.pml:28, state 6, "-end-"
      (2 of 6 states)
  

---

Вы можете использовать опцию -noclaim, чтобы проверить модель только для утверждения, что тогда легко доказывается ложным:

~$ 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