Sunday, November 25, 2007

zelda

I held my sword in front, and approached the village cautiously. I would have to slaughter the terrible Yook monster disguised in one of the hapless villagers's homes. I pushed the doors open, ready to hack and slash. To my shock, all of the villagers looked exactly the same!

And each had something to say about the other Anouki:

* FoFo said that Gumo was honest.
* Kumu said Mazo or Aroo was lying.
* Dobo said Mazo was honest.
* Gumo said Fofo or Aroo was lying.
* Aroo said Kumu was lying.
* Mazo said that he and Dobo were honest.

How dastardly! Only the Yook would lie to me. And I couldn't just kill them all and let God sort them out. I had to think about this. So I did what anyone in this circumstance would do: I pulled out Alloy.


abstract sig Boolean {}
one sig True, False extends Boolean {}

abstract sig Anouki {
truthful: Boolean
}

one sig Fofo, Kumu, Dobo, Gumo, Aroo, Mazo extends Anouki {}

pred whoTellsTruth {
Fofo.truthful = True implies Gumo.truthful=True
Kumu.truthful = True implies ((Mazo.truthful=False) or
(Aroo.truthful=False))
Dobo.truthful = True implies Mazo.truthful=True
Gumo.truthful = True implies ((Fofo.truthful=False) or
(Aroo.truthful=False))
Aroo.truthful = True implies (Kumu.truthful=False)
Mazo.truthful = True implies (Mazo.truthful=True and
Dobo.truthful=True)
}

pred onlyOneIsLying {
one a: Anouki | a.truthful=False
}

run {
whoTellsTruth
onlyOneIsLying
}


Ah ha! But as I was about to raise my gleaming blade against the trembling liar, doubt came to my mind: what if there were two of them out there? Or three, or four? I thought: perhaps I should plan this out more carefully before executing my righteous justice. And maybe I should rewrite the model a little more to make it more general: who knows how many villages of liars I might run across?


/* Anouki can be friendly or antagonistic to other Anouki */
sig Anouki {
supports: set Anouki,
denies: set Anouki
} {
/* and it's nonsensical to be both supportive and antagonistic of
the same Anouki. */
no (supports & denies)
}

/* A village consists of folks who tell the truth, and symmetrically,
those who lie. And we will categorically make every Anouki a
truthteller or a liar. */
one sig Village {
truthtellers: set Anouki,
liars: set Anouki
} {
no truthtellers & liars
Anouki = truthtellers + liars
}

fact truthiness {
all a : Village.truthtellers {
all a' : a.supports | a' in Village.truthtellers
all a': a.denies | a' not in Village.truthtellers
}
}

/* Here's what everyone says about each other */
pred hearsay {
some disj fofo, kumu, dobo, gumo, aroo, mazo : Anouki {
fofo.supports = gumo
fofo.denies = none
kumu.supports = none
kumu.denies = mazo or kumu.denies = aroo
dobo.supports = mazo
dobo.denies = none
gumo.supports = none
gumo.denies = fofo or gumo.denies = aroo
aroo.supports = none
aroo.denies = kumu
mazo.supports = mazo + dobo
mazo.denies = none
fofo + kumu +dobo + gumo + aroo + mazo = Anouki
}
}

pred oneLiar {
hearsay and #Village.liars = 1
}

pred twoLiars {
hearsay and #Village.liars = 2
}

run oneLiar for 6
run twoLiars for 6


Hours passed as I played out different scenarios. By this time, the Yook had already run away, but I had a model I was happy with.