Murphi入门（五）—— 用murphi实现GCD（2）

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

该博文是对之前GCD编程的改进：

  • 未改进的GCD地址
  • 改进思路
  • 通过GCD，对Murphi编程的思想做个总结

Mar 7 GCD 改进

目标

  • 改进GCD
  • 通过GCD求解，更深刻理解Murphi与其他编程原理的不同

思想

Murphi最主要的思想是，按照所有全局变量的赋值来考虑，亦即考虑状态。因为是通过遍历所有状态来达到检验的目的。思考路线如下：

x y arr_i arr_temp
inital 12 21 [1,3] [1,3]
swap 21 12 [1,3] [1,3]
gcd 21 12 [1,3] [1,3]

这是根据rule的迁移而写的状态。可以看到，全局变量有x, y, arr_i, arr_temp。其中，x，y为需要求gcd的两个数。两个数组是用来保证invariant性质的。

规则

有两种思路：

函数思路：

​ 用常规编程的思想来思考这个程序，比如python语言中，用递归：

1
2
def gcd(x,y):
    return y if y == 0 else gcd(y, x%y)

​ 或者不用递归，用交换和循环：

1
2
3
4
5
6
7
8
9
10
11
12
def gcd(x,y):
	if x < y :
        temp = y
        y = x
        x = temp
    r = x % y
    while r != 0:
        x = y
        y = r
        r = x % y
    return y

可以看到，有两个步骤：

  • 交换
  • 循环直到找到最大公因数

所以将这个思路用于murphi规则：

  • rule “swap”
    • 条件：x < y
    • 动作：交换x，y的值
  • rule “gcd”
    • 条件：x > y
    • 动作：循环，求出gcd

代码实现：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
rule "swap" -- 交换
	x < y ==> 
    var temp: var_t;
    begin
      	temp := y;
		y := x;
		x := temp;
	end;

rule "gcd"  -- 求解
 	x >= y ==> 
	begin
  		gcd(x,y);
	end;
状态思路

因为全局变量有x和y，x与y的关系有3种可能：

  • x > y
  • x = y
  • x < y

其中，第二种直接可以输出x。第一种可以执行gcd(x,y)，第二种执行gcd(y,x)。将这个思路直接写成规则即可。

  • rule “gcd_x”
    • 条件：x > y
    • 动作：gcd(x,y)
  • rule “equal”
    • 条件：x = y
    • 动作：put(x)
  • rule “gcd_y”
    • 条件：x < y
    • 动作：gcd(y,x)

代码如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
rule "gcd_x"
	x > y ==>
	begin
		gcd(x,y);
	end;

rule "gcd_y"
	x < y ==>
	begin
  		gcd(y,x);
	end;

rule "equal"
  	x = y ==>
  	begin
  		put(y);
	end;

初始状态

x y arr_i arr_temp
initial 21 12 [1,3] [1,3]

代码实现：

1
2
3
4
5
6
startstate
	x := 21;
	y := 12;
	commonDivdors(x,y,arr_temp); 
	commonDivdors(21, 12, arr_i);
end;

不变量

在过程中，x，y的值都设置为不变，则此时不变的为x，y的公因数集合。每次状态的迁移都必须满足该表达式。即保证x，y不会改变。

代码：

1
2
invariant "commonDivdors"
	compare(arr_i, arr_temp);

函数 ／ 程序

函数与程序的区别为，函数有返回值，程序没有返回值。

在传递参数时，传入的参数都为引用传递，var开头表示在函数体内部可改变其值，没有var开头则为不可改变值。

如果要传入数值，则只能用不带var开头的形参。

要实现的函数／程序有：

  • gcd — 求解最大公因数
  • commonDivdors —求解x，y的公因数集合
  • compare —用来比较两个数组是否相同

具体实现如下：

gcd
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
Procedure gcd(x,y: val_t);
var
	r : val_t; 
	a : val_t; -- x，y的值不能改变，所以用局部变量来接受值
	b : val_t;
begin
	a := x;
	b := y;
	r := a % b;
	while r!= 0 do
		a := b;
		b := r;
		r := a % b;
	end;
	put(b); -- 输出最大公因数
end;
commonDivdors
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
Procedure commonDivdors(x, y: val_t; Var arr_temp:arr_t);
Var 
	temp : val_t;
	i : val_t;
	a: val_t;
	b: val_t;
begin
	a := x;
	b := y;
	i := 0;
	temp := b;
	
	if a < b then  -- 交换，使得被除数一直大于等于除数
		b := a;
		a := temp;
	end;

	while temp >= 1 do  -- 将除数一直减1，除被除数和除数，如果可以整除，则放入数组
		if (a % temp = 0) & (b % temp = 0) then
			arr_temp[i] := temp;
			i := i + 1;
		end;
		temp := temp -1;
	end;

	while i < 30 do   -- 把没有赋值的数组中其他的元素置0
		arr_temp[i] := 0; 
		i := i + 1;
	arr_temp[i] := 0; -- 最后一位循环不到，直接赋值
	end;
end;
compare
1
2
3
4
5
6
7
8
9
10
11
Function compare(arr_temp, arr_i: arr_t): Boolean; -- 有返回值
begin
	for i: val_t Do
      -- 逐位比较，如果碰到不同，则返回false。
      -- 因为commonDivdors函数按照从大到小依次减1的顺序计算，所以只要不同，则集合不同
		if arr_temp[i] != arr_i[i] then  -- 没有var开头，不可改变其值
			return false;  
		end;
	end;
	return true;
end;

运行

*死锁：某状态只有该状态本身之外，没有其他后继状态。

因为程序设置x，y的值不变（或互换之后，公因数集仍然没有改变），所以对于规则而言，一开始满足的，后来也会满足。所有造成死锁。但没关系，因为状态枚举完成，且会输出最大公因数。（用例： x = 24, y = 18, 规则用第二种方案）

1
./gcd_2.o -pr

结果如下：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
b:6

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

Result:

	Deadlocked state found.

State Space Explored:

	1 states, 1 rules fired in 0.10s.

Rules Information:

	Fired 0 times	- Rule "equal"
	Fired 0 times	- Rule "gcd_y"
	Fired 1 times	- Rule "gcd_x"

总结

  • murphi编程与一般编程的思维方式不太一样，要考虑全局状态的迁移。
  • 可以写出状态的表格，更有利于分析和理解。
  • 当分析了所有状态之后，规则集也就方便写出了。
  • 不变量的选择很重要。