ProtVisualizer - An Automatic Protocol Visualization Tool

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

由于形式化的协议往往晦涩难懂，对于科研研究造成了很大程度的阻碍。主要是本人在研究协议的时候，感觉晦涩难懂，看了一些论文和介绍，研读了代码，花了很长时间才弄懂。如果有一个可视化的方法能够帮助理解，就会大大缩短理解协议的时间，从而把更多时间花在真正的理论研究上。

因此，为提高可理解性，特做此协议可视化的脚本。

PS. 目前只支持固定样式的german 和flash 协议（结点=3）

环境及配置

  • 环境：Mac OX (不影响运行)
  • 配置：
    • Python3 （记得是python3，因为需要引入bs包）
    • beautiful soup 4 ——处理html
    • html （不用配置环境，sublime 或txt即可打开。有用到bootstrap的一些样式，所以可能需要安装bootstrap）——可视化图
    • webkit2png 需要安装 ——html转png
    • ffmpeg 需要安装 —— png转视频

项目思路

  • python读入文本（murphi打印出来的状态序列）
  • python读完一个状态，就批量改一次html中同id下的状态的值。更改了的值用不同的class做颜色标示
  • 依次读完所有状态，就依次得到N个状态图
  • ffmpeg将N个状态图做成视频，每张图停顿3秒（可调整）

具体实现

以下，将比较详细的讲解murphi控制error（反例）路径追踪打印、python处理文本、html制作及最后的视频生成处理。

状态生成

Prerequisite

murphi的具体安装详见murphi入门

murphi使用手册中文翻译详见 murphi手册

Invariant设置

因为想要用可视化来观察协议的运行路径，所以需要设置invariant

  • 选择想要到达的状态

由于每个node的cache的初始状态都是I（Invalid），也就是无效状态，如果想观察某个节点是怎样从初始状态到达S的，那么设置invariant如下：（以flash协议为例）

1
2
3
4
ruleset p:NODE do
  invariant "I2S"
    p!=0 -> (Sta.Proc[p].CacheState != CACHE_E)
  end;

反例路径生成

生成 .o 文件之后，选择输出参数。因为想要获得最短路径，所以用bfs（广度搜索）效果会比深度搜索更好。

如果不能理解，看下面这个例子：

这是互斥协议的状态简化图。

其中（I,I）是初始状态，每条边都是规则迁移，每个结点都表示一个状态。当每条路径走到一个已经在hash表（用于存储状态集合）的状态时，该路径就不再继续下去。

例子

现在，令invariant为：node[1].state != I | node[2].state !=T，也就是图中的（I,T）。则当两个节点的状态分别为I和T的时候，则会产生error trace。让我们分别看一下深度和广度搜索的工作原理：

  • 深度搜索：

    原理：从第一条路径开始，直到违反invariant，或走到走过了的状态为止；然后搜索下一条路径。

    路径：(I,I) —> (T,I)—>(C,I) —>(E,I) —> (I,I) 走过了，退出该路径

       (I,I) —> (T,I)—>(C,I) —>(E,I) —> (E,T) —> (I,T) 违反invariant，退出

    打印error trace = (I,I) —> (T,I)—>(C,I) —>(E,I) —> (E,T) —> (I,T) ，路径长度 = 6

    遍历的状态数 = 5 + 2 = 7 (去掉重复的)

    但是可以发现，这不是最短的路径

  • 广度搜索：

    原理：从初始状态开始，将该初始状态能到达的所以状态先走一步，如果没有违反invariant，则每一条路再往下走一次。

    路径：(I,I) —>(T,I) —>(I,T) ，违反invariant，退出

    打印error trace = (I,I) —>(I,T)， 路径长度 = 2

    遍历的状态数 = 3

    是最短的路径.

需要注意的是，广度遍历一般会遍历比深度遍历更多的状态数，但是找到的路径会是最短的。该案例只是一个特殊的案例，能在第一步就找到反例。

输出参数

  • 这里选择-tf打印具有完整状态的error trace，路径中的每一个状态都是完整的全局变量的赋值，这是为了之后python处理的时候所需。完整的语句为：(输出路径可选)
1
./protocol_name.o -tf >output.txt
  • 平时观察的时候，建议使用-ta或者-td。两者都会将error trace打印出来，并且除了初始化和最后违反的状态，其他的中间状态都只显示改变了的量，利于观察。另外，前者还会将遍历到的所有状态也打印出来。
  • 其他可选择的输出参数有很多，可以通过-help得到。

文本处理

逐行处理txt

  • 先处理掉之前的murphi版本之类的信息
  • 判断开头：
    • 空白开头、“The”、“Obtained”：continue
    • “Rule”或“Startstate”开头： 记录规则名
    • “-”开头：（说明一个状态已记录完整）传入draw函数，绘制
    • “End”开头：break
    • 其他：写入states字典

要点

  • 处理的时候注意一下开头的情况
  • line写入字典的方法

