; Catcha mouse
(role mouse)
(role catcher)

; Initial conditions
(init (control catcher))

(init (cell 1 1 empty))
(init (cell 1 2 empty))
(init (cell 1 3 empty))
(init (cell 1 4 empty))
(init (cell 1 5 empty))
(init (cell 1 6 hole))
(init (cell 1 7 empty))
(init (cell 1 8 empty))
(init (cell 1 9 empty))

(init (cell 2 a empty))
(init (cell 2 b empty))
(init (cell 2 c empty))
(init (cell 2 d hole))
(init (cell 2 e hole))
(init (cell 2 f empty))
(init (cell 2 g empty))
(init (cell 2 h empty))

(init (cell 3 1 empty))
(init (cell 3 2 empty))
(init (cell 3 3 empty))
(init (cell 3 4 hole))
(init (cell 3 5 trap))
(init (cell 3 6 empty))
(init (cell 3 7 hole))
(init (cell 3 8 empty))
(init (cell 3 9 empty))

(init (cell 4 a empty))
(init (cell 4 b empty))
(init (cell 4 c empty))
(init (cell 4 d empty))
(init (cell 4 e empty))
(init (cell 4 f empty))
(init (cell 4 g hole))
(init (cell 4 h empty))

(init (cell 5 1 empty))
(init (cell 5 2 empty))
(init (cell 5 3 empty))
(init (cell 5 4 empty))
(init (cell 5 5 empty))
(init (cell 5 6 hole))
(init (cell 5 7 empty))
(init (cell 5 8 empty))
(init (cell 5 9 empty))

(init (cell 6 a empty))
(init (cell 6 b empty))
(init (cell 6 c trap))
(init (cell 6 d empty))
(init (cell 6 e empty))
(init (cell 6 f hole))
(init (cell 6 g empty))
(init (cell 6 h empty))

(init (cell 7 1 mouse))
(init (cell 7 2 empty))
(init (cell 7 3 empty))
(init (cell 7 4 empty))
(init (cell 7 5 empty))
(init (cell 7 6 empty))
(init (cell 7 7 empty))
(init (cell 7 8 empty))
(init (cell 7 9 empty))
(init (step 0))

; Legal moves
(<= (legal ?p noop)
    (role ?p)
    (not (true (control ?p))))
(<= (legal catcher (lay_trap ?x ?y))
    (true (control catcher))
    (true (cell ?x ?y empty)))
(<= (legal mouse (move ?x ?y))
    (true (control mouse))
    (true (cell ?mx ?my mouse))
    (true (cell ?x ?y ?something))
    (connected ?mx ?x)
    (connected ?my ?y))
(<= (legal mouse (move ?x ?y))
    (true (control mouse))
    (true (cell ?x ?my mouse))
    (true (cell ?x ?y ?something))
    (connected ?my ?y))

(<= (next (step ?new_step))
    (true (step ?old_step))
    (++ ?old_step ?new_step))

; Transition rules
(<= (next (cell ?x ?y mouse))
    (does mouse (move ?x ?y)))
(<= (next (cell ?x ?y mouse))
    (true (cell ?x ?y mouse))
    (true (control catcher)))
(<= (next (cell ?x ?y trap))
    (true (cell ?x ?y trap)))
(<= (next (cell ?x ?y hole))
    (true (cell ?x ?y hole)))
(<= (next (cell ?x ?y trap))
    (does catcher (lay_trap ?x ?y)))
(<= (next (cell ?x ?y empty))
    (true (cell ?x ?y empty))
    (not (does catcher (lay_trap ?x ?y)))
    (not (does mouse (move ?x ?y))))
(<= (next (cell ?x ?y empty))
    (true (cell ?x ?y mouse))
    (true (control mouse)))
(<= (next (control mouse))
    (true (control catcher)))
(<= (next (control catcher))
    (true (control mouse)))

(<= terminal
    caught)

(<= terminal
    escaped)

(<= terminal
    (true (step 20)))

(<= (goal catcher 100)
    caught)
(<= (goal catcher 0)
    (not caught))
(<= (goal mouse 100)
    escaped)
(<= (goal mouse 0)
    (not escaped))

; General knowledge
(<= caught
    (true (cell ?x ?y mouse))
    (true (cell ?x ?y trap)))

(<= escaped
    (true (cell ?x ?y mouse))
    (true (cell ?x ?y hole)))

(succ 1 2)
(succ 2 3)
(succ 3 4)
(succ 4 5)
(succ 5 6)
(succ 6 7)
(succ 7 8)
(succ 9 10)

(succ 1 a)
(succ 2 b)
(succ 3 c)
(succ 4 d)
(succ 5 e)
(succ 6 f)
(succ 7 g)
(succ 8 h)

(succ a b)
(succ b c)
(succ c d)
(succ d e)
(succ e f)
(succ f g)
(succ g h)

(succ h 9)

(<= (connected ?first ?second)
    (succ ?first ?second))
(<= (connected ?second ?first)
    (succ ?first ?second))

(++ 0 1)
(++ 1 2)
(++ 2 3)
(++ 3 4)
(++ 4 5)
(++ 5 6)
(++ 6 7)
(++ 7 8)
(++ 8 9)
(++ 9 10)
(++ 10 11)
(++ 11 12)
(++ 12 13)
(++ 13 14)
(++ 14 15)
(++ 15 16)
(++ 16 17)
(++ 17 18)
(++ 18 19)
(++ 19 20)