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

pred checkin (t, t': Time, r: Room, g: Guest) {
	some c: Card {
		c.fst = r.(Desk.prev.t)
		c.snd not in Desk.issued.t
		cards.t' = cards.t + g -> c
--		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 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'
	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)
	}

assert NoIntruder {
	no t1: Time, disj g, g': Guest, r: Room | let t2 = next(t1), t3 = next(t2), t4 = next (t3) |
		enter (t1, t2, r, g) and enter (t2, t3, r, g') and enter (t3, t4, r, g) 
	}
check NoIntruder for 3 but 6 Time, 1 Room, 2 Guest
check NoIntruder for 6 -- 3 but 6 Time, 3 Room, 3 Guest
check NoIntruder for 4 but 10 Time
check NoIntruder for 4 but 7 Time, 2 Guest, 1 Room
check NoIntruder for 6 but 12 Time, 3 Guest, 3 Room

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