exercise-a.3.4.als

sig Person {
  shaken: set Person,
  partner: Person
}

fact partnerProperties {
  partner = ~partner
  no p: Person | p in p.partner
}

fact shakenProperties {
  shaken = ~shaken
  no p: Person | p in p.shaken
  no p: Person | p.partner in p.shaken
}

one sig Alice, Bob extends Person {}
fact { Alice -> Bob in partner }

fact numShakenPeopleMutuallyDiffer {
  all disj p, p': Person - Alice {
    #p.shaken != #p'.shaken
  }
}

pred show {}

run show for exactly 10 Person

show.png