You are not logged in. login register
Game othello-cornercontrol
name othello-cornercontrol
creator admin
number of roles 2
stylesheet othello/othello.xsl
GDL v1
enabled
matches show matches
statistics show game statistics
description

Game Description

; game has bugs (in clear/5) and JavaProver computes wrong states
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;role
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(role black)
(role white)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;initialize
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(init (cell c1 c1 green))
(init (cell c1 c2 green))
(init (cell c1 c3 green))
(init (cell c1 c4 green))
(init (cell c1 c5 green))
(init (cell c1 c6 green))
(init (cell c1 c7 green))
(init (cell c1 c8 green))

(init (cell c2 c1 green))
(init (cell c2 c2 green))
(init (cell c2 c3 green))
(init (cell c2 c4 green))
(init (cell c2 c5 green))
(init (cell c2 c6 green))
(init (cell c2 c7 green))
(init (cell c2 c8 green))

(init (cell c3 c1 green))
(init (cell c3 c2 green))
(init (cell c3 c3 green))
(init (cell c3 c4 green))
(init (cell c3 c5 green))
(init (cell c3 c6 green))
(init (cell c3 c7 green))
(init (cell c3 c8 green))

(init (cell c4 c1 green))
(init (cell c4 c2 green))
(init (cell c4 c3 green))
(init (cell c4 c4 white))
(init (cell c4 c5 black))
(init (cell c4 c6 green))
(init (cell c4 c7 green))
(init (cell c4 c8 green))

(init (cell c5 c1 green))
(init (cell c5 c2 green))
(init (cell c5 c3 green))
(init (cell c5 c4 black))
(init (cell c5 c5 white))
(init (cell c5 c6 green))
(init (cell c5 c7 green))
(init (cell c5 c8 green))

(init (cell c6 c1 green))
(init (cell c6 c2 green))
(init (cell c6 c3 green))
(init (cell c6 c4 green))
(init (cell c6 c5 green))
(init (cell c6 c6 green))
(init (cell c6 c7 green))
(init (cell c6 c8 green))

(init (cell c7 c1 green))
(init (cell c7 c2 green))
(init (cell c7 c3 green))
(init (cell c7 c4 green))
(init (cell c7 c5 green))
(init (cell c7 c6 green))
(init (cell c7 c7 green))
(init (cell c7 c8 green))

(init (cell c8 c1 green))
(init (cell c8 c2 green))
(init (cell c8 c3 green))
(init (cell c8 c4 green))
(init (cell c8 c5 green))
(init (cell c8 c6 green))
(init (cell c8 c7 green))
(init (cell c8 c8 green))

(init (control white))

(init (fringe c3 c3))
(init (fringe c3 c4))
(init (fringe c3 c5))
(init (fringe c3 c6))
(init (fringe c4 c3))
(init (fringe c4 c6))
(init (fringe c5 c3))
(init (fringe c5 c6))
(init (fringe c6 c3))
(init (fringe c6 c4))
(init (fringe c6 c5))
(init (fringe c6 c6))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;define a relationship Greater
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(succ c0 c1)
(succ c1 c2)
(succ c2 c3)
(succ c3 c4)
(succ c4 c5)
(succ c5 c6)
(succ c6 c7)
(succ c7 c8)
(succ c8 c9)
(succ c9 c10)
(succ c10 c11)
(succ c11 c12)
(succ c12 c13)
(succ c13 c14)
(succ c14 c15)
(succ c15 c16)
(succ c16 c17)
(succ c17 c18)
(succ c18 c19)
(succ c19 c20)
 (succ c20 c21)
  (succ c21 c22)
  (succ c22 c23)
  (succ c23 c24)
  (succ c24 c25)
  (succ c25 c26)
  (succ c26 c27)
  (succ c27 c28)
  (succ c28 c29)
  (succ c29 c30)
  (succ c30 c31)
  (succ c31 c32)
  (succ c32 c33)
  (succ c33 c34)
  (succ c34 c35)
  (succ c35 c36)
  (succ c36 c37)
  (succ c37 c38)
  (succ c38 c39)
  (succ c39 c40)
  (succ c40 c41)
  (succ c41 c42)
  (succ c42 c43)
  (succ c43 c44)
  (succ c44 c45)
  (succ c45 c46)
  (succ c46 c47)
  (succ c47 c48)
  (succ c48 c49)
  (succ c49 c50)
  (succ c50 c51)
  (succ c51 c52)
  (succ c52 c53)
  (succ c53 c54)
  (succ c54 c55)
  (succ c55 c56)
  (succ c56 c57)
  (succ c57 c58)
  (succ c58 c59)
  (succ c59 c60)
  (succ c60 c61)
  (succ c61 c62)
  (succ c62 c63)
  (succ c63 c64)

(<= (greater ?a ?b)
    (succ ?b ?a))
