前言

SPIN和SMV是课程中介绍了两种特别重要的模型检测工具，本文将介绍两种工具的安装、基本使用，同时使用两种工具来解决农夫过河问题，并对这两种工具进行比较。

一、形式化验证工具的安装

1.1.SPIN的安装

1.1.1下载SPIN可执行文件

进入spin验证工具的官网：http://spinroot.com/spin/whatispin.html

进入安装向导页面，按照指示来进行安装。
Windows 10操作系统可以直接下载二进制文件。

可执行文件链接：http://spinroot.com/spin/Src/pc_spin649.zip
完整文件链接：http://spinroot.com/spin/Src/spin649.tar.gz
或者直接下载：https://pan.baidu.com/s/1mXOpl4kmXTqE46mKqbtz5w提取码：ji9h

下载完毕后解压,切换到spin.exe所在的目录下。

但是，直接跑是不得行的，它会报如下错误：

这是因为SPIN需要将promela语言先转义为C语言，然后再用C语言的编译器例如GCC生成最终的模型检验程序。

因此，还需给Windows 10安装gcc编译器。

1.1.2安装gcc编译器

下载cygwin安装文件。
文件链接：http://www.cygwin.com/setup-x86_64.exe
安装时注意选择安装gcc这个packages。

把路径C:\cygwin64\bin添加到系统的环境变量中。

使环境变量生效：

重新打开powershell,测试一下工具是否可以使用，如果出现如下界面就说明安装成功了。

1.1.3安装SPIN的GUI界面iSpin

自从6.4.9开始,spin的gui界面就改由基于tcltk来实现了。这是因为使用tcltk实现的GUI程序可以具有更好的跨平台移植性。
首先需要安装tclck.下载tcltk安装包,下载链接：https://bitbucket.org/tombert/tcltk/downloads/tcltk86-8.6.8-10.tcl86.Win7.x86_64.tgz
把文件解压后，将文件的bin路径添加到环境变量，并使环境变量生效。
然后切换到刚刚spin649所在的目标，输入：wish ispin.tcl，打开图形界面。

图形化界面视图：

运行一个Example测试一下。
输入：

1    init {
2       printf("passed first test!\n")
3   }

发现会报错：

这是因为刚刚没有把spin.exe所在的目录添加到环境变量中。现在把spin.exe所在目录添加至环境变量，并使环境变量生效，从新打开ispin图形化界面。

运行结果：

还是要报错，查询资料后发现需要做如下修改。
把刚刚安装的cygwin for 64bit,改成cygwin for 32 bit.这是因为spin只会生成32位的pan.c代码。
Cygwin for 32bit下载地址：https://cygwin.com/setup-x86.exe,安装过程同1.2所示。安装完毕后。
再运行Verification:

发现就是成功的了。

1.2.NuSMV的安装

1.2.1NuSMV下载

在http://nusmv.fbk.eu/bin/bin_download2-v2.cgi 页面下载合适的二进制可运行版本即可。在本报告中使用的是http://nusmv.fbk.eu/distrib/NuSMV-2.6.0-win64.tar.gz 文件。
解压后，即可得到具有如下目录的文件夹：

在bin目录下有可执行文件nusmv.exe，直接在命令行运行即可。

当然，为了方便起见，也可以将NuSMV.exe所在的目录添加到系统的环境变量中，这样就可以在系统的任意工作目录使用NuSMV。

1.2.2NuSMV可运行测试

可以测试一下看是否NuSMV.exe是否可用。

可以发现是可以运行的。

二、使用SPIN和SMV解决农夫过河问题

2.1问题描述

一个人带着狼、山羊和白菜在一条河的左岸，有一条船，大小正好能装下这个人和其它三者之一，人和他的随行物都要带过岸，但他每次只能带一样东西摆渡过河。如人将狼和羊留在同一岸，无人照顾，那么狼会把羊吃掉。同样，如羊和白菜在同一岸，无人照顾，那么羊会吃了白菜。

2.2农夫过河问题的有限状态机

其中MGCW-Empty表示初始状态。“—”左边的符号表示对应的符号在左岸。“—”右边的服务表述对应的符号在右岸。
M表示人，G表示羊goat,C表示白菜Cabbage,W表示狼wolf.
箭头表示表示每次在船上运输的物品的种类。

2.3使用NuSMV解决农夫过河问题

