module hotel_locking_hw
open util/ordering [Time] as TO
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
   }
}

// sanity checks
pred someCheckin { some Checkin }
run someCheckin for 3 but 2 Time, 1 Event, 6 Key

pred someCheckout { some Checkout }
run someCheckout

pred someEntry { some Entry }
run someEntry

pred someAll { someCheckin and someCheckout and someEntry }
run someAll for 3 but 4 Time, 3 Event, 6 Key


// end of hotel_checking_operations, start of hotel_checking_traces


// At the first clock time, no guests have any keys, no rooms are owned
// by any guests and the FrontDesk and each room agree on what
// key is current 
pred init [ t: Time ] {
   no Guest.keys.t
   no FrontDesk.owns.t
   all r: Room | FrontDesk.current.t [r] = r.current.t
}

run init  // sanity check 

// The ordering of clock ticks induces an execution order on events
fact Traces {
   init [ TO/first ]
   all t: Time - TO/last | let t' = TO/next [t] |
      some e: Event {
         e.pre = t and e.post = t'
         Room <:current.t != Room<:current.t' => e in Entry
         owns.t != owns.t' => e in Checkin + Checkout
         (FrontDesk<:current.t != FrontDesk<:current.t' or keys.t != keys.t')
            => e in Checkin
      }
}

// A guest may enter a room only if the guest owns that room
assert NoBadEntry {
   all e: Entry | let o = FrontDesk.owns.(e.pre) [e.room] |
      some o => e.guest in o
}

// This check produces a counterexample
check NoBadEntry for 5 but 3 Room, 3 Guest, 5 Time, 4 Event

// No event intervenes between a guest checking into a room
// and entering the room 
pred NoIntervening {
   all c: Checkin |
      c.post = TO/last or
      some e: Entry {
         e.pre = c.post
         e.room = c.room
         e.guest = c.guest
      }
}

// A predicate version of NoBadEntry
pred BadEntrySafe [ ] {
   all e: Entry | let o = FrontDesk.owns.(e.pre) [e.room] |
      some o => e.guest in o
}

// Will NoIntervening prevent "bad" entry?
assert GuardedNoBadEntry { NoIntervening => BadEntrySafe }
check GuardedNoBadEntry for 5 but 2 Room, 3 Guest, 5 Time, 4 Event