(<= (greater ?a ?b)
    (distinct ?a ?b)
    (succ ?c ?a)
    (greater ?c ?b))
    
(coordinate c1)
(coordinate c2)
(coordinate c3)
(coordinate c4)
(coordinate c5)
(coordinate c6)
(coordinate c7)
(coordinate c8)

(piece white)
(piece black)

(opponent white black)
(opponent black white)

(direction n)
(direction s)
(direction e)
(direction w)
(direction nw)
(direction ne)
(direction sw)
(direction se)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;Define flip
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(opp n s)
(opp s n)
(opp e w)
(opp w e)
(opp nw se)
(opp se nw)
(opp ne sw)
(opp sw ne)

(<= (adj nw ?a ?b ?c ?d)
    (succ ?c ?a)
    (succ ?d ?b))

(<= (adj sw ?a ?b ?c ?d)
    (succ ?a ?c)
    (succ ?d ?b))

(<= (adj ne ?a ?b ?c ?d)
    (succ ?c ?a)
    (succ ?b ?d))

(<= (adj se ?a ?b ?c ?d)
    (succ ?a ?c)
    (succ ?b ?d))

(<= (adj w ?a ?b ?a ?d)
    (succ ?d ?b)
    (coordinate ?a))

(<= (adj e ?a ?b ?a ?d)
    (succ ?b ?d)
    (coordinate ?a))

(<= (adj n ?a ?b ?c ?b)
    (succ ?c ?a)
    (coordinate ?b))

(<= (adj s ?a ?b ?c ?b)
    (succ ?a ?c)
    (coordinate ?b))

;; True if there is a line of ?c1 pieces from ?i ?j on a line 
;; ending just before ?m ?n pointing in ?dir

(<= (onalinep ?i ?j ?c1 ?m ?n ?c2 ?dir)
    (true (cell ?i ?j ?c1))
    (adj ?dir ?i ?j ?m ?n)
    (piece ?c2))

(<= (onalinep ?i ?j ?c1 ?m ?n ?c2 ?dir)
    (true (cell ?i ?j ?c1))
    (adj ?dir ?i ?j ?x ?y)
    (onalinep ?x ?y ?c1 ?m ?n ?c2 ?dir))

;; True if there is a line of ?c1 pieces from ?i ?j on a line 
;; ending just before ?m ?n pointing in ?dir, where ?m ?n is
;; a ?c2 piece

(<= (onaline ?i ?j ?c1 ?m ?n ?c2 ?dir)
    (true (cell ?i ?j ?c1))
    (true (cell ?m ?n ?c2))
    (adj ?dir ?i ?j ?m ?n))

(<= (onaline ?i ?j ?c1 ?m ?n ?c2 ?dir)
    (true (cell ?i ?j ?c1))
    (adj ?dir ?i ?j ?x ?y)
    (onaline ?x ?y ?c1 ?m ?n ?c2 ?dir))
    
;; A black piece at ?i ?j gets flipped by white placement at ?m ?n 

(<= (flip ?i ?j white ?m ?n)
    (onalinep ?i ?j black ?m ?n white ?dir)
    (opp ?dir ?odir)
    (onaline ?i ?j black ?x ?y white ?odir))

;; A white piece at ?i ?j gets flipped by black placement at ?m ?n 

(<= (flip ?i ?j black ?m ?n)
    (onalinep ?i ?j white ?m ?n black ?dir)
    (opp ?dir ?odir)
    (onaline ?i ?j white ?x ?y black ?odir))

(<= (onanylinep ?i ?j ?color ?m ?n ?othercolor)
    (onalinep ?i ?j ?color ?m ?n ?othercolor ?dir))

(<= (clear ?i ?j black ?m ?n)
    (not (onanylinep ?i ?j white ?m ?n black))
    (coordinate ?i)
    (coordinate ?j)
    (coordinate ?m)
    (coordinate ?n))

(<= (clear ?i ?j white ?m ?n)
    (not (onanylinep ?i ?j black ?m ?n white))
    (coordinate ?i)
    (coordinate ?j)
    (coordinate ?m)
    (coordinate ?n))

(<= (clear ?i ?j black ?m ?n)
    (onalinep ?i ?j white ?m ?n black ?dir)
    (opp ?dir ?odir)
    (not (onaline ?i ?j white ?x ?y black ?odir))
    (coordinate ?x)
    (coordinate ?y))

(<= (clear ?i ?j white ?m ?n)
    (onalinep ?i ?j black ?m ?n white ?dir)
    (opp ?dir ?odir)
    (not (onaline ?i ?j black ?x ?y white ?odir))
    (coordinate ?x)
    (coordinate ?y))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;Update rules
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (next (cell ?m ?n white))
    (does white (place ?m ?n))
    (true (cell ?m ?n green)))