2.3.1编码实现

    MODULE mainVARferrymen:boolean;goat:boolean;wolf:boolean;cabbage:boolean;ship:{goat_man,wolf_man,cabbage_man,empty,man};--ship 表示船上装着是什么ASSIGNinit(ferrymen):=FALSE;    --人在左边init(goat):=FALSE;       --羊在左边init(wolf):=FALSE;       --狼在左边init(cabbage):=FALSE;    --白菜在左边init(ship):=empty;      --船上为空--初始化的时候,全部在河岸的左边FALSEASSIGNnext(ship):= caseferrymen=TRUE&ferrymen=goat & goat=wolf & goat=cabbage :empty;          --全部已经过河,不再运输ferrymen=FALSE & goat=FALSE & wolf=FALSE & cabbage=FALSE : {goat_man}; --表示状态1的转移关系ferrymen=TRUE&goat=TRUE & cabbage=FALSE & wolf=FALSE :{goat_man,man};   --表示状态2的转移关系ferrymen=FALSE & cabbage=FALSE&wolf=FALSE&goat=TRUE : {man,wolf_man,cabbage_man};   --表示状态3的转移关系ferrymen=TRUE & cabbage=FALSE & wolf=TRUE&goat=TRUE : {goat_man,wolf_man};  --表示状态4的转移关系ferrymen=FALSE & cabbage=FALSE & wolf=TRUE&goat=FALSE : {goat_man,cabbage_man}; --表示状态5的转移关系ferrymen=TRUE & cabbage=TRUE & wolf=TRUE&goat=FALSE : {man,cabbage_man,wolf_man};   --状态6的转移关系ferrymen=FALSE & cabbage=TRUE & wolf=TRUE&goat=FALSE : {goat_man,man};    --状态7的转移关系ferrymen=TRUE & cabbage=TRUE & wolf=FALSE&goat=TRUE : {cabbage_man,goat_man}; --状态9的转移关系ferrymen=FALSE & cabbage=TRUE & wolf=FALSE&goat=FALSE : {wolf_man,goat_man};  --状态10的转移关系TRUE: empty;esac;next(goat):=case(next(ship)=goat_man)& ferrymen=goat:    next(ferrymen);     --如果运输的是人和羊,那么人和羊都换到另外一边TRUE    : goat;esac;next(wolf):=case(next(ship)=wolf_man) & ferrymen=wolf:   next(ferrymen);     --如果运输的是人和狼,那么人和狼都换到另外一边TRUE    :wolf;esac;next(cabbage):=case(next(ship)=cabbage_man)& ferrymen=cabbage:    next(ferrymen); --如果运输的人和白菜,那么人和白菜都转移TRUE:  cabbage;esac;next(ferrymen):=  case(ship=empty): ferrymen;TRUE:!ferrymen  ;                                           --每次都需要人的陪同esac;--每次都要人陪同CTLSPEC!E [(   ((goat=wolf)-> (goat=ferrymen)) & ((goat=cabbage)->(goat=ferrymen)))U ((cabbage=TRUE)& (goat=TRUE) & (wolf=TRUE) &(ferrymen=TRUE))]### 2.3.2实现说明ferrymen,goat,wolf,cabbage都是boolean类型的变量，分别表示人、羊、狼、白菜是否在河的右边。当他们的值为FALSE的时候，说明他们在左边，否则在右边。ship表示每次船上运输的东西，它的取值为goat_man（同时运人和羊）、wolf_man(同时运人和狼)、cabbage_man(同时运人和白菜)、man(只运人)、empty(什么都不运)。初始化时设置所有的变量的初始值，对应于状态机的初始状态。写出转移过程：

2.3.3安全过河的条件

CTLSPECE [(  ((goat=wolf)-> (goat=ferrymen)) & ((goat=cabbage)->(goat=ferrymen)))U ((cabbage=TRUE)& (goat=TRUE) & (wolf=TRUE) &(ferrymen=TRUE))]

2.3.4模型检测结果

使用NuSMV运行上面的农夫过河实现，得到结果如下：

说明是的确是存在这么一条运输方法的。

2.3.5过河路径

因为NuSMV只会举出不符合所需要性质的反例，因此为了得到一条运输路径，可以写出上述的非，表示不存在这么一条路径···，然后NuSMV就会找出一个反例，而这个反例就是我们所需要的运输方法。
检验的性质为：
CTLSPEC
!E [( ((goat=wolf)-> (goat=ferrymen)) & ((goat=cabbage)->(goat=ferrymen)))
U ((cabbage=TRUE)& (goat=TRUE) & (wolf=TRUE) &(ferrymen=TRUE))]
模型验证结果：

这个结果显示的运输路径如下：
1. 船上先运输羊和人，这样goat=TRUE,ferrymen=TRUE
2. 人在单独过河，这样ferrymen=FALSE
3. 人和狼过河，这样ferrymen=TRUE,goat=TRUE,wolf=TRUE.
4. 人把羊带过河，这样ferrymen=FALSE,goat=FALSE
5. 人把白菜带过河，这样ferrymen=TRUE,cabbage=TRUE
6. 在再单独过河，这样ferrymen=FALSE
7. 最后，人带着羊一起过河。

