线性时序逻辑-模型检测-maude-狼羊白菜

线性时序逻辑-模型检测-maude-狼羊白菜过河问题是可以用到Maude中 LTL模型检测的一个例子。过河问题是一个古老的智力游戏题，讲的是一个牧羊人要用一条小船把一只狼，一只羊和一颗白菜从河的这岸送到彼岸。连带牧羊人小船一次只能拉两样事物；并且当牧羊人不在附近的时候：狼和羊在一起，狼会吃掉羊；羊和白菜在一起，羊会吃掉白菜。摆渡者怎样才能顺利完成摆渡任务？场景代码布置如下。有 left和 right两岸，有牧羊人，狼，羊，白菜等事物。这些事物所处位置构成系统状态。 sorts Side Group . ops left right : ->...

过河问题是可以用到Maude中 LTL模型检测的一个例子。过河问题是一个古老的智力游戏题，讲的是一个牧羊人要用一条小船把一只狼，一只羊和一颗白菜从河的这岸送到彼岸。连带牧羊人小船一次只能拉两样事物；并且当牧羊人不在附近的时候：狼和羊在一起，狼会吃掉羊；羊和白菜在一起，羊会吃掉白菜。摆渡者怎样才能顺利完成摆渡任务？场景代码布置如下。有 left和 right两岸，有牧羊人，狼，羊，白菜等事物。这些事物所处位置构成系统状态。 sorts Side Group . ops left right : -> Side . op change_ : Side -> Side . eq change(left) = right . eq change(right) = left . ops shepherd wolf lamb cabbage : Side -> Group [ctor] . op __ : Group Group -> Group [ctor assoc comm] . 迁移规则分别是 shepherd:牧羊人单独从河的某岸到另一岸；wolf:牧羊人带着狼从某岸到另一岸；lamb: 牧羊人带着小羊从某岸到另一岸；cabbage：牧羊人带着狼从某岸到另一岸。 vars S S' S'' : Side . rl [shepherd] : shepherd(S) => shepherd(change(S)) . rl [wolf] : shepherd(S) wolf(S) => shepherd(change(S)) wolf(change(S)) . rl [lamb] : shepherd(S) lamb(S) => shepherd(change(S)) lamb(change(S)) . rl [cabbage] : shepherd(S) cabbage(S) => shepherd(change(S)) cabbage(change(S)) . 起先，所有事物都在河的左岸，初始状态： shepherd(left),wolf(left),lamb(left),cabbage(left) 牧羊人所要完成的任务可以描述为：在不产生损失的情况下，到达 shepherd(right),wolf(right),lamb(right),cabbage(right) “ ”为了能表示损失，使用Maude中的MODEL-CHECKER模块： including MODEL-CHECKER . subsort Group < State . ops disaster success : -> Prop . ceq ((wolf(S) lamb(S) shepherd(S') cabbage(S'')) |= disaster) = true if S =/= S' . ceq ((wolf(S'') lamb(S) shepherd(S') cabbage(S)) |= disaster) = true if S =/= S' . eq ((shepherd(right) wolf(right) lamb(right) cabbage(right)) |= success) = true . 现在我们就可以用一个 LTL（线性时序逻辑）公式来表示符合要求的解决方案 : E success and (¬ disaster until success)，意思是有一个方案使得 “ ”最终可以成功，并且成功之前不会有灾难。而在 LTL模型检测中，我们通常给出要检测性质的否定，然后得到反例就是原问题的解。 “ ”原任务不可能完成的表达是所有通到成功的道路中必然要经过失败 , “或者说如果最终有成功， ”那么最终有灾难并且不成功直到出现灾难。公式表达为： E success —> ( E disaster and ¬success until disaster) maude代码表达为： red modelCheck(initial, <> success -> (<> disaster /\ ((~ success) U disaster))) . 把以上代码写入一个文件 crossing-river.maude 。打开maude 解释器：～$ ./maude.linux 在maude解释器里执行 crossing-river.maude的代码： Maude > in crossing-river.maude . (如下图)

                    本文档为【线性时序逻辑-模型检测-maude-狼羊白菜】，请使用软件OFFICE或WPS软件打开。作品中的文字与图均可以修改和编辑，
                    图片更改请在作品中右键图片并更换，文字修改请直接点击文字进行修改，也可以新增和删除文档中的内容。 
 该文档来自用户分享，如有侵权行为请发邮件ishare@vip.sina.com联系网站客服，我们会及时删除。

                    [版权声明] 本站所有资料为用户分享产生，若发现您的权利被侵害，请联系客服邮件isharekefu@iask.cn，我们尽快处理。

                    本作品所展示的图片、画像、字体、音乐的版权可能需版权方额外授权，请谨慎使用。

                    网站提供的党政主题相关内容(国旗、国徽、党徽..)目的在于配合国家政策宣传，仅限个人学习分享使用，禁止用于任何广告和商用目的。
                

下载需要：免费已有0 人下载

立即下载

线性时序逻辑-模型检测-maude-狼羊白菜

你可能还喜欢