使用NuSMV做形式化验证

NuSMV的安装

在 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。

使用NuSMV解决过河问题

过河问题的描述

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

画出过河问题的有限状态机

其中MGCW-Empty表示初始状态。“—”左边的符号表示对应的符号在左岸。“—”右边的服务表述对应的符号在右岸。

M表示人，G表示羊goat,C表示白菜Cabbage,W表示狼wolf.
箭头表示表示每次在船上运输什么东西。

使用NuSMV表示出过河问题的状态机

MODULE main
VARferrymen: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;      --船上为空--初始化的时候,全部在河岸的左边FALSE
ASSIGNnext(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};   --表示状态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};    --状态6的转移关系ferrymen=FALSE & cabbage=TRUE & wolf=TRUE&goat=FALSE : {goat_man,man};    --状态7的转移关系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;

代码的逻辑就是为了反映状态机。
代码设计思路：
ferrymen,goat,wolf,cabbage都是boolean类型的变量，分别表示人、羊、狼、白菜是否在河的右边。当他们的值为FALSE的时候，说明他们在左边，否则在右边。
ship表示每次船上运输的东西，它的取值为goat_man（同时运人和羊）、wolf_man(同时运人和狼)、cabbage_man(同时运人和白菜)、man(只运人)、empty(什么都不运)。
初始化时设置所有的变量的初始值，对应于状态机的初始状态。

写出转移过程：

写出安全过河的条件：

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

这个条件表示，在羊、白菜、狼、人全部到河右边之前，始终存在当羊和狼在一起时必有人和他们在一起，且当羊和白菜在一起时必然有羊和人在一起。

模型检验

运行上面的代码，得到结果如下：

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

输出一条可行的运输路径

因为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. 最后，人带着羊一起过河。

使用NuSMV解决过河问题相关推荐

python解决过河问题
只有一艘船,三个商人三个仆人过河,每一次船仅且能坐1~2个人,而且任何一边河岸上仆人比商人多的时候,仆人会杀人越货. 这是一个很经典的过河问题.题解: #允许状态集合,例num=3 #S={(x,y) ...
SPIN和SMV工具的对比学习 ——基于农夫过河问题
前言 SPIN和SMV是课程中介绍了两种特别重要的模型检测工具,本文将介绍两种工具的安装.基本使用,同时使用两种工具来解决农夫过河问题,并对这两种工具进行比较. 一.形式化验证工具的安装 1.1.SP ...
python代码怎么变成软件_Python变成技术
Python 变成技术数科 181 李思涵我在阅读了教材后,大致了解了 python 是最流行的动态脚本语言之一.<编程导论 - 以 Python 为舟>本书共 8 章,由浅入深.全面 ...
高中计算机选修代码,高中信息技术新课标(完整版)
<高中信息技术新课标(完整版)>由会员分享,可在线阅读,更多相关<高中信息技术新课标(完整版)(24页珍藏版)>请在人人文库网上搜索. 1.高中信息技术课程标准一.课程的基本理 ...
javaEE面试重点
Hibernate工作原理及为什么要用? 原理: 1. 读取并解析配置文件 2. 读取并解析映射信息,创建SessionFactory 3. 打开Sesssion 4. 创建事务Transation ...
用BFS（广度优先搜索queuelist）算法解决农夫过河问题
用BFS(广度优先搜索queue&&list)算法解决农夫过河问题一.问题需求分析一个农夫带着一只狼.一只羊和一棵白菜,身处河的南岸.他要把这些东西全部运到北岸.问题是他面前只有一 ...
基于visual Studio2013解决C语言竞赛题之1089牛虎过河
题目解决代码及点评 /************************************************************************/ /* ...
用C语言解决狼羊白菜过河的思路,基于visual Studio2013解决C语言竞赛题之1079狼羊过河...
题目解决代码及点评 /************************************************************************/ /* ...
java狼羊草过河_解决狼、羊、白菜过河问题的编程思路
前几天女朋友复习人工智能的考试,看见了一道经典的狼.羊.白菜过河问题,题目如下:一个人带着一只羊,一条狼和一个白菜想过河,假设他每次只能带一只羊,或者一条狼,或者一棵白菜过河,并限定人不在场时,狼和羊 ...
一位老农带着猫、狗、鱼过河，河边有一条船，每次老农只能带一只动物过河。当老农不和猫狗鱼在一起时，狗会咬猫，猫会吃鱼，当老农和猫狗鱼在一起时，则不会发生这种问题。编程解决猫狗鱼过河问题。
import java.util.ArrayList; import java.util.List; import java.util.Random;/*** 一位老农带着猫.狗.鱼过河,河边有一条船 ...

使用NuSMV解决过河问题

NuSMV的安装

使用NuSMV解决过河问题

过河问题的描述

画出过河问题的有限状态机

使用NuSMV表示出过河问题的状态机

写出转移过程：

模型检验

输出一条可行的运输路径

使用NuSMV解决过河问题相关推荐

最新文章

热门文章