(<= (next (cell ?m ?n black))
    (does black (place ?m ?n))
    (true (cell ?m ?n green)))

(<= (next (cell ?m ?n white))
    (true (cell ?m ?n black))
    (does white (place ?i ?j))
    (flip ?m ?n white ?i ?j))

(<= (next (cell ?m ?n black))
    (true (cell ?m ?n white))
    (does black (place ?i ?j))
    (flip ?m ?n black ?i ?j))

;; a piece stays the same color if that player moved--can't flip your own

(<= (next (cell ?m ?n black))
    (true (cell ?m ?n black))
    (does black (place ?x ?y)))

(<= (next (cell ?m ?n white))
    (true (cell ?m ?n white))
    (does white (place ?x ?y)))

(<= (next (cell ?m ?n black))
    (true (cell ?m ?n black))
    (does white (place ?i ?j))
    (clear ?m ?n white ?i ?j))

(<= (next (cell ?m ?n white))
    (true (cell ?m ?n white))
    (does black (place ?i ?j))
    (clear ?m ?n black ?i ?j))

(<= (next (cell ?m ?n green))
    (does ?w (place ?j ?k))
    (true (cell ?m ?n green))
    (or (distinct ?m ?j) (distinct ?n ?k)))

;; A cell is in the fringe if it is was in the fringe and 
;; did not get placed in.

(<= (next (fringe ?x ?y))
    (true (fringe ?x ?y))
    (does ?player (place ?i ?j))
    (or (distinct ?x ?i) (distinct ?y ?j)))

(<= (next (fringe ?x ?y))
    (true (fringe ?x ?y))
    (does white noop)
    (does black noop))

;; A cell becomes in the fringe if it is a green cell adjacent 
;; to whereever a player placed.

(<= (next (fringe ?x ?y))
    (does ?player (place ?i ?j))
    (adj ?dir ?i ?j ?x ?y)
    (true (cell ?x ?y green)))

;;; Everything stays the same if the player with control noops
(<= (next (cell ?m ?n ?color))
    (true (cell ?m ?n ?color))
    (true (control ?p))
    (does ?p noop))

(<= (next (control white))
    (true (control black)))

(<= (next (control black))
    (true (control white)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; White can place a square if
;;;; It will flip some pieces
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (legal white (place ?m ?n))
    (true (control white))
    (true (fringe ?m ?n))
    (true (cell ?m ?n green))
    (flip ?i ?j white ?m ?n))

(<= (legal black (place ?m ?n))
    (true (control black))
    (true (fringe ?m ?n))
    (true (cell ?m ?n green))
    (flip ?i ?j black ?m ?n))

(<= (legal white noop)
    (true (control black))
    (true (cell ?x ?y green)))

(<= (legal black noop)
    (true (control white))
    (true (cell ?x ?y green)))

(<= (legal ?p noop)
    (true (control ?p))
    (not (flippable ?p)))

(<= (flippable ?p)
    (true (fringe ?x ?y))
    (true (cell ?x ?y green))
    (flip ?i ?j ?p ?x ?y))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; define the goal state
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (goal white ?value)
    (corner_control white ?value))

(<= (goal black ?value)
    (corner_control black ?value))
    
(<= (corner_control ?color ?value)
    (cornercheck c1 c1 ?color ?ul)
    (cornercheck c1 c8 ?color ?ur)
    (addition ?ur ?ul ?s1)
    (cornercheck c8 c1 ?color ?lr)
    (addition ?lr ?s1 ?s2)
    (cornercheck c8 c8 ?color ?ll)
    (addition ?ll ?s2 ?value))

(<= (cornercheck ?c ?r ?color 25)
    (true (cell ?c ?r ?color)))

(<= (cornercheck ?c ?r ?color 0)
    (true (cell ?c ?r ?x))
    (piece ?color)
    (distinct ?x ?color))

(addition 0 0 0)
(addition 25 0 25)
(addition 0 25 25)
(addition 25 25 50)
(addition 50 25 75)
(addition 25 50 75)
(addition 50 50 100)
(addition 0 50 50)
(addition 50 0 50)
(addition 25 75 100)
(addition 75 25 100)
(addition 0 75 75)
(addition 75 0 100)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; define the terminal state
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(<= terminal
    (true (cell c1 c1 ?x1))
    (distinct ?x1 green)
    (true (cell c1 c1 ?x2))
    (distinct ?x2 green)
    (true (cell c1 c1 ?x3))
    (distinct ?x3 green)
    (true (cell c1 c1 ?x4))
    (distinct ?x4 green))
(<= open
    (true (cell ?m ?n green)))
(<= terminal
    (not open))
(<= terminal
    (not (flippable white))
    (not (flippable black)))

sees_XML(...) rules

(<= (sees_xml random ?t) (true ?t))
(<= (sees_xml ?p ?t) (role ?p) (distinct ?p random) (true ?t))