example-battleship-1x4.limbo

// A 1x4-battleship game with a 3-ship.
// The output of the game is very limited; sorry for that.

Call: disable_query_logging()

Sort POS
Var p, q -> POS
Name p0, p1, p2, p3, p4, p5 -> POS
Fun n/1, s/1 -> POS

KB:  n(p1)=p0
KB:  n(p2)=p1
KB:  n(p3)=p2
KB:  n(p4)=p3
KB:  n(p5)=p4

// KB: ~n(p1)=p4
// KB: ~s(p4)=p3

KB: n(s(p))=p
KB: s(n(p))=p
// KB: ~n(p)=p
// KB: ~s(p)=p

// KB: s(p0)=p1
// KB: s(p1)=p2
// KB: s(p2)=p3
// KB: s(p3)=p4
// KB: s(p4)=p5

Sort SHIP
Var x, y -> SHIP
Name three -> SHIP
Fun head/1 -> POS
Fun body/1 -> POS
Fun tail/1 -> POS

Sort BOOL
Name T -> BOOL
Fun water/1 -> BOOL
Fun fired/1 -> BOOL

KB: s(head(three))=body(three)
KB: n(body(three))=head(three)
KB: s(body(three))=tail(three)
KB: n(tail(three))=body(three)

KB: ~water(head(three))=T
KB: ~water(body(three))=T
KB: ~water(tail(three))=T

KB: water(n(head(three)))=T
KB: water(s(tail(three)))=T

KB: p=p1 v p=p2 v p=p3 v p=p4 v water(p)=T
// We don't need the following in the KB. If we do have it, however,
// split level 1 suffices for the assertions below.
//KB: head(three)=p v body(three)=p v tail(three)=p v water(p)=T
Assert: G Fa p K<2> (head(three)=p v body(three)=p v tail(three)=p v water(p)=T)

Call: bs_init(p1, p2, p3, p4)
Call: bs_print()


while Ex p G (~K<0> fired(p)=T ^ ~K<2> water(p)=T) {
    for P -> POS    G (~K<0> fired(P)=T ^ K<2> ~water(P)=T) {
        Call: bs_fire(P)
        Call: print(P)
    } else if P -> POS   G (~K<0> fired(P)=T ^ ~K<2> water(P)=T ^ ~K<2> ~water(P)=T) {
       Call: bs_fire(P)
       Call: print(P,P)
    }
    Call: bs_print()
}