摆渡者难题课件

摆渡者难题

你可记得摆渡者难题：一个船夫、山羊、卷心菜和狼都在河的一边。船夫至多可搭载一位乘客过河。如果船夫离开，山羊会吃掉卷心菜，狼也会吃掉山羊。船夫能否将它们（包括狼、山羊、卷心菜）安全送到河对岸？

其实这只是一道很简单的智力题，我们几乎马上可以得到其中一种答案：

而今天我们要做的就是让计算机来给出我们这样一个答案。

分析过河过程：从问题的描述可以看出,在过河的过程中船夫是具有选择权的（这个选择交由计算机执行），他可以选择搭载或者不搭载物品（即狼，羊，菜）。而且，船夫只有和某物品处在同一侧岸边，他才有可能搭载这个物品，并且最多只能搭载一个。这就意味着，若船夫同狼、羊、菜分别位于河的两岸时，就没有办法搭载它们了。根据以上过河过程的分析，我们可以建立这样一个迁移状态：

船夫：在此岸或者彼岸山羊：在此岸或者彼岸狼：在此岸或者彼岸卷心菜：在此岸或者彼岸初始时船夫：此岸山羊：此岸狼：此岸卷心菜：在此岸下个状态船夫：在此岸或彼岸

（搭载物品？由计算机在满足条件的物品中随机选择）狼：若此时和船夫同处一岸又被选中，则下个状态在对岸，否则还在此地。山羊：若此时和船夫同处一岸又被选中，则下个状态在对岸，否则还在此地。卷心菜：若此时和船夫同处一岸又被选中，则下个状态在对岸，否则还在此地。

上述迁移状态用NuSMV语言表达则为：MODULEmainVARferryman:boolean;goat:boolean;cabbage:boolean;wolf:boolean;carry:{g,c,w,0};ASSIGNinit(ferryman):=0;init(goat):=0;init(cabbage):=0;init(wolf):=0;init(carry):=0;next(ferryman):=!ferryman;next(goat):=casenext(carry):=caseferryman=goat&next(carry)=g:next(ferryman);ferryman=goat:g;1:goat;1:0;esac;esacunionnext(cabbage):=casecaseferryman=cabbage&next(carry)=c:next(ferryman);ferryman=cabbage:c;1:cabbage;1:0;esac;esacunionnext(wolf):=casecaseferryman=wolf&next(carry)=w:next(ferryman);ferryman=wolf:w;1:wolf;1:0;esac;esacunion0;

以上过河程序计算机在运行时可以产生多个状态迁移，关系图如下：LTL

线性时态逻辑LTL(Linear-timeTemporalLogic)

带有允许指示未来的连接词，它将时间建模成状态的序列，无限延伸到未来，这个状态序列有时称为计算路径，一般我们考虑若干路径，代表不同的可能未来，任何一种都可能是实现的“实际”路径。在LTL语法定义的公式中，二元连接词U(代表until)是最常见的一个，公式在一条路径上成立，如果连续地成立直到成立，此外,实际上要求在某个未来状态确实成立。如图，沿着所示的路径，

到的每个状态都满足pUq，但到不满足。LTL语义中Until含义的解释.假设p

在(且只在)点满足q在(且只在)点满足,那么沿着所示路径只有到满足pUq

运行结果告诉我们这个取否定的表达式isfalse，并显示了一条路径来说明可以找到使船夫、狼、山羊、卷心菜都安全到达彼岸的方法。

这条路径就是摆渡者难题的一个答案，也是我们一开始最希望计算机给出的。

由摆渡者难题可以看到计算机只是在机械地进行遍历，在遍历过程中如果找到不满足我们给的条件的路径就显示此条件为假，不然就一直遍历完所有状态显示我们给的条件是真的。

问题分析摆渡者难题之所以我们能够很快得到答案，是因为有一个隐含条件：只有船夫才能划船，即船夫在渡河问题中既充当了船的角色同时又是狼、羊、菜之间能够安全相处的重要因素。八人渡河问题与摆渡者难题最大的不同在于，船夫的唯一性发生了改变，船夫由一人变为三人。也就是说，船在哪岸会划船的人不一定也在哪岸，不能再将船和划船人等同看待，而要把船看作一个独立的事物。同时还要设置一个记号来标记由计算机选择的船夫。{猎人、女人、老人}{猎人、狼、女人、孩子1、孩子2、老人、孩子3、孩子4}

