6.2.4 An Event-Based Variation

gistfile1.txt

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 DisjointKeySets {
	keys in 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) {
	no Guest.keys.t
	no FrontDesk.occupant.t
	all r: Room | FrontDesk.lastKey.t[r] = r.currentKey.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" => e in Entry
		occupant.t != occupant.t" => e in Checkin + Checkout
		(lastKey.t != lastKey.t" or keys.t != keys.t")
				 => e in Checkin
	}
}

// fact
pred NoIntervening {
	all c: Checkin |
		c.post = TO/last[]
		or some e: Entry {
			e.pre = c.post
			e.room = c.room
			e.guest = c.guest
		}
}

assert NoBadEntry {
	all e: Entry | let o = FrontDesk.occupant.(e.pre) [e.room] |
		some o => e.guest in o
}

check NoBadEntry for 5 but 1 Room, 2 Guest, 9 Time, 8 Event