module hotel
open util/ordering [Time]

sig Key, Time {}
sig Card {
	fst, snd: Key
	}
sig Room {
	key: Key one -> Time
	}
one sig Desk {
	prev: (Room -> lone Key) -> Time,
	issued: Key -> Time,
	occ: (Room -> lone Guest) -> Time
	}
sig Guest {
	cards: Card -> Time
	}

pred init (t: Time) {
	Desk.prev.t = key.t
--	no issued.t and no cards.t
	Desk.issued.t = Room.key.t and no cards.t and no occ.t
	}

pred checkin (t, t': Time, r: Room, g: Guest) {
	no r.(Desk.occ.t)
	Desk.occ.t' = Desk.occ.t + r ->g
	some c: Card {
		c.fst = r.(Desk.prev.t)
		c.snd not in Desk.issued.t
		cards.t' = cards.t + g -> c
		Desk.issued.t' = Desk.issued.t + c.snd
		Desk.prev.t' = Desk.prev.t ++ r -> c.snd
		}
	key.t = key.t'
	}

pred checkout (t, t': Time, r: Room, g: Guest) {
	Desk.occ.t' = Desk.occ.t - r ->g
	issued.t = issued.t' and prev.t = prev.t'
	cards.t = cards.t' and key.t = key.t'
	}

pred enter (t, t': Time, r: Room, g: Guest) {
	some c: g.cards.t |
		let k = r.key.t {
			c.snd = k and key.t' = key.t
			or c.fst = k and key.t' = key.t ++ r -> c.snd
			}
	issued.t = issued.t' and prev.t = prev.t' and occ.t = occ.t'
	cards.t = cards.t'
	}

fact Traces {
	init (first())
	all t: Time - last () | some g: Guest, r: Room | let t' = next (t) | 
		checkin (t, t', r, g) or enter (t, t', r, g) or checkout (t, t', r, g)
	}

assert NoIntruder {
	no t: Time, g: Guest, r: Room |
		enter (t, next(t), r, g) and r -> g not in Desk.occ.t
	}
check NoIntruder for 3 but 5 Time, 1 Room, 2 Guest

-- exercise: give guest ability to make new cards from keys she has