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
	key.t: Room lone -> Key
	}

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
		}
	}

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

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
			}
	}

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

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

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