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
	}

abstract sig Event {t, t': Time, r: Room, g: Guest}

sig Checkin extends Event {} {
	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
		}
	}

sig Checkout extends Event {} {
	r -> g in Desk.occ.t
	Desk.occ.t' = Desk.occ.t - (r ->g)
	}

sig Enter extends Event {} {
	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())
	no t'.first()
	all x: Time - last () | let x' = next (x) {
		one t.x
		all e: Event | e.t = x => {
			e.t' = x'
			(issued.x = issued.x' and cards.x' = cards.x and prev.x = prev.x' or e in Checkin)
			(occ.x = occ.x' or e in Checkin + Checkout)
			(key.x = key.x' or e in Enter)
			}
		}
	}

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

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