2.4使用SPIN解决农夫过河问题

2.4.1编码实现

    mtype={original_side,destination_side}mtype ferryman=original_side,cabbage=original_side,goat=original_side,wolf=original_side;inline swap_side(loc){if:: loc==original_side -> loc =destination_side:: else -> loc =original_sidefi}inline carry(object){atomic{swap_side(ferryman);swap_side(object);}}inline carry_nothing(){atomic{swap_side(ferryman);}}proctype cross_river(){do:: carry_nothing():: ferryman==goat -> carry(goat):: ferryman==wolf -> carry(wolf):: ferryman==cabbage-> carry(cabbage)od}init{run cross_river();}#define GOAL ((ferryman==destination_side) && (wolf==destination_side) && (goat==destination_side) && (cabbage==destination_side))#define COND ((wolf==goat && ferryman != wolf)||(goat==cabbage && ferryman==goat))ltl nice {((!COND) U GOAL)}

2.4.2实现说明

首先通过mtype定义河的两岸：mtype={original_side,destination_side}
接着将农夫、白菜、羊、狼初始化在原岸边：
mtype ferryman=original_side,
cabbage=original_side,
goat=original_side,
wolf=original_side;
接下来实现swap_side部分，这是一个inline函数，它不是一个进程，但是可以传递参数。它表示把loc从一边运到另外一边。
接着实现携带物品过河的函数carry(object).注意里面是一个atomic语句。之所以用atomic是为了表达携带物品过河的动作要么人和物品一起过河，要么都不过河。
carry_nothing用于表示人空手过河。
cross_river进程才是关键。
proctype cross_river()
{
do
:: carry_nothing()
:: ferrymangoat -> carry(goat)
:: ferrymanwolf -> carry(wolf)
:: ferryman==cabbage-> carry(cabbage)
od
}
过河一共存在四种情况：要么人空手过河、要么人现在和羊在一边，那么接下来带着羊过河、要么带着狼过河、要么带着白菜过河。
SPIN里面的循环语句：do里面是从其中四条语句选一条满足条件的执行；如果有多条语句同时可执行，那么随机选一条。

2.4.3安全过河条件

#define GOAL ((ferryman==destination_side) && (wolf==destination_side) && (goat==destination_side) && (cabbage==destination_side))
#define COND ((wolf==goat && ferryman != wolf)||(goat==cabbage && ferryman==goat))
ltl nice {((!COND) U GOAL)}

SPIN里面的性质都是使用宏来定义的。GOAL表示最终的目标，人和羊和白菜和狼都过河。
COND表示需要满足的条件：如果狼和羊在一起，那么人就必须得和他们在一起；同时羊和白菜在一起，那么人必须也得羊在一起。
ltl nice xxx则是用ltl的语法写了这个约束。

2.4.4模型检测结果

我们使用iSPIN图形化界面来检测模型。SPIN会在性质前面自动添加一个Never来寻找一条不满足的路径,表示不存在那么一条路径使用到达目标前满足我们写的安全条件。可以看到，在Verification 部分，SPIN检测到了一条可行路径。

然后我们在iSPIN的Simulation/Replay页面可以看到整个的路径。

2.4.5过河路径

SPIN输出的过河路径比较长，主要是SPIN会有很多的农夫不携带任何物品而在河的两岸空转。我们把这些空转的路径给人工过滤掉即可得到一条简化的路径。
1. 船上先运输羊和人，这样goat=destination_side,ferrymen=destination_side
2. 人在单独过河，这样ferrymen=original_side
3. 人和菜带过河，这样ferrymen=destination_side,goat=destination_side,
cabbage=destination_side.
4. 人把羊带过河，这样ferrymen=original_side,goat=original_side;
5. 人把狼带过河，这样ferrymen=destination_side,wolf=destination_side
6. 人再单独过河，这样ferrymen=original_side
7. 最后，人带着羊一起过河。然后就全部安全过河了。

三、总结

3.1SPIN与SMV的比较

本人在做课后作业“农夫过河问题”使用的SMV工具来完成的。SPIN和SMV都是基于有限状态机来做形式化验证的。但是在使用过程中，个人感觉SPIN会比SMV具有更强的模型表达能力。因为SPIN是使用Promela语言来描述模型的，它可以很方便、自然的表达系统里面的各个并发进程。而SMV则是着重把状态机的状态转移表达出来，它在表达多个系统的同步转移的时候是需要进行一定的构造和转化的，它不想SPIN那样自然。

