module examples/hotelEvents
open util/ordering[Time] as to
open util/ordering[Key] as ko

sig Key, Time {}

sig Room {
	keys: set Key,
	currentKey: keys one -> Time
	}
fact {
	Room <: keys : Room lone -> Key
	}

one sig FrontDesk {
	lastKey: (Room -> lone Key) -> Time,
	occupant: (Room -> Guest) -> Time
	}

sig Guest {
	keys: Key -> Time
	}

fun nextKey (k: Key, ks: set Key): set Key {
	ko/min (ko/nexts (k) & ks)
	}

pred init (t: Time) {
	all r: Room | FrontDesk.lastKey.t [r] = r.currentKey.t
	no FrontDesk.occupant.t
	no Guest.keys.t
	}

abstract sig Event {
	pre, post: Time,
	guest: Guest
	}

abstract sig RoomKeyEvent extends Event {
	room: Room,
	key: Key
	}

sig Entry extends RoomKeyEvent { } {
	key in guest.keys.pre
	let ck = room.currentKey |
		(key = ck.pre and ck.post = ck.pre) or 
		(key = nextKey(ck.pre, room.keys) and ck.post = key)
	}

sig Checkin extends RoomKeyEvent { } {
	keys.post = keys.pre + guest -> key
	let occ = FrontDesk.occupant {
		no occ.pre [room]
		occ.post = occ.pre + room -> guest
		}
	let lk = FrontDesk.lastKey {
		lk.post = lk.pre ++ room -> key
		key = nextKey (lk.pre [room], room.keys)
		}
	}

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

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'
			currentKey.t = currentKey.t' or e in Entry
			occupant.t = occupant.t' or e in Checkin + Checkout
			(lastKey.t = lastKey.t' and keys.t = keys.t') or e in Checkin
			}
	}

assert NoBadEntry {
	all e: Entry | let occs = FrontDesk.occupant.(e.pre) [e.room] | 
		some occs => e.guest in occs
	}
-- 6 seconds
check NoBadEntry for 3 but 2 Room, 2 Guest, 5 Time, 4 Event
check NoBadEntry for 3 but 2 Room, 2 Guest, 6 Time, 5 Event

check NoBadEntry for 5 but 3 Room, 3 Guest, 9 Time, 8 Event
-- analyzed in 25 seconds; standard version of this model took 1:52

/*
fact NoIntervening {
	all c: Checkin |
		c.post = to/last ()
		or some e: Entry | e.pre = c.post and e.room = c.room and e.guest = c.guest
	}
*/