The Farmer, Fox, Chicken and Grain problem (in maude)

In my previous post I solved this problem with prolog. Here I have written a solution using the rewrite logic of the Maude system.


mod FARMER is
        sort GameState .
        sort Bank .
        sort Actor .
        subsort Actor < Bank .

        op state : Bank Bank -> GameState [ ctor ] .
        ops Farmer, Fox, Chicken, Grain : -> Actor [ ctor ] .

        op Empty : -> Bank [ ctor ] .
        op __ : Bank Bank -> Bank [ctor assoc comm id: Empty] .

        op safe : Bank -> Bool .

        vars A1 : Actor .
        vars X Y Z : Bank .
        eq safe( Farmer X ) = true .
        eq safe( Chicken Fox X) = false .
        eq safe( Chicken Grain X) = false .
        eq safe( X ) = true [owise] .

        crl [cross_with] : state((Farmer A1 X),Y) => state(X,(Farmer A1 Y)) if safe(X) .
        crl [cross_alone] : state((Farmer X),Z) => state(X,(Farmer Z)) if safe(X) .
        crl [cross_back_with] : state(X,(Farmer A1 Z)) => state((Farmer A1 X),Z) if safe(Z) .
        crl [cross_back_alone] : state(X,(Farmer Z)) => state((Farmer X),Z) if safe(Z) .
endm

Maude has a built-in search mechanism that allows us to find a solution:


Maude> search state(Farmer Fox Chicken Grain,Empty) =>+ state(Empty, Farmer Grain Chicken Fox) .
search in FARMER : state(Farmer Fox Chicken Grain, Empty) =>+ state(Empty, Farmer Fox Chicken Grain) .

Solution 1 (state 9)
states: 10  rewrites: 43 in 0ms cpu (0ms real) (~ rewrites/second)
empty substitution

No more solutions.
states: 10  rewrites: 50 in 0ms cpu (0ms real) (~ rewrites/second)
Maude> show path 9 .
state 0, GameState: state(Farmer Fox Chicken Grain, Empty)
===[ crl state(Farmer X A1, Y) => state(X, Farmer Y A1) if safe(X) = true [label cross_with] . ]===>
state 1, GameState: state(Fox Grain, Farmer Chicken)
===[ crl state(X, Farmer Z) => state(Farmer X, Z) if safe(Z) = true [label cross_back_alone] . ]===>
state 2, GameState: state(Farmer Fox Grain, Chicken)
===[ crl state(Farmer X A1, Y) => state(X, Farmer Y A1) if safe(X) = true [label cross_with] . ]===>
state 3, GameState: state(Grain, Farmer Fox Chicken)
===[ crl state(X, Farmer Z A1) => state(Farmer X A1, Z) if safe(Z) = true [label cross_back_with] . ]===>
state 5, GameState: state(Farmer Chicken Grain, Fox)
===[ crl state(Farmer X A1, Y) => state(X, Farmer Y A1) if safe(X) = true [label cross_with] . ]===>
state 7, GameState: state(Chicken, Farmer Fox Grain)
===[ crl state(X, Farmer Z) => state(Farmer X, Z) if safe(Z) = true [label cross_back_alone] . ]===>
state 8, GameState: state(Farmer Chicken, Fox Grain)
===[ crl state(Farmer X A1, Y) => state(X, Farmer Y A1) if safe(X) = true [label cross_with] . ]===>
state 9, GameState: state(Empty, Farmer Fox Chicken Grain)