/* 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. */
sig Village {
   truthtellers: set Anouki,
   liars: set Anouki
} {
   no truthtellers & liars
   Anouki = truthtellers + liars
}

fact truthiness {
   all v:Village, a : v.truthtellers {
      all a' : a.supports | a' in v.truthtellers
      all a': a.denies | a' not in v.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 {
   all v: Village {#v.liars = 1}
}

pred twoLiars {
   all v:Village {#v.liars = 2}
}

pred multipleSolution {
   some v, v' : Village | v.liars != v'.liars
}


/* Original puzzle */
run { hearsay and oneLiar} for 6


/* What if there are two liars?  What does that look like? */
run { hearsay and twoLiars} for 6


/* If we wanted to generate a puzzle with two liars, but a unique solution,
   what would that look like? */
pred noSelfRecrimination {
    all a: Anouki | a not in a.denies
}

pred simpleRelations {
    all a: Anouki | { #a.supports <= 2 and #a.denies <= 2 }
}

check {
  (#Village = 2 and (oneLiar or twoLiars) and noSelfRecrimination and simpleRelations)
    implies multipleSolution
} for 6