人鬼过河游戏
有三个人，三只鬼，在河流的同一 侧。河中有一只两个座位的小船，小船 需要人或者鬼的操作才能从河的一侧 运动到河的另一侧。当河的一岸鬼的 数目大于人的数目，鬼会吃同岸的人。 系统不允许这种状态发生。系统如何 操作才能将人鬼全部安全的移动到河 的另一侧。
网页版游戏
人鬼过河在 Maude 中建模
POSITION模块
位置模块，该模块完成对位置的 建模，河只有“Left”、“Right”两岸。
fmod POSITION is
sort Position .
op !_ : Position -> Position .
ops Left Right : -> Position .
---var Left Right : Position
eq !( Left ) = Right .
eq !( Right ) = Left .
endfm
PASSENGER模块
该模块完成乘客的建模，乘客有两种，分别是人和鬼。
fmod PASSENGER is
including QID-LIST .
including POSITION .
sorts Type Passenger .
ops M G : -> Type .
op P(_,_) : Type Position -> Passenger [ctor] .
endfm
BOAT模块
完成对船的建模，船和乘客一样，有位置信息。船的载荷在其他模块中实现。
fmod BOAT is
sort Boat .
including POSITION .
op B(_) : Position -> Boat .
endfm
STATE模块
完成对系统状态的建模，乘客和船的位置共同组成了系统状态。
fmod STATE is
sort State .
including PASSENGER .
including BOAT .
subsort Passenger < State .
subsort Boat < State .
op nil : -> State [ctor].
op _,_ : State State -> State [ctor assoc id: nil] .
endfm
SAFE模块
此模块完成了实现了人和鬼计数功能，并且完成对系统安全的定义。
fmod SAFE is
including STATE .
including PASSENGER .
including POSITION .
op Safe(_) : State -> Bool .
var p1 : Position .
var s1 : State .
var t1 : Type .
var b1 : Boat .
ops numML(_) numGL(_) numMR(_) numGR(_) : State -> Nat .
eq numML(nil) = 0 .
eq numML(b1) = 0 .
ceq numML( P( t1 , p1 ) , s1 ) = 1 + numML(s1)
if p1 == Left /\ t1 == M .
ceq numML( P( t1 , p1 ) , s1 ) = numML(s1)
if p1 == Right .
ceq numML( P( t1 , p1 ) , s1 ) = numML(s1)
if t1 == G .
eq numGL(nil) = 0 .
eq numGL(b1) = 0 .
ceq numGL(P(t1,p1),s1) = 1 + numGL(s1)
if p1 == Left /\ t1 == G .
ceq numGL(P(t1,p1),s1) = numGL(s1)
if p1 == Right .
ceq numGL(P(t1,p1),s1) = numGL(s1)
if t1 == M .
eq numMR(nil) = 0 .
eq numMR(b1) = 0 .
ceq numMR(P(t1,p1),s1) = 1 + numMR(s1)
if p1 == Right /\ t1 == M .
ceq numMR(P(t1,p1),s1) = numMR(s1)
if p1 == Left .
ceq numMR(P(t1,p1),s1) = numMR(s1)
if t1 == G .
eq numGR(nil) = 0 .
eq numGR(b1) = 0 .
ceq numGR(P(t1,p1),s1) = 1 + numGR(s1)
if p1 == Right /\ t1 == G .
ceq numGR(P(t1,p1),s1) = numGR(s1)
if p1 == Left .
ceq numGR(P(t1,p1),s1) = numGR(s1)
if t1 == M .
ceq Safe(s1) = false
if (numMR(s1) < numGR(s1)) /\ (numMR(s1) > 0 ) .
ceq Safe(s1) = false
if (numML(s1) > 0) /\ (numML(s1) < numGL(s1)) .
ceq Safe(s1) = true
if (numMR(s1) == numGR(s1)) /\ (numML(s1) == numGL(s1)) .
ceq Safe(s1) = true
if (numMR(s1) > numGR(s1)) /\ (numML(s1) == 0) .
ceq Safe(s1) = true
if (numMR(s1) == 0 ) /\ (numML(s1) > numGL(s1)) .
endfm
GM_SYSTEM
完成转移规则的建模，定义初始状态和结束状态。
mod GM_SYSTEM is
including BOAT .
including SAFE .
including PASSENGER .
including POSITION .
var L R : Position .
op init : -> State .
eq init = P(M,Left), P(M,Left), P(M,Left), P(G,Left), P(G,Left), P(G,Left), B(Left) .
op finish : -> State .
eq finish = P(M,Right), P(M,Right), P(M,Right), P(G,Right), P(G,Right), P(G,Right), B(Right) .
---var B1 : Boat .
---vars P1 P2 P3 P4 P5 P6 : Passenger .
vars t1 t2 t3 t4 t5 t6 : Type .
vars p1 p2 p3 p4 p5 p6 : Position .
vars s1 s2 s3 s4 : State .
crl s1, P(t1,p1), s2, P(t2,p1), s3, B(p1) =>
s1, P(t1,!(p1)), s2, P(t2,!(p1)), s3, B(!(p1))
if Safe(s1, P(t1,!(p1)), s2, P(t2,!(p1)), s3 )
== true .
crl s1, P(t1,p1), s2, B(p1) =>
s1, P(t1,!(p1)), s2, B(!(p1))
if Safe(s1, P(t1,!(p1)), s2 )
== true .
endm
实验效果
S0=“P(M,Left), P(M,Left), P(M,Left), P(G,Left), P(G,Left), P(G,Left), B(Left)”，能否达到Sfinal=“P(M,Right), P(M,Right), P(M,Right), P(G,Right), P(G,Right), P(G,Right), B(Right)”。
操作语句：
load ghost.maude .
search [1] P(M,Left), P(M,Left), P(M,Left), P(G,Left), P(G,Left), P(G,Left), B(Left) =>* P(M,Right), P(M,Right), P(M,Right), P(G,Right), P(G,Right), P(G,Right), B(Right) .
show search graph .
实验效果：