;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Blocksworld
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(role robot)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(init (clear b))
(init (clear c))
(init (table a))
(init (table b))
(init (on c a))
(init (step 1))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (legal robot (s ?x ?y))
    (true (clear ?x))
    (true (clear ?y))
    (true (table ?x))
    (distinct ?x ?y))
(<= (legal robot (u ?x ?y))
    (true (clear ?x))
    (true (on ?x ?y)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (next (on ?x ?y))
    (does robot (s ?x ?y)))
(<= (next (on ?x ?y))   ; nötig für den Frame
    (does robot (s ?u ?v))
    (true (on ?x ?y)))
(<= (next (table ?x))   ; nötig für den Frame
    (does robot (s ?u ?v))
    (true (table ?x))
    (distinct ?u ?x))
(<= (next (clear ?y))   ; nötig für den Frame
    (does robot (s ?u ?v))
    (true (clear ?y))
    (distinct ?v ?y))

(<= (next (table ?x))
    (does robot (u ?x ?y)))
(<= (next (clear ?y))
    (does robot (u ?x ?y)))
(<= (next (on ?x ?y))   ; nötig für den Frame
    (does robot (u ?u ?v))
    (true (on ?x ?y))
    (distinct ?u ?x))
(<= (next (table ?x))   ; nötig für den Frame
    (does robot (u ?u ?v))
    (true (table ?x)))
(<= (next (clear ?x))   ; nötig für den Frame
    (does robot (u ?u ?v))
    (true (clear ?x)))

(<= (next (step ?y))
    (true (step ?x))
    (succ ?x ?y))
)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= terminal
    (true (step 4)))
(<= terminal
    (true (on a b))
    (true (on b c)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (goal robot 100)
    (true (on a b))
    (true (on b c)))
(<= (goal robot 0)
    (not (true (on a b))))
(<= (goal robot 0)
    (not (true (on b c))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(succ 1 2)
(succ 2 3)
(succ 3 4)