Murphi入门（二）—— 可达集范例讲解（1）

发表于 更新于 分类于 阅读次数：

本文内容：

  • ​通过简单例子分析murphi代码执行状态
  • 可达集概念分析
  • 分析murphi如何求出可达集

概念

从初始状态开始，在不违反安全性质的情况下，根据规则集可到达的所有状态的集合。

以下，以pingpong.m为例，进行讲解。

（pingpong.m 文件可以在 cmurphi／ex/toy 中找到）

用Murphi求出可达集

打印出所有可能状态

(如果不知道怎么运行，请看 Murphi入门（一）)

./pingpong.o -p

输出：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
Unpacking state from queue:
Players[0].hasball:true
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:false

The following next states are obtained:

Firing rule Pass ball, p:0
Obtained state:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:true

Firing rule Keep ball, p:0
Obtained state:
Players[0].hasball:true
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:false

------------------------------
Unpacking state from queue:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:true
Players[1].gotball:false

The following next states are obtained:

Firing rule Pass ball, p:1
Obtained state:
Players[0].hasball:false
Players[0].gotball:true
Players[1].hasball:false
Players[1].gotball:false

Firing rule Keep ball, p:1
Obtained state:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:true
Players[1].gotball:false

------------------------------
Unpacking state from queue:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:true

The following next states are obtained:

Firing rule Get ball, p:1
Obtained state:
Players[0].hasball:false
Players[0].gotball:false
Players[1].hasball:true
Players[1].gotball:false

------------------------------
Unpacking state from queue:
Players[0].hasball:false
Players[0].gotball:true
Players[1].hasball:false
Players[1].gotball:false

The following next states are obtained:

Firing rule Get ball, p:0
Obtained state:
Players[0].hasball:true
Players[0].gotball:false
Players[1].hasball:false
Players[1].gotball:false


==========================================================================

Status:

	No error found.

State Space Explored:

	4 states, 6 rules fired in 0.10

讲解

  • 以上为所有4种状态：
    • 初始状态：玩家1执球，或玩家2执球。这就有两种状态了。
      • 将这两种状态放进queue中，也放入可达集中。
    • 从queue中拿出一个，即玩家1执球
      • 往下执行，玩家2接球
      • 该状态不在queue中，且不违反invariant，放入可达集
      • 放进queue中
    • 从queue再拿出一个，即玩家2执球
      • 往下执行，玩家1接球
      • 该状态不在queue中，且不违反invariant，放入可达集
      • 放进queue中
    • 从queue中拿出一个，即玩家2接球
      • 往下执行，玩家2执球
      • 该状态已经在可达集中，不放入queue中
    • 从queue中拿出一个，即玩家1接球
      • 往下执行，玩家1执球
      • 该状态已经在可达集中，不放入queue中
  • 最终，可达集中有4个状态，且每一步规则都不违反invariant，即场上每次只能有一个球。
  • 程序运行不会终止，所以是正确的。