Murphi入门（一）——安装配置

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

该博文将讲述以下两个方面：

  • Murphi安装、配置、运行
  • 讲解一个Murphi范例：pingpong

Preliminary

带参协议验证

  • 带参系统用P(N)表示

    • P = protocol
    • N = 参数的个数。
      • 参数 = 具有相同结构的并发执行的主体（+有限个结构不同的主体）

  • 当N被具体赋值时，就是这个带参系统的一个实例

  • 每个主体都能通过规则进行交互（条件+行为）

  • 规则集R：刻画带参系统的运行过程

  • 应用：缓存一致、安全系统、网络通信等

    ​

理解

  • 相当于每个主体是一个进程，进程之间通过规则进行状态迁移，所有可能发生的事情，都是进程们从初始状态通过规则集R中的规则，所到达的状态。带参系统通过调整参数，来增加进程，通过验证器来保证某个待验证系统的所有可达的状态都是正确的（validation + verification）。

安装及配置

本机环境

Mac OX 10.12.3 （环境不影响安装步骤）

安装步骤

注意：

如果将cmurphi整个文件夹复制到新的系统中，可能会编译不成功。这是由于src下make这一步在不同环境中（平台）有不同操作。所以这时候就需要到src中重新make一下。

如果重新make不行，则重新下载新的cmurphi，重新make即可。

验证步骤

  • 编写Murphi语言程序，命名如pingpong.m

  • 运行Murphi编译器，将pingpong.m编译成pingpong.c（c++）

  • 运行C++编译器，将pingpong.c进行编译

  • 运行pingpong.out来运行模拟／验证过程

  • 接下来两种方法
    • 直接make（example中的例子）
      • 到ex／toy中make，就将所有的m结尾的文件都make成o结尾的
      • 直接运行./pingpong
    • 没有make文件的，需要按照上面的引用部分，进行m - c - o的生成
      • 在cmurphi5.4.9.1/bella目录下
        • ../src/mu pingpong.m =>生成cpp
        • g++ -ggdb -o pingpong.o pingpong.cpp -I ../../include -lm
          • ../include 是inclue的路径，比如ex下目录是../include 然后其它的比如ex/toy下就要../../include了

           

        • ./pingpong.o
  • pingpong运行结果如下：
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
TsoArabelas-MacBook-Pro:toy Bella$ ./pingpong
This program should be regarded as a DEBUGGING aid, not as a 
certifier of correctness.
Call with the -l flag or read the license file for terms
and conditions of use.
Run this program with "-h" for the list of options.

Bugs, questions, and comments should be directed to
"melatti@di.uniroma1.it".

CMurphi compiler last modified date: Jan 26 2017
Include files last modified date:    Nov 8 2016
==========================================================================

==========================================================================
Caching Murphi Release 5.4.9.1
Finite-state Concurrent System Verifier.

Caching Murphi Release 5.4.9.1 is based on various versions of Murphi.
Caching Murphi Release 5.4.9.1 :
Copyright (C) 2009-2012 by Sapienza University of Rome.
Murphi release 3.1 :
Copyright (C) 1992 - 1999 by the Board of Trustees of
Leland Stanford Junior University.

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

Protocol: pingpong

Algorithm:
	Verification by breadth first search.
	with symmetry algorithm 3 -- Heuristic Small Memory Normalization
	with permutation trial limit 10.

Memory usage:

	* The size of each state is 8 bits (rounded up to 8 bytes).
	* The memory allocated for the hash table and state queue is
	  8 Mbytes.
	  With two words of overhead per state, the maximum size of
	  the state space is 476219 states.
	   * Use option "-k" or "-m" to increase this, if necessary.
	* Capacity in queue for breadth-first search: 47621 states.
	   * Change the constant gPercentActiveStates in mu_prolog.inc
	     to increase this, if necessary.

Warning: No trace will not be printed in the case of protocol errors!
         Check the options if you want to have error traces.

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

Status:

	No error found.

State Space Explored:

	4 states, 6 rules fired in 0.10s.

语法规则

Murphi的保留字：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
alias           array           assert          begin           
boolean         by              case            clear
const           do              else            elsif
end             endalias        endexists       endfor
endforall       endfunction     endif           endprocedure
endrecord       endrule         endruleset      endstartstate
endswitch       endwhile        enum            error
exists          false           for             forall
function        if              in              interleaved
invariant       of              procedure       process
program         put             record          return
rule            ruleset         startstate      switch
then            to              traceuntil      true
type            var             while

以pingpong.m为例

定义部分

1
2
3
4
Type player_t : 0..1;
Var Players : Array[ player_t ] of Record
hasball, gotball: boolean
		     End;
  • 每个玩家分别有两个属性
    • hasball
    • gotball
  • 总共两个玩家：0/1

规则集部分

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
Ruleset p : player_t Do
  Alias ping: Players[p];
        pong: Players[ 1 - p ] Do

    Rule "Get ball"
      ping.gotball
    ==>
    Begin
      ping.hasball := true;
      ping.gotball := false;
    End;

    Rule "Keep ball"
      ping.hasball
    ==>
    Begin
    End;

    Rule "Pass ball"
      ping.hasball
    ==>
    begin
      ping.hasball := false;
      pong.gotball := true;
    End;

    Startstate /* Yes, a startstate within an alias and a ruleset. */
    Begin
      ping.hasball := true;
      ping.gotball := false;
      clear pong;
    End;

  End;

End;

  • Alias语句：

    • <aliasstmt> ::= alias <alias> { ; <alias> } do [ <stmts> ] end

    <alias> ::= <ID> : <expr>

      1
      2
      3
      4
      5
      6
      7
      8
      9
      10
      11
      12
      13
      14
      15
      16
      17
      18
      19
      20
      21
      22
      23


      - Alias中定义的<ID>会覆盖外层同样的<ID>。

      - 也就是定义两个玩家：ping，pong

      - 规则集中分别有：

        - 执球
        - 接球
        - 抛球

      ### 不变量

      ```c
      Invariant "Only one ball in play."
        Forall p : player_t Do
          !(Players[p].hasball & Players[p].gotball) &
          (Players[p].hasball | Players[p].gotball) ->
          Forall q : player_t Do
            (Players[q].hasball | Players[q].gotball) -> p = q
          End
        End;

  • “只能有一个球在场上”是不能改变的，最基础的要求