You are not logged in. login register
Game othello
name othello
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 white)
(role black)

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

(init (cell 1 1 green))
(init (cell 1 2 green))
(init (cell 1 3 green))
(init (cell 1 4 green))
(init (cell 1 5 green))
(init (cell 1 6 green))
(init (cell 1 7 green))
(init (cell 1 8 green))

(init (cell 2 1 green))
(init (cell 2 2 green))
(init (cell 2 3 green))
(init (cell 2 4 green))
(init (cell 2 5 green))
(init (cell 2 6 green))
(init (cell 2 7 green))
(init (cell 2 8 green))

(init (cell 3 1 green))
(init (cell 3 2 green))
(init (cell 3 3 green))
(init (cell 3 4 green))
(init (cell 3 5 green))
(init (cell 3 6 green))
(init (cell 3 7 green))
(init (cell 3 8 green))

(init (cell 4 1 green))
(init (cell 4 2 green))
(init (cell 4 3 green))
(init (cell 4 4 white))
(init (cell 4 5 black))
(init (cell 4 6 green))
(init (cell 4 7 green))
(init (cell 4 8 green))

(init (cell 5 1 green))
(init (cell 5 2 green))
(init (cell 5 3 green))
(init (cell 5 4 black))
(init (cell 5 5 white))
(init (cell 5 6 green))
(init (cell 5 7 green))
(init (cell 5 8 green))

(init (cell 6 1 green))
(init (cell 6 2 green))
(init (cell 6 3 green))
(init (cell 6 4 green))
(init (cell 6 5 green))
(init (cell 6 6 green))
(init (cell 6 7 green))
(init (cell 6 8 green))

(init (cell 7 1 green))
(init (cell 7 2 green))
(init (cell 7 3 green))
(init (cell 7 4 green))
(init (cell 7 5 green))
(init (cell 7 6 green))
(init (cell 7 7 green))
(init (cell 7 8 green))

(init (cell 8 1 green))
(init (cell 8 2 green))
(init (cell 8 3 green))
(init (cell 8 4 green))
(init (cell 8 5 green))
(init (cell 8 6 green))
(init (cell 8 7 green))
(init (cell 8 8 green))

(init (control white))

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

(succ 0 1)
(succ 1 2)
(succ 2 3)
(succ 3 4)
(succ 4 5)
(succ 5 6)
(succ 6 7)
(succ 7 8)
(succ 8 9)
(succ 9 10)
(succ 10 11)
(succ 11 12)
(succ 12 13)
(succ 13 14)
(succ 14 15)
(succ 15 16)
(succ 16 17)
(succ 17 18)
(succ 18 19)
(succ 19 20)
 (succ 20 21)
  (succ 21 22)
  (succ 22 23)
  (succ 23 24)
  (succ 24 25)
  (succ 25 26)
  (succ 26 27)
  (succ 27 28)
  (succ 28 29)
  (succ 29 30)
  (succ 30 31)
  (succ 31 32)
  (succ 32 33)
  (succ 33 34)
  (succ 34 35)
  (succ 35 36)
  (succ 36 37)
  (succ 37 38)
  (succ 38 39)
  (succ 39 40)
  (succ 40 41)
  (succ 41 42)
  (succ 42 43)
  (succ 43 44)
  (succ 44 45)
  (succ 45 46)
  (succ 46 47)
  (succ 47 48)
  (succ 48 49)
  (succ 49 50)
  (succ 50 51)
  (succ 51 52)
  (succ 52 53)
  (succ 53 54)
  (succ 54 55)
  (succ 55 56)
  (succ 56 57)
  (succ 57 58)
  (succ 58 59)
  (succ 59 60)
  (succ 60 61)
  (succ 61 62)
  (succ 62 63)
  (succ 63 64)

(<= (greater ?a ?b)
    (succ ?b ?a))
(<= (greater ?a ?b)
    (distinct ?a ?b)
    (succ ?c ?a)
    (greater ?c ?b))
    
(coordinate 1)
(coordinate 2)
(coordinate 3)
(coordinate 4)
(coordinate 5)
(coordinate 6)
(coordinate 7)
(coordinate 8)

(piece white)
(piece black)

(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))


(<= (clear ?i ?j black ?m ?n)
    (not (onalinep ?i ?j white ?m ?n black ?dir))
    (coordinate ?i)
    (coordinate ?j)
    (coordinate ?m)
    (coordinate ?n)
    (direction ?dir))

(<= (clear ?i ?j white ?m ?n)
    (not (onalinep ?i ?j black ?m ?n white ?dir))
    (coordinate ?i)
    (coordinate ?j)
    (coordinate ?m)
    (coordinate ?n)
    (direction ?dir))

(<= (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)))

;;; 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 (cell ?m ?n green))
    (flip ?i ?j white ?m ?n))

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

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

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

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

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

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; count pieces
;;;; if the game is in terminal state
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= (count ?row ?column ?whitenum ?blacknum)
    (distinct ?column 8)
    (true (cell ?row ?column white))
    (succ ?column ?nc)
    (count ?row ?nc ?rest ?blacknum)
    (succ ?rest ?whitenum))

(<= (count ?row ?column ?whitenum ?blacknum)
    (distinct ?column 8)
    (true (cell ?row ?column black))
    (succ ?column ?nc)
    (count ?row ?nc ?whitenum ?rest)
    (succ ?rest ?blacknum))

(<= (count ?row ?column ?whitenum ?blacknum)
    (distinct ?column 8)
    (true (cell ?row ?column green))
    (succ ?column ?nc)
    (count ?row ?nc ?whitenum ?blacknum))

(<= (count ?row 8 ?whitenum ?blacknum)
    (distinct ?row 8)
    (true (cell ?row 8 white))
    (succ ?row ?nr)
    (count ?nr 1 ?rest ?blacknum)
    (succ ?rest ?whitenum))

(<= (count ?row 8 ?whitenum ?blacknum)
    (distinct ?row 8)
    (true (cell ?row 8 black))
    (succ ?row ?nr)
    (count ?nr 1 ?whitenum ?rest)
    (succ ?rest ?blacknum))

(<= (count ?row 8 ?whitenum ?blacknum)
    (distinct ?row 8)
    (true (cell ?row 8 green))
    (succ ?row ?nr)
    (count ?nr 1 ?whitenum ?blacknum))

(<= (count 8 8 1 0)
    (true (cell 8 8 white)))

(<= (count 8 8 0 1)
    (true (cell 8 8 black)))

(<= (count 8 8 0 0)
    (true (cell 8 8 green)))

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

(<= (goal white 100)
    (count 1 1 ?w ?b)
    (greater ?w ?b))

(<= (goal black 100)
    (count 1 1 ?w ?b)
    (greater ?b ?w))

(<= (goal ?role 50)
    (count 1 1 ?x ?x)
    (role ?role))

(<= (goal black 0)
    (count 1 1 ?w ?b)
    (greater ?w ?b))

(<= (goal white 0)
    (count 1 1 ?w ?b)
    (greater ?b ?w))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; define the terminal state
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(<= 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))