module hotel_locking_ops_hw
open util/ordering [ Key ] as KO
sig Time { }    // time instants (clock ticks)
sig Key { }     // key combinations (cards not explicitly modeled)

// The front desk maps a room to a current key and to
// a guest checked into the room, if any 
one sig FrontDesk {
   current: (Room -> lone Key) -> Time,  // no current key prior to initialization
   owns: (Room -> Guest) -> Time 
}

// A guest holds a set of keys at a given time
sig Guest { 
  keys: Key -> Time 
}

// A room has a fixed set of keys,  a current key at a given time
sig Room {
  keys: set Key, 
  current: keys one -> Time
}

// No key belongs to more than one room lock
fact DisjointKeySets {
   Room <: keys in Room lone -> Key
}

// Function to generate the successor key
fun nextKey [ k: Key, ks: set Key ] : set Key {
   // smallest key that follows k and belongs to ks
   KO/min [ KO/nexts [k]  &  ks ]
}


// All operations involve a guest, are (immediately) preceded by a clock tick,
// and immediately followed by a clock tick
abstract sig Event {
   pre, post: Time,
   guest: Guest
}

// A RoomKeyEvent additionally involves a given room and a given key
abstract sig RoomKeyEvent extends Event {
   room: Room,
   key: Key
}

sig Entry extends RoomKeyEvent { } {
   // the given key should have been issued to the given guest
   key in guest.keys.pre                    
   let ck = room.current |
      // key must match ck.pre or its successor (among the room's keys)
      (key = ck.pre and ck.post = ck.pre) or        // key matches, no recoding
      (key = nextKey [ ck.pre, room.keys ] and ck.post = key)   // recode key
}

sig Checkin extends RoomKeyEvent { } {
   // update the FrontDesk's keys mapping---Checkin assigns
   // the guest a(nother) key
   keys.post = keys.pre + guest -> key
   let occ = FrontDesk.owns {
      // precondition: no guest owns the room prior to Checkin  
      no occ.pre [room]  
      // postcondition: after Checkin, the given guest owns the given room                              
      occ.post = occ.pre + room -> guest
   }
  let curr = FrontDesk.current {
      // postcondition: the key given to the guest is the "next" one in
      // the order that the FrontDesk and the room are using
      key = nextKey [ curr.pre [room], room.keys ]
      // postcondition: FrontDesk replaces the current key for this room
      // with the new one just generated (it is now current)
      curr.post = curr.pre ++ room -> key
   }
}

sig Checkout extends Event { } {
   let occ = FrontDesk.owns {
      some occ.pre.guest
      occ.post = occ.pre - Room -> guest
   }
}

pred any [] {}
run any