Найти минимальное значение переменной во всех возможных исполнениях с формулой LTL

Question

Рассмотрим следующую Promela модель двух процессов, которые управляют общей переменной N:

byte N = 0; 

active [2] proctype P(){ 
    byte temp, i; 
    i = 1; 
    do 
     :: i < 10 -> 
      temp = N; 
      temp++; 
      N = temp; 
      i++; 
     :: else -> 
      break; 
    od 
} 

Как я могу использовать LTL formula, чтобы узнать минимальный значение, которое может иметь переменная N, когда оба процесса завершены?

Answer 1

Обычно, это невозможно. Формула LTL выражает свойство, которое должно удерживать путь выполнения, тогда как по определению минимум вы хотите выразить свойство по нескольким путям выполнения. На самом деле N считается минимальной только если нет другого выполнения трассировки, в котором он имеет меньшее значение.

---

Рабочие места. Вы можете, однако, найти минимальное значение из N, запустив Spin несколько раз по формуле LTL с увеличивающимся значением для N и проанализировав выход, чтобы определить правильный ответ.

Рассмотрим следующий пример:

byte N = 0; 

short cend = 0; 

active [2] proctype P(){ 
    byte temp, i; 
    i = 1; 
    do 
     :: i < 10 -> 
      temp = N; 
      temp++; 
      N = temp; 
      i++; 
     :: else -> 
      break; 
    od 

    cend++; 
} 

ltl p0 { [] ((cend == 2) -> 2 <= N) }; 
ltl p1 { [] ((cend == 2) -> 3 <= N) }; 

У нас есть два свойства:

• p0 заявляет, что глобально верно, что, когда оба процесса прекратить значение N, по крайней мере 2. Эта формула проверяется:

  ~$ spin -a -search -bfs -ltl p0 m.pml 
  ... 
  Full statespace search for: 
      never claim    + (p0) 
      assertion violations + (if within scope of claim) 
      cycle checks   - (disabled by -DSAFETY) 
      invalid end states  - (disabled by never claim) 
  
  State-vector 36 byte, depth reached 98, errors: 0 
  ... 
  

• p1 утверждает, что это глобально верно, что, когда оба процесса прекратить значение N, по крайней мере 3. Эта формула не проверено:

  ~$ spin -a -search -bfs -ltl p1 m.pml 
  ... 
  Full statespace search for: 
      never claim    + (p1) 
      assertion violations + (if within scope of claim) 
      cycle checks   - (disabled by -DSAFETY) 
      invalid end states  - (disabled by never claim) 
  
  State-vector 36 byte, depth reached 95, errors: 1 
  ... 
  

Итак, мы знаем, что минимальное значение N равно 2.

Давайте посмотрим контрпример:

~$ spin -l -g -p -t m.pml 
ltl p0: [] ((! ((cend==2))) || ((2<=N))) 
ltl p1: [] ((! ((cend==2))) || ((3<=N))) 
starting claim 2 
using statement merging 
    1: proc 1 (P:1) m.pml:7 (state 1) [i = 1] 
     P(1):i = 1 
    2: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
    3: proc 0 (P:1) m.pml:7 (state 1) [i = 1] 
     P(0):i = 1 
    4: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
    5: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 0 
    6: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 1 
    7: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 0 
    8: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 1 
    9: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 1 
10: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 2 
11: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
12: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 1 
13: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 2 
14: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 2 
15: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 3 
16: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
17: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 2 
18: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 3 
19: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 3 
20: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 4 
21: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
22: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 3 
23: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 4 
24: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 4 
25: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 5 
26: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
27: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 4 
28: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 5 
29: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 5 
30: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 6 
31: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
32: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 5 
33: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 6 
34: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 6 
35: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 7 
36: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
37: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 6 
38: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 7 
39: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 7 
40: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 8 
41: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
42: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 7 
43: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 8 
44: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 8 
45: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 9 
46: proc 1 (P:1) m.pml:9 (state 2) [((i<10))] 
47: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 1 
48: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 2 
49: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
50: proc 1 (P:1) m.pml:10 (state 3) [temp = N] 
     P(1):temp = 1 
51: proc 1 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(1):temp = 2 
52: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 1 
53: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 2 
54: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 2 
55: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 3 
56: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
57: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 2 
58: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 3 
59: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 3 
60: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 4 
61: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
62: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 3 
63: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 4 
64: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 4 
65: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 5 
66: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
67: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 4 
68: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 5 
69: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 5 
70: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 6 
71: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
72: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 5 
73: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 6 
74: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 6 
75: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 7 
76: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
77: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 6 
78: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 7 
79: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 7 
80: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 8 
81: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
82: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 7 
83: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 8 
84: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 8 
85: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 9 
86: proc 0 (P:1) m.pml:9 (state 2) [((i<10))] 
87: proc 0 (P:1) m.pml:10 (state 3) [temp = N] 
     P(0):temp = 8 
88: proc 0 (P:1) m.pml:11 (state 4) [temp = (temp+1)] 
     P(0):temp = 9 
89: proc 0 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 9 
90: proc 0 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(0):i = 10 
91: proc 0 (P:1) m.pml:14 (state 7) [else] 
92: proc 1 (P:1) m.pml:12 (state 5) [N = temp] 
     N = 2 
93: proc 1 (P:1) m.pml:13 (state 6) [i = (i+1)] 
     P(1):i = 10 
94: proc 1 (P:1) m.pml:14 (state 7) [else] 
95: proc 0 (P:1) m.pml:17 (state 12) [cend = (cend+1)] 
     cend = 1 
96: proc 1 (P:1) m.pml:17 (state 12) [cend = (cend+1)] 
     cend = 2 
spin: trail ends after 96 steps 
#processes: 2 
     N = 2 
     cend = 2 
96: proc 1 (P:1) m.pml:18 (state 13) <valid end state> 
96: proc 0 (P:1) m.pml:18 (state 13) <valid end state> 
96: proc - (p1:1) _spin_nvr.tmp:11 (state 6) 
2 processes created 

Как вы можете видеть, контрпример соответствует исполнению, в котором:

• proc0 сохраняет значение N = 0 в temp и затем прекращает выполнение любой команды
• proc1 увеличивает значение N для 8 раз
• proc0 сбрасывает значение N обратно к 1
• proc1 копий N = 1 в temp, а затем прекращает выполнение любой инструкции
• proc0 приращения
N до 9, а затем завершает
• proc1 сбрасывает значение N Назад к 2, а затем завершается