next(hunter):=case(next(ferryman)=h|next(carry)=h)&boat=hunter:next(boat);--511:hunter;esac;next(female):=case(next(ferryman)=f|next(carry)=f)&boat=female:next(boat);--551:female;esac;next(older):=case(next(ferryman)=o|next(carry)=o)&boat=older:next(boat);1:older;esac;next(wolf):=casenext(child3):=caseboat=wolf&next(carry)=w:next(boat);boat=child3&next(carry)=c3:next(boat);1:wolf;1:child3;esac;esac;next(child1):=caseboat=child1&next(carry)=c1:next(boat);next(child4):=case1:child1;boat=child4&next(carry)=c4:next(boat);esac;1:child4;next(child2):=caseesac;boat=child2&next(carry)=c2:next(boat);1:child2;esac;

八人过河问题的安全性条件为：某一时刻包括狼在内的八人都到达彼岸，且在这一时刻之前狼不能伤人，所有的孩子也不能挨打。这也就是说当狼和除猎人以外的人同在一侧河岸时，猎人也必须在这侧河岸以保证狼不能咬人。女人或老人只有在对方也在时，才能和对方的孩子同处一地。用LTL公式表达如下：!((((female=child3|female=child4)->female=older)&((older=child1|older=child2)->older=female)&((wolf=female|wolf=child1|wolf=child2|wolf=older|wolf=child3|wolf=child4)->wolf=hunter))U(hunter&wolf&female&child1&child2&older&child3&child4))

如此建立模型,虽然可以得到一条安全路径,但显然计算机的工作量很大，会划船的有3个人，每人都可以有2个状态即此岸和彼岸，在每个状态下都有可能载人，而需要被搭载的有8个人，每个人又有2个状态(此岸或彼岸)被载等等，这样看来整个迁移系统就非常庞大复杂了，是否能简化一下整个系统呢？我们的做法是将所有人划分为两个类，会划船的人和不会划船的人，首先让计算机在会划船的人中选出1~2人坐船，这样共有6个选择(+)，而在选1个会划船时,才再选不会划船的人,又有6个选择(5人和0人)，如此做法就会使整个迁移系统简化不少，显然机器遍历时速度快了。

限时过桥问题某合唱团的4名成员A,B,C,D赶往演出现场，他们途中要经过一座小桥。当他们赶到桥头时，天已经黑了，周围没有灯，他们只有一只手电筒。桥很窄一次最多只许2人一起过桥，过桥人手里必须有手电筒。4个人的步行速度都不同，若2人同行，则以较慢者的速度为准。A需花1分钟过桥，B过桥需要2分钟，C需花5分钟，D需花10分钟过桥。请问：他们能在17分钟内过桥吗？

问题分析很明显，开始两人拿着手电筒过桥后，手电筒就在桥的另一边了，此时需要已经过桥的那两人中的一个人再把手电筒送回桥这边。送手电筒回来过桥也要花时间，所以就要用限定的时间减去两个人中较慢的那个人所花的时间，再减掉送手电筒那人用的时间。

过桥过程的程序如下：MODULEmaininit(torch):=0;init(person1):=0;VARinit(person2):=0;init(time):=0;personA:boolean;personB:boolean;init(total):=17;personC:boolean;personD:boolean;next(person1):=casetorch:boolean;person1:{1,2,5,10,0};personA=torch:1;person2:{1,2,5,10,0};total:-10..20;1:0;time:{1,2,5,10,0};esacunionASSIGNcaseinit(personA):=0;init(personB):=0;personB=torch:2;init(personC):=0;init(personD):=0;1:0;esacunion

上一次我们主要讲了布尔型变量问题，这次主要内容是非布尔型变量问题，包括枚举型和整型。这里枚举型例子包括一个符号枚举型和一个整符枚举型，当然这里主要是同层次的枚举型问题，非层次的枚举问题将在下一次的内容中进行演示。猜猜谁是谁

