Murphi入门（四）—— 用murphi实现GCD（1）

发表于 更新于 分类于 阅读次数：
  • 该博文将通过murphi语言，求解GCD（最大公因数）

GCD Murphi Programming

目标

  • 用murphi编程，实现GCD（最大公约数）求解

思想

  • 迁移规则1: 保证被除数>=除数，如果不满足，则互换
  • 迁移规则2: 循环：被除数除以除数，如果余数不为零，则被除数 = 除数，除数 = 余数。
  • 不变量：余数>0. 当余数=0时，程序结束。
  • 打印反例：用put

代码

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
type
	val_t:0..1000;
var
	x : val_t;
	y : val_t;
	r : val_t;
	temp: val_t;

Procedure gcd(Var x,y,r: val_t);
begin
	while r!= 0 do
		x := y;
		y := r;
		r := x % y;
	end;
	put(y);
end;

rule r > 0 ==> begin gcd(x,y,r); end;
rule x<y ==> begin temp :=y; y := x; x := temp; end;
	
startstate  -- 测试用例，x是被除数，y是除数，r是余数。特地设置成x<y。
	x := 12;  
	y := 16;
	r := x%y;
end;


-- 不变量／安全性质
invariant r > 0;

将该murphi文件存储于cmurphi/ex/test下，名为gcd.m，控制台切换路径到该目录下，执行：

1
../../src/mu gcd.m

生成对应cpp文件，再用gcc编译：

1
g++ -ggdb -o gcd.o gcd.cpp -I../../include -lm

生成o文件，直接运行：

1
./gcd.o

输出：

1
2
3
4
5
6
7
8
9
10
11
12
y:4

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

Result:

	Invariant "Invariant 0" failed.

State Space Explored:

	3 states, 2 rules fired in 0.10s.

如果加上选项 -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
Verbose option selected.  The following is the detailed progress.

Firing startstate Startstate 0
Obtained state:
x:12
y:16
r:12
temp:Undefined

------------------------------
Unpacking state from queue:
x:12
y:16
r:12
temp:Undefined

The following next states are obtained:

Firing rule Rule 1
Obtained state:
x:16
y:12
r:12
temp:16

y:4
Firing rule Rule 0
Obtained state:
x:12
y:4
r:0
temp:Undefined
==========================================================================

Result:

	Invariant "Invariant 0" failed.

State Space Explored:

	3 states, 2 rules fired in 0.10s.

可以看到，先进入rule2，将x，y进行交换，再执行rule1，直到不满足为止。输出y = 4.