代码

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
def read_states():
    states = []
    start = True
    with open(filename) as f:
        for line in f:
            if start and not line.startswith('Startstate'):
                continue
            else:
                start = False

            # 去掉头尾空白
            line = line.strip()
            # 如果结尾
            if line.startswith('End'): break

            # 其他字段
            if not len(line) or line.startswith('The') or line.startswith('Obtained'):
                continue
                
            # 一个状态读入完毕，可以绘画
            if line.startswith('-'):
                draw(states,s)
                states = []
                print(states)
            # 一个状态的开始
            elif line.startswith('Startstate') or line.startswith('Rule'):
                s = line
                print(s)
            else:
                # 状态写入中
                states.append([n for n in line.split(':')])

html制作

绘制草图

可以先用ppt或者ps绘制出协议的基本可视化图。

German协议和Flash协议的草图如下：

German

Flash

html代码实现

css

  • 直接在头文件里写style —— 懒人者模式

  • 或者在另一个file里写css，再引入

  • 在实现html的时候，允许和草图有所出入

    注意：

    因为之后要用到webkit2png，而在不同系统下默认的是不同的浏览器引擎。所以在设置大小的时候，尽量不要用%，用px最直接，也最真实。

    可以在ps中测量大小，也可以直接用开发者模式进行实时调整。

模块编写

没有难度，可以随时用开发者模式在浏览器中看。因为苹果自带的safari效果调试不是很方便，我直接在chrome中调试。

写id

因为需要修改每个能改的值，所以要在能改的值那里加上id。因为之后为了映射方便，所以id值直接就等于muprhi程序中设置的每个全局变量的名字。

额外增加css

原因是让修改了的值更加醒目。

这里直接设置了两种背景色，一种是透明，就可以显示本来的颜色；一种是加深了的背景色，固定了一个背景色的值

最终效果

视频生成

修改原html

  • 一次状态完全读完之后，将状态字典和规则名传入draw函数
  • 遍历所有的全局变量，找到对应的id，取出里面的string
    • 如果与现在要赋的值不一样，则修改string，修改class = ‘dark’
    • 如果与现在要赋的值一样，则另class = ‘light’
  • 修改规则名
  • 保存成html
  • 写进html文件

html转png

  • webkit2png安装
  • 设置画幅大小 （1366 * 768）

png转视频

  • ffmpeg安装
  • 设置每张png放映多久： -r 1/3 就是三秒一张

命名的技巧

因为新建文件夹的时候，如果有相同的名字，则会报错而结束程序。所以将文件的命名与时间联系起来，生成独一无二的文件名，就不会出现重名或者覆盖的问题。

完整代码

draw函数

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
def draw(states,s):
    global count

    # edit each state id
    # if changed, then class = dark
    # else, change class = light
    for i in range(len(states)):
        q = soup.find(id=states[i][0])
        if not q: continue;
        # print(q)
        if q.string != states[i][1]:
            q['class'] = 'dark'
            q.string = states[i][1]
        else:
            q['class'] = 'light'

    # change rule name
    p = soup.find(id='rule')
    p.string = s.split(',')[0];

    # generate each html
    html = soup.prettify()

    # write each html into profile
    with open("./"+ timestr +fn+'_output/'+fn+'_htmls/output'+str(count)+".html", "w") as file:
        file.write(html)

    rooturl='./' + timestr + fn+'_output/'

    # transform html to png
    os.system('webkit2png -W 1366 -H 768 -F '+rooturl+fn+'_htmls/output'+str(count)+'.html -D '
        + rooturl+'/'+fn+'_pngs -o ' + fn + str(count))

    count += 1

main函数

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
if __name__ == '__main__':
    # location of cmurphi/ex/test
    default_url = '/Users/Bella/Documents/Lab/visualization'
    fn = filename.split('.')[1].split('/')[1]

    # datetime as parameter
    timestr = time.strftime("%Y%m%d%H%M%S")
    rooturl = timestr + fn + '_output/'

    # change location
    os.chdir(default_url)

    # create new folder for outputs
    os.mkdir(rooturl)
    os.mkdir(rooturl + fn + '_htmls')
    os.mkdir(rooturl + fn + '_pngs')

    # initialization
    list = []
    count = 1
    soup = BeautifulSoup(open('./flash.html'), "lxml")


    read_states()
    os.chdir(timestr + fn+'_output/'+fn+'_pngs')
    if not os.system('ffmpeg -f image2 -r 1/3 -start_number 1 -i ./' + fn + '%d-full.png -vcodec mpeg4 -y ../'
        + fn + '.mp4'):
        print('video generated!')

在最前面添加上import和文件路径：

1
2
3
4
5
6
7
8
filename = "./flash_I2E.txt"
# location of cmurphi/ex/test
default_url = '/Users/Bella/Documents/Lab/visualization'


from bs4 import BeautifulSoup
import os
import time

注意

  • 要将html文件与txt文件放在同一个文件夹 a 中，然后default_url 是写到 a 的路径

  • filename 是 txt的文件名

未来改进方向

  • js实现动态化
  • 响应机制，有按钮可以点击，可以选择
  • 将状态生成和可视化相结合，可以可视化地跑出状态
  • 对文本的识别可以再智能化一点