老张、老王和老周，他们分别是教师、律师和医生。他们之间有如下关系：（1）老王比教师矮一些；（2）老张比医生高些；（3）老周比医生矮一些；

猜猜看：他们谁是律师，谁是教师，谁是医生呢？

MODULEmainVAR

wang:{d,t,l,0};next(zhou):=case

zhang:{d,t,l,0};next(zhang)=t:l;

zhou:{d,t,l,0};1:{t,l};ASSIGNesac;

init(wang):=0;LTLSPEC

init(zhang):=0;!F(wang!=zhang&wang!=zhou)

init(zhou):=0;

next(wang):={d,l};

next(zhang):=case

next(wang)=d:t;

1:{t,l};

esac;山羊买外套小白羊、小黑羊、小灰羊一起上街各买了一件外套。三件外套的颜色分别是白色、黑色、灰色。回家路上，一只小羊说：“我很久以前就想买白外套，今天终于买到了！”说到这里，她好像是发现了什么，惊喜地对同伴说：“今天我们可真有意思，白羊没有买白外套，黑羊没有买黑外套，灰羊没有买灰外套。”小黑羊说：“真是这样，你要是不说，我还真没注意这一点呢！”你能根据他们的对话，猜出小白羊、小黑羊、小灰羊各买了什么颜色的外套吗？

建模过程：

根据画线部分可以分析得出白羊goatw的外套颜色为黑色（b)或是灰色(g)，黑羊goatb的外套颜色为白色(w)或是灰色(g)，而灰羊goatg的外套颜色则为黑色(b)或是白色(w)。

而且黑羊的话说明他的外套颜色不可能是白色（题目中隐含了三只羊的外套颜色不能重复）。那么可以得出这个问题的LTL公式可以表示为：!F((goatw!=goatb)&(goatw!=goatg)&(goatb!=w))门铃问题某户的门铃声整天不断，于是，他请人在大门前设计了一排6个按钮，其中只有一个是通门铃的。来访者只要摁错了一个按钮，哪怕是和正确的同时摁，整个电铃系统将立即停止工作。在大门的按钮旁边，贴有一张告示，上面写着：“A在B的左边；B是C右边的第三个；C在D的右边；D紧靠着E；E和A中间隔一个按钮。请摁上面没有提到的那个按钮。”问：这6个按钮中，通门铃的按钮处于什么位置？建模过程：根据分析，B是C右边第三个门铃，那么可以门铃位置可以确定为CxxB。又D在C的左边，那么就是说C的左边仍然有门铃，C的位置不可能是1，4，5，6，这样就可以确定C的位置只能是2或者3。当C的位置确定时，B的位置相应的也就确定了；而D的位置可以根据C的位置来判断，当C的位置是2时，D的位置就只能是1

了；当C的位置是３时，D的位置可能是１或者２；同理E的位置可以根据D的位置来判断可能性，而Ａ呢可以根据Ｅ的位置来判断。各门铃位置不重复，所以Ａ、Ｅ、Ｃ位置各不同。用LTL公式表示为：

!F(a!=c&c!=e)

MODULEmainnext(b):=caseVARnext(c)=2:5;

a:{1,2,3,4,5,6,0};1:6;

b:{1,2,3,4,5,6,0};esac;

c:{1,2,3,4,5,6,0};next(e):=case

d:{1,2,3,4,5,6,0};next(d)=1:2;

e:{1,2,3,4,5,6,0};1:{1,3};ASSIGNesac;

init(a):=0;next(a):=case

init(b):=0;next(e)=1:3;

init(c):=0;next(e)=2:4;

init(d):=0;1:{1,5};

init(e):=0;esac;

next(c):={2,3};LTLSPEC

next(d):=case!F(a!=c&c!=e)

next(c)=2:1;

1:{1,2};

esac;

身份辨认我毕业于一所政法大学，我的同学(包括我在内)不是做了法官就是做了律师。在一次同学聚会上，有16位同学出席。我统计了一