http://www23.atwiki.jp/alloy/pages/21.html

booking1.als

sig System {
  slist: some SSeat,
  alist: some ASeat,
  reserved: set slist + alist
}
abstract sig Seat {}
sig ASeat extends Seat {}
sig SSeat extends Seat {}
enum SeatType { A, S }

pred reserve_seat(t: SeatType, rs: Seat, s, s': System) {
  s'.slist = s.slist
  s'.alist = s.alist
  !(rs in s.reserved)
  s'.reserved = s.reserved + rs
  t = A => rs in s.alist
  t = S => rs in s.slist
}
run reserve_seat for 3 but exactly 2 System

pred cancel_seat(cs: Seat, s, s': System) {
  cs in s.reserved
  s'.reserved = s.reserved - cs
  s'.alist = s.alist
  s'.slist = s.slist
}
run cancel_seat for 3 but exactly 2 System