在输出结果上，SMV提供的错误反馈是一系列在执行路径上的各个状态的变量值的额序列，这一点非常类似于文本性的输出。这种过于简单的输出，使得寻找错误的过程变得非常困难和低效。而SPIN提供的错误反馈是整个协议执行的轨迹图，并且轨迹图直接编辑了发生错误（Assert失败）的具体行数。这使的分析变得更加便利和直观。例如2.4.4和2.3.4两个工具在输出过河路径的时候，SPIN就便于调试，它可以最终系统每个状态各个变量的值；而SMV则只是把最终的结果输出出来。

而且SPIN是具有图形化界面iSPIN的，因此其对用户的友好程度更佳，但从实际的使用体验来说SPIN的图形化界面奇丑无比，还不如输入命令行来的快。

SPIN相比SMV最大的优势在于：SPIN可以很方便的表达原子操作、不同实体之间交互的语义、同时SPIN也天生的对C语言支持很大。例如，在使用SMV不支持原子操作这种原语。于是在用SMV表达人携带着白菜过河时，写出的语句就不是特别直观，需要在case语句中使用两个next来表达这个原子语义。

 next(cabbage):=case(next(ship)=cabbage_man)& ferrymen=cabbage:   next(ferrymen); --如果运输的人和白菜,那么人和白菜都转移TRUE:  cabbage;esac;

然后SPIN是不支持CTL的，这是其不如SMV的地方。有些性质使用CTL可以很好的表达，例如存在一条路径，使得这条路径所有的节点都满足···。LTL在表达这种语义就不是特别方便了。

SPIN和SMV工具的对比学习 ——基于农夫过河问题相关推荐

NeurIPS 2022｜探明图对比学习的“游戏规则”：谱图理论视角
©作者 | 刘念, 王啸单位 | 北邮 GAMMA Lab 研究方向 | 图神经网络论文标题: Revisiting Graph Contrastive Learning from the Per ...
论文浅尝 - AAAI2021 | 基于对比学习的三元组生成式抽取方法
作者 | 叶宏彬,浙江大学博士研究生,研究方向:知识图谱.自然语言处理接收会议 | AAAI2021 论文链接 | https://arxiv.org/pdf/2009.06207.pdf 摘要在 ...
手把手！基于领域预训练和对比学习SimCSE的语义检索（附源码）
之前看到有同学问,希望看一些偏实践,特别是带源码的那种,安排!今天就手把手带大家完成一个基于领域预训练和对比学习SimCSE的语义检索小系统. 所谓语义检索(也称基于向量的检索),是指检索系统不再拘泥 ...
自然语言处理学习——基于对比自监督学习的语言模型设计和改进*
基于对比自监督学习的语言模型设计和改进* 摘要:最近几年见证了自然语言处理特别是表示学习的预训练模型的蓬勃发展,基于对比学习的自监督模型是其中最火的一种.BERT是近几年来在多种语言处理任务上取得了突 ...
AAAI 2022 | 北大阿里达摩院：基于对比学习的预训练语言模型剪枝压缩
近年来,预训练语言模型迅速发展,模型参数量也不断增加.为了提高模型效率,各种各样的模型压缩方法被提出,其中就包括模型剪枝. 然而,现有的模型剪枝方法大多只聚焦于保留任务相关知识,而忽略了任务无关的通用 ...
直播预告 | AAAI 2022论文解读：基于对比学习的预训练语言模型剪枝压缩
「AI Drive」是由 PaperWeekly 和 biendata 共同发起的学术直播间,旨在帮助更多的青年学者宣传其最新科研成果.我们一直认为,单向地输出知识并不是一个最好的方式,而有效地反馈和 ...
NAACL 2021 | AWS AI 提出基于对比学习的端到端无监督聚类方法
©PaperWeekly 原创 · 作者 | 李婧蕾学校 | 北京邮电大学硕士生研究方向 | 自然语言处理 Abstract 无监督聚类的目的是根据在表示空间中的距离发现数据的语义类别.然而,在学 ...
ACL 2021 | ConSERT：基于对比学习的句子语义表示迁移框架
©PaperWeekly 原创 · 作者 | 张琨学校 | 中国科学技术大学博士生研究方向 | 自然语言处理 Motivation 从 BERT,GPT 被提出来之后,自然语言处理领域相关研究进入 ...
直播 | KDD 2021论文解读：基于协同对比学习的自监督异质图神经网络
「AI Drive」是由 PaperWeekly 和 biendata 共同发起的学术直播间,旨在帮助更多的青年学者宣传其最新科研成果.我们一直认为,单向地输出知识并不是一个最好的方式,而有效地反馈和 ...

SPIN和SMV工具的对比学习 ——基于农夫过河问题

前言