;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;; Dots and Boxes ;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;; Roles ;;;;;;;;;;;

(role misterx)
(role mistery)

;;;;;;;; Initials ;;;;;;;;

(init (cell 2 1 b))
(init (cell 4 1 b))

(init (cell 1 2 b))
(init (cell 3 2 b))
(init (cell 5 2 b))

(init (cell 2 3 b))
(init (cell 4 3 b))

(init (cell 1 4 b))
(init (cell 3 4 b))
(init (cell 5 4 b))

(init (cell 2 5 b))
(init (cell 4 5 b))

(init (points misterx 0))
(init (points mistery 0))

(init (control misterx))
(init (round 0))

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


;;; Markierungen ;;;
(<= (next (cell ?x ?y f))
    (does ?r (mark ?x ?y))
    (true (cell ?x ?y b))
)
	
(<= (next (cell ?x ?y f))
    (true (cell ?x ?y f))
)
	
(<= (next (cell ?x ?y b))
    (does ?r (mark ?i ?j))
    (true (cell ?x ?y b))
    (or
        (distinct ?x ?i)
        (distinct ?y ?j)
    )
)

;;; Hat ein Spieler gepunktet? ;;;
(<= (justBoxed ?r)
    (true (control ?r))
    (or
        (newBox 1 1)
        (newBox 1 2)
        (newBox 2 1)
        (newBox 2 2)
    )
)
	
;;; Punkte werden vergeben ;;;
(<= (next (points ?r 1))
    (true (points ?r 0))
    (true (control ?r))
    (or
        (newBox 1 1)
        (newBox 1 2)
        (newBox 2 1)
        (newBox 2 2)
    )
)
	
(<= (next (points ?r 2))
    (or 
        (and
            (true (points ?r 0))
            (true (control ?r))
            (or
                (and
                    (newBox 1 1)
                    (newBox 1 2)
                )
                (and
                    (newBox 1 2)
                    (newBox 2 2)
                )
                (and
                    (newBox 2 1)
                    (newBox 1 1)
                )
                (and
                    (newBox 2 2)
                    (newBox 2 1)
                )
            )
        )
        (and
            (true (points ?r 1))
            (true (control ?r))
            (or
                (newBox 1 1)
                (newBox 1 2)
                (newBox 2 1)
                (newBox 2 2)
            )
        )
    )
)

(<= (next (points ?r 3))
    (or 
        (and
            (true (points ?r 1))
            (true (control ?r))
            (or
                (and
                    (newBox 1 1)
                    (newBox 1 2)
                )
                (and
                    (newBox 1 2)
                    (newBox 2 2)
                )
                (and
                    (newBox 2 1)
                    (newBox 1 1)
                )
                (and
                    (newBox 2 2)
                    (newBox 2 1)
                )
            )
        )
        (and
            (true (points ?r 2))
            (true (control ?r))
            (or
                (newBox 1 1)
                (newBox 1 2)
                (newBox 2 1)
                (newBox 2 2)
            )
        )
    )
)
	
(<= (next (points ?r 4))
    (or 
        (and
            (true (points ?r 2))
            (true (control ?r))
            (or
                (and
                    (newBox 1 1)
                    (newBox 1 2)
                )
                (and
                    (newBox 1 2)
                    (newBox 2 2)
                )
                (and
                    (newBox 2 1)
                    (newBox 1 1)
                )
                (and
                    (newBox 2 2)
                    (newBox 2 1)
                )
            )
        )
        (and
            (true (points ?r 3))
            (true (control ?r))
            (or
                (newBox 1 1)
                (newBox 1 2)
                (newBox 2 1)
                (newBox 2 2)
            )
        )
    )
)

;;; alte Punkte bleiben erhalten ;;;
(<= (next (points ?r ?n))
    (true (points ?r ?n))
    (not (newBox 1 1))
    (not (newBox 1 2))
    (not (newBox 2 1))
    (not (newBox 2 2))
)
(<= (next (points ?r ?n))
    (true (points ?r ?n))
    (not (true (control ?r)))
)

;;; entsteht eine neue Box? ;;;
(<= (newBox ?x ?y)
    (not (true (box ?x ?y)))
    (nextt (box ?x ?y))
)
	
;;; next-Praedikate, die man auch auf der anderen Seite der Implikation nutzen kann
(<= (nextt (box ?x ?y))
    (true (box ?x ?y))
)
	
(<= (nextt (box 1 1))
    (oneLeft 1 1 (mark 2 1))
    (does ?r (mark 2 1))
)
(<= (nextt (box 1 1))
    (oneLeft 1 1 (mark 1 2))
    (does ?r (mark 1 2))
)
(<= (nextt (box 1 1))
    (oneLeft 1 1 (mark 3 2))
    (does ?r (mark 3 2))
)
(<= (nextt (box 1 1))
    (oneLeft 1 1 (mark 2 3))
    (does ?r (mark 2 3))
)
(<= (nextt (box 1 2))
    (oneLeft 1 2 (mark 4 1))
    (does ?r (mark 4 1))
)
(<= (nextt (box 1 2))
    (oneLeft 1 2 (mark 3 2))
    (does ?r (mark 3 2))
)
(<= (nextt (box 1 2))
    (oneLeft 1 2 (mark 4 3))
    (does ?r (mark 4 3))
)
(<= (nextt (box 1 2))
    (oneLeft 1 2 (mark 5 2))
    (does ?r (mark 5 2))
)
(<= (nextt (box 2 1))
    (oneLeft 2 1 (mark 2 3))
    (does ?r (mark 2 3))
)
(<= (nextt (box 2 1))
    (oneLeft 2 1 (mark 1 4))
    (does ?r (mark 1 4))
)
(<= (nextt (box 2 1))
    (oneLeft 2 1 (mark 2 5))
    (does ?r (mark 2 5))
)
(<= (nextt (box 2 1))
    (oneLeft 2 1 (mark 3 4))
    (does ?r (mark 3 4))
)
(<= (nextt (box 2 2))
    (oneLeft 2 2 (mark 4 3))
    (does ?r (mark 4 3))
)
(<= (nextt (box 2 2))
    (oneLeft 2 2 (mark 3 4))
    (does ?r (mark 3 4))
)
(<= (nextt (box 2 2))
    (oneLeft 2 2 (mark 4 5))
    (does ?r (mark 4 5))
)
(<= (nextt (box 2 2))
    (oneLeft 2 2 (mark 5 4))
    (does ?r (mark 5 4))
)


;;; Eine Box wird existieren, wenn sie entweder schon da ist,
;;; oder nur noch ein Strich fehlt, welcher dann auch gesetzt wird
(<= (next (box ?x ?y))
    (true (box ?x ?y))
)
	
(<= (next (box 1 1))
    (oneLeft 1 1 (mark 2 1))
    (does ?r (mark 2 1))
)
(<= (next (box 1 1))
    (oneLeft 1 1 (mark 1 2))
    (does ?r (mark 1 2))
)
(<= (next (box 1 1))
    (oneLeft 1 1 (mark 3 2))
    (does ?r (mark 3 2))
)
(<= (next (box 1 1))
    (oneLeft 1 1 (mark 2 3))
    (does ?r (mark 2 3))
)
(<= (oneLeft 1 1 (mark 2 1))
    (true (cell 2 1 b))
    (true (cell 1 2 f))
    (true (cell 3 2 f))
    (true (cell 2 3 f))
)
(<= (oneLeft 1 1 (mark 1 2))
    (true (cell 2 1 f))
    (true (cell 1 2 b))
    (true (cell 3 2 f))
    (true (cell 2 3 f))
)
(<= (oneLeft 1 1 (mark 3 2))
    (true (cell 2 1 f))
    (true (cell 1 2 f))
    (true (cell 3 2 b))
    (true (cell 2 3 f))
)
(<= (oneLeft 1 1 (mark 2 3))
    (true (cell 2 1 f))
    (true (cell 1 2 f))
    (true (cell 3 2 f))
    (true (cell 2 3 b))
)
	
(<= (next (box 1 2))
    (oneLeft 1 2 (mark 4 1))
    (does ?r (mark 4 1))
)
(<= (next (box 1 2))
    (oneLeft 1 2 (mark 3 2))
    (does ?r (mark 3 2))
)
(<= (next (box 1 2))
    (oneLeft 1 2 (mark 4 3))
    (does ?r (mark 4 3))
)
(<= (next (box 1 2))
    (oneLeft 1 2 (mark 5 2))
    (does ?r (mark 5 2))
)
(<= (oneLeft 1 2 (mark 4 1))
    (true (cell 4 1 b))
    (true (cell 3 2 f))
    (true (cell 4 3 f))
    (true (cell 5 2 f))
)
(<= (oneLeft 1 2 (mark 3 2))
    (true (cell 4 1 f))
    (true (cell 3 2 b))
    (true (cell 4 3 f))
    (true (cell 5 2 f))
)
(<= (oneLeft 1 2 (mark 4 3))
    (true (cell 4 1 f))
    (true (cell 3 2 f))
    (true (cell 4 3 b))
    (true (cell 5 2 f))
)
(<= (oneLeft 1 2 (mark 5 2))
    (true (cell 4 1 f))
    (true (cell 3 2 f))
    (true (cell 4 3 f))
    (true (cell 5 2 b))
)
	
(<= (next (box 2 1))
    (oneLeft 2 1 (mark 2 3))
    (does ?r (mark 2 3))
)
(<= (next (box 2 1))
    (oneLeft 2 1 (mark 1 4))
    (does ?r (mark 1 4))
)
(<= (next (box 2 1))
    (oneLeft 2 1 (mark 2 5))
    (does ?r (mark 2 5))
)
(<= (next (box 2 1))
    (oneLeft 2 1 (mark 3 4))
    (does ?r (mark 3 4))
)
(<= (oneLeft 2 1 (mark 2 3))
    (true (cell 2 3 b))
    (true (cell 1 4 f))
    (true (cell 2 5 f))
    (true (cell 3 4 f))
)
(<= (oneLeft 2 1 (mark 1 4))
    (true (cell 2 3 f))
    (true (cell 1 4 b))
    (true (cell 2 5 f))
    (true (cell 3 4 f))
)
(<= (oneLeft 2 1 (mark 2 5))
    (true (cell 2 3 f))
    (true (cell 1 4 f))
    (true (cell 2 5 b))
    (true (cell 3 4 f))
)
(<= (oneLeft 2 1 (mark 3 4))
    (true (cell 2 3 f))
    (true (cell 1 4 f))
    (true (cell 2 5 f))
    (true (cell 3 4 b))
)
	
(<= (next (box 2 2))
    (oneLeft 2 2 (mark 4 3))
    (does ?r (mark 4 3))
)
(<= (next (box 2 2))
    (oneLeft 2 2 (mark 3 4))
    (does ?r (mark 3 4))
)
(<= (next (box 2 2))
    (oneLeft 2 2 (mark 4 5))
    (does ?r (mark 4 5))
)
(<= (next (box 2 2))
    (oneLeft 2 2 (mark 5 4))
    (does ?r (mark 5 4))
)
(<= (oneLeft 2 2 (mark 4 3))
    (true (cell 4 3 b))
    (true (cell 3 4 f))
    (true (cell 4 5 f))
    (true (cell 5 4 f))
)
(<= (oneLeft 2 2 (mark 3 4))
    (true (cell 4 3 f))
    (true (cell 3 4 b))
    (true (cell 4 5 f))
    (true (cell 5 4 f))
)
(<= (oneLeft 2 2 (mark 4 5))
    (true (cell 4 3 f))
    (true (cell 3 4 f))
    (true (cell 4 5 b))
    (true (cell 5 4 f))
)
(<= (oneLeft 2 2 (mark 5 4))
    (true (cell 4 3 f))
    (true (cell 3 4 f))
    (true (cell 4 5 f))
    (true (cell 5 4 b))
)
	
;;; Die Boxen bestehen aus je 4 Strichen
(<= (box 1 1)
    (true (cell 2 1 f))
    (true (cell 1 2 f))
    (true (cell 3 2 f))
    (true (cell 2 3 f))
)
(<= (box 1 2)
    (true (cell 4 1 f))
    (true (cell 3 2 f))
    (true (cell 4 3 f))
    (true (cell 5 2 f))
)
(<= (box 2 1)
    (true (cell 2 3 f))
    (true (cell 1 4 f))
    (true (cell 2 5 f))
    (true (cell 3 4 f))
)
(<= (box 2 2)
    (true (cell 4 3 f))
    (true (cell 3 4 f))
    (true (cell 4 5 f))
    (true (cell 5 4 f))
)

;;; Wer wird den naechsten Zug machen?
;;; Wer gerade einen Punkt bekam, darf nochmal ziehen
(<= (next (control misterx))
    (true (control mistery))
    (not  (justBoxed mistery))
)

(<= (next (control mistery))
    (true (control misterx))
    (not  (justBoxed misterx))
)
	
(<= (next (control ?r))
    (justBoxed ?r)
)
	
;;; Nach 12 Runden ist immer Schluss
(<= (next (round 1))
    (true (round 0))
)
(<= (next (round 2))
    (true (round 1))
)
(<= (next (round 3))
    (true (round 2))
)
(<= (next (round 4))
    (true (round 3))
)
(<= (next (round 5))
    (true (round 4))
)
(<= (next (round 6))
    (true (round 5))
)
(<= (next (round 7))
    (true (round 6))
)
(<= (next (round 8))
    (true (round 7))
)
(<= (next (round 9))
    (true (round 8))
)
(<= (next (round 10))
    (true (round 9))
)
(<= (next (round 11))
    (true (round 10))
)
(<= (next (round 12))
    (true (round 11))
)

;;;;;;;;; Legal Moves ;;;;;

(<= (legal ?r (mark ?x ?y))
    (true (cell ?x ?y b))
    (true (control ?r))
)
	
(<= (legal misterx noop)
    (true (control mistery))
)
	
(<= (legal mistery noop)
    (true (control misterx))
)

;;;;;;;;; Goals ;;;;;;;;;;;

(<= (goal misterx 100)
    (true (points misterx 4))
)
(<= (goal misterx 75)
    (true (points misterx 3))
)
(<= (goal misterx 50)
    (true (points misterx 2))
)
(<= (goal misterx 25)
    (true (points misterx 1))
)
(<= (goal misterx 0)
    (true (points misterx 0))
)
(<= (goal mistery 100)
    (true (points mistery 4))
)
(<= (goal mistery 75)
    (true (points mistery 3))
)
(<= (goal mistery 50)
    (true (points mistery 2))
)
(<= (goal mistery 25)
    (true (points mistery 1))
)
(<= (goal mistery 0)
    (true (points mistery 0))
)

;;;;;;;; Terminal ;;;;;;;;;

(<= terminal
    (true (round 12))
)
	
;;;;;;;;;;;;;;;;;;;;;;;;;;;