通过LTL公式在所有可能的执行中找到变量的最小值

请考虑操纵共享变量N的两个过程的Promela模型：

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可以拥有的最小值？

在一般中，这是不可能的。 ltl公式表达必须在执行路径上保留的属性，而根据最小的定义，您想通过多个执行路径表达属性。实际上，仅当没有其他执行跟踪具有较小的值的情况下，才考虑 n 最小。

Work-Around。，您可以通过在LTL公式上多次运行Spin来查找N的最小值，并且对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递增8次N的值
proc0将N的值重置为1
proc1在temp中复制N = 1，然后停止执行任何指令
proc0将N递增至9，然后终止
proc1将N的值重置为2，然后终止

相关内容

最新更新

热门标签：