sig Event {}

sig Person {
  , events: set Event
  , likes: set Event
  , hates: set Event
} 

pred valid[p: Person]
{
 no p.likes & p.hates
}

sig NewPerson {
  , person: one Person
}

sig Attendance {
  , event: Event
  , attendee: NewPerson
}

abstract sig Review {
  , event: Event
  , reviewer: NewPerson
}

sig Likes, Hates extends Review {}

pred same_events[p: Person, np: NewPerson] {
  p.events = np.~attendee.event
}

pred same_reviews[p: Person, np: NewPerson] {
  p.likes = (np.~reviewer & Likes).event
  p.hates = (np.~reviewer & Hates).event
}

pred equivalent[p: Person, np: NewPerson] {
  p = np.person
  same_events[p, np]
  same_reviews[p, np]
}

pred valid[np: NewPerson] {
  --- 1    
  all r, r': np.~reviewer |
    r in Likes and r' in Hates => r.event != r'.event

  --- 2
  all e: Event {
    -- at most one review for this
    lone r: np.~reviewer |
      r.event = e

    -- at most one attendance
    lone a: np.~attendee |
      a.event = e
  }
}

pred migration[p: Person, np: NewPerson] {
  p = np.person

  -- only generate the records needed
  #p.events = #np.~attendee
  #p.likes = #np.~reviewer & Likes
  #p.hates = #np.~reviewer & Hates

  -- migrate events
  all e: p.events |
    one a: Attendance {
      a.event = e
      a.attendee = np
    }

  -- migrate likes
  all l: p.likes |
    one r: Likes {
      r.event = l
      r.reviewer = np
    }

  -- migrate hates
  all h: p.hates |
    one r: Hates {
      r.event = h
      r.reviewer = np
    }

}

assert migration_preserves_equivalence {
  all p: Person, np: NewPerson |
    migration[p, np] => equivalent[p, np]
}

assert equivalence_implies_migration {
  all p: Person, np: NewPerson |
    equivalent[p, np] and valid[np] => migration[p, np]
}

assert equivalence_preserves_validity {
  all p: Person, np: NewPerson |
    equivalent[p, np] => (valid[p] iff valid[np])
}

assert equivalence_does_not_decrease_validity {
  all p: Person, np: NewPerson |
    equivalent[p, np] and not valid[p] => not valid[np]
}

assert migrations_stay_valid {
  all p: Person, np: NewPerson |
    migration[p, np] and valid[p] => valid[np]
}

pred all_valid_at_start {
  all p: Person | valid[p]
}

run all_valid_at_start

check migrations_stay_valid
check equivalence_does_not_decrease_validity
check equivalence_implies_migration
check migration_preserves_equivalence
check equivalence_preserves_validity

example: run {
  one Person
  one NewPerson
  equivalent[Person, NewPerson]
}