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.