-- Alloy model of an Active Badge Location System as described in:
-- 	Roy Want, Andy Hopper, Veronica Falcão, Jonathan Gibbons.  
-- 	The Active Badge Location System.  
-- 	In ACM Transactions on Information Systems, January 1992.
-- Author: Steven Xu, Queen's University, Kingston, Canada
-- Date: Spring 2002

module ActiveBadgeSystem

sig Level { }		

sig Badge {
	-- levels of areas that the owner of a Badge are allowed to access
	accessLevel: set Level,
	-- a Badge sends signals to a Base
	signal: option Base,	
	-- the set of rooms that a Badge has been in historically
	history: set Room
}

sig Base { }

sig Room {
	-- each room is associated with an access level
	level: Level,
	-- a room has a set of bases
	bases: set Base
}

-- Entrance of a building  
sig Entrance extends Room { }
{ 	--all Badges have access to the building
	all abs: ABS, b: Badge, e: Entrance | e.Room$level in b.accessLevel
}

-- the whole ABS system
sig ABS {
	-- there are many badges registered in the system
	registered: set Badge,
	rooms: set Room,
	entrance: set Entrance,
	location: registered ->! rooms,
	prev : option ABS
}


fact {
	some Room
	some Entrance
	some Badge
	some ABS
	all r: Room | some r.bases && one r.level && some r.~rooms
}

-- a Base can not belong to more than one room
fact noSharedBase {
	all s: Base | one s.~bases 	
}

-- a Person(Badge) only has access to rooms that he is allowed to access
fact signalReceivedByBaseInAccessLevel {
	all abs: ABS, b: Badge, s: Base, r: Room | b.signal.~bases.level in  
b.accessLevel --&& sole b.signal
	--some b.(abs.location).level & b.accessLevel
}

-- the location(Room) of a Badge always contains the Base that detects  
the signal emitted by that Badge
fact locatedByBase {
	all abs: ABS, b: Badge, s: Base, r: Room |
		(b -> r) in abs.location iff s in r.bases && b.signal = s
}

-- all Badges in the ABS should have registered already
fact registeredBadgesHaveRegistered {
	all abs': ABS, b: Badge | some e: Entrance | some abs1,abs2: ABS |
		b in abs'.registered iff (register(abs1,abs2,b,e) && abs1 in  
abs'.^prev && abs2 in abs'.*prev)
}

fact stateChangedByMoveRegisterLeave {
	all a1, a2 : ABS | a1 in a2.prev iff some b : Badge, r1, r2 : Room, e:  
Entrance |
		(move(a1, a2, b, r1, r2) || register(a1,a2,b,e) || leave(a1,a2,b,e))
}

fact noSelfPrev {
	all a: ABS | a !in a.prev
}

fact prevNotSymmetric { 	
	all a1,a2: ABS | a1 in a2.prev && a2 in a1.prev => a1=a2
}

/*
fact noReflexivePrev {
	all a: ABS | a !in a.^prev
}
*/
-----------------------------------------------------------------

-- defining the case that a Badge is moving from one room to another
-- a Badge passing cross Bases within a room is not considered as  
'moving'
fun move (abs,abs': ABS, b: Badge, from,to: Room) {
	(b -> from) in abs.location &&
	to.level in b.accessLevel &&
	abs'.location = abs.location ++ (b -> to) &&
	b.history = b.history + to &&
	abs'.prev = abs &&
	abs'.registered=abs.registered && abs'.rooms=abs.rooms &&  
abs'.entrance=abs.entrance
}

-- Boolean function: true if Badge b is in Room r
fun find (abs: ABS, r: Room, b: Badge) {
	r = b.(abs.location)
}

-- Boolean function: true if Badge b2 is currently with a set of Badges  
b1(including b2 self)
fun withOthers (abs: ABS, b1: set Badge, b2: Badge) {
	b1 = b2.(abs.location).~(abs.location)
}

-- boolean function: true if the set of Badges are currently in Room r
fun look (abs: ABS, b: set Badge, r: Room) {
	b = r.~(abs.location)
}

-- boolean function: true if the set of Badges are currently in Base s  
of Room r
fun lookBase (abs: ABS, badges: set Badge, s: Base) {
	badges in (s.~bases).~(abs.location) &&
	badges in s.~signal
}

-- boolean function: happens when a Badge enters the ABS
fun register (abs,abs': ABS, b: Badge, e: Entrance) {
	abs'.registered = abs.registered + b &&
	abs'.location = abs.location ++ (b -> e) &&
	b.history = e &&
	abs'.prev = abs &&
	abs'.rooms=abs.rooms && abs'.entrance=abs.entrance
}

-- Boolean function: true when a Badge leaves the ABS
fun leave (abs,abs': ABS, b: Badge, e: Entrance) {
	e = b.(abs.location) &&
	abs'.registered = abs.registered - b &&
	abs'.location = abs.location - (b -> b.(abs.location)) &&
	abs'.prev = abs &&
	abs'.rooms=abs.rooms && abs'.entrance=abs.entrance
	--the ABS can retain the history of a left Badge
}

fun show()
{	
	--#Badge=3
	#ABS.registered=2
	--#ABS=1
	--#Room=3
	--#Level=1
}

------------------------------------------------------------------------ -------------

-- a Badge can have at most one location at any given time (the absence  
of 'location' means 'away')
assert BadgeHasAtMostOneLocation {
	all abs: ABS, b: Badge | sole b.(abs.location)
}

-- a Badge can only be located iff it's signal has been received
assert locatedBySignal {
	all abs: ABS, r: Room, b: Badge |
		--( one b.(abs.location) iff one b.signal ) &&
		( no b.signal => no b.(abs.location) )
}

-- everyone is with herself
assert withOneself {
	all abs: ABS, b2: Badge | some r: Room | some b1: set Badge |
		withOthers (abs,b1,b2) => b2 in b1
}	

-- History is consistent with access level
assert historyConsistency {
	all abs: ABS, b: Badge, r: Room | b in abs.registered =>  
(b.history).level in b.accessLevel
}

-- check function move()
assert moveWorks1 {
	all abs,abs': ABS, b: Badge, r1,r2: Room|
 		move(abs,abs',b,r1,r2) => find(abs',r2,b) && r1+r2 in b.history
}
/*
assert moveWorks2 {
	all abs,abs': ABS, b: Badge, r1,r2: Room |
 		move(abs,abs',b,r1,r2) => find(abs',r2,b) && r2 in b.history
}
*/
assert moveWorks3 {
	all abs,abs': ABS, b: Badge, r1,r2: Room |
 		move(abs,abs',b,r1,r2) && r1 != r2 => !find(abs',r1,b)
}

-- check function find(),look(),lookBase(), and withOthers()
assert findAndWithWork {
	all abs: ABS, b1,b2: Badge, r: Room, b3: set Badge |
		find (abs,r,b1) && find (abs,r,b2) && withOthers (abs,b3,b2) => b1  
in b3
}

assert findAndLookWork {
	all abs: ABS, b1: Badge, b2: set Badge, r :Room |
		find(abs,r,b1) && look(abs,b2,r) => b1 in b2
}

assert lookAndWithWork {
	all abs: ABS, b1: Badge, b2: set Badge, r :Room |
		withOthers(abs,b2,b1) && find(abs,r,b1) => look(abs,b2,r)
}

assert lookBaseWorks1 {
	all abs: ABS, b1,b2: set Badge, r: Room, s: Base |
		lookBase(abs,b1,s) && look(abs,b2,r) => b1 in b2
}

assert lookBaseWorks2 {
	all abs: ABS, b1,b2,b3: set Badge, r: Room, s1,s2: Base |
		lookBase(abs,b1,s1) && lookBase(abs,b2,s2) && s1+s2 in r.bases &&  
look(abs,b3,r) => b1+b2 in b3
}

assert withOthersIsSymmetric {
	all abs: ABS, b1,b2: Badge, bs1,bs2: set Badge |
		withOthers(abs,bs1,b2) && withOthers(abs,bs2,b1) && b1 in bs1 && b1  
!= b2  => b2 in bs2
}

-- check function register() and leave()
assert registerWorks1 {
	all abs: ABS, b: Badge | some e: Entrance | b in abs.registered => e  
in b.history
}
assert registerWorks2 {
	all abs1: ABS, b: Badge, r: Room | some abs2,abs3: ABS, e: Entrance |
		find(abs1,r,b) iff register(abs2,abs3,b,e)
}
assert leaveWorks1 {
	all abs': ABS, b: Badge | some e: Entrance | some abs: ABS |
		leave(abs,abs',b,e) => no r: Room | r in abs'.rooms && find(abs',r,b)  
--b.(abs'.location)
}

assert registerAndMove {
	all abs': ABS, b: Badge, e: Entrance, r: Room | some abs1,abs2: ABS |
		register(abs1,abs2,b,e) && move(abs2,abs',b,e,r) => e+r in b.history  
&& find(abs',r,b)
}

-- b1, b2 have same history in a2 => some a1 in a2.^prev |  
withOthers(a1, bs, b1) && b2 in bs assert sameHistoryImpliesWereTogether {
	all disj b1,b2: Badge, a2: ABS |
	    	b1+b2 in a2.registered && b1.history=b2.history => some a1: ABS,  
bs: set Badge |
			a1 in a2.^prev && withOthers(a1,bs,b1) && b2 in bs
}


assert foundAfterMove {
	all abs,abs' : ABS, b: Badge, r1,r2: Room |
		move(abs,abs',b,r1,r2) && find(abs',r2,b)
}
/*
assert noReflexivePrev {
	all a: ABS | a !in a.^prev
}	

assert prevIsTransitive {
	all a1,a2,a3: ABS | a1 in a2.prev && a2 in a3.prev =>a1 in a3.^prev
}
*/
------------------------------------------------------------------------ ----------------------------

run show for 3
run move for 3
check BadgeHasAtMostOneLocation for 3
check locatedBySignal for 5
check withOneself for 5
check historyConsistency for 3
check moveWorks1 for 3
--check moveWorks2 for 5
check moveWorks3 for 5
check findAndWithWork for 3
check findAndLookWork for 3
check lookAndWithWork for 3
check lookBaseWorks1 for 5
check lookBaseWorks2 for 5
check withOthersIsSymmetric for 3
check registerWorks1 for 3
check registerWorks2 for 5
check leaveWorks1 for 3
check registerAndMove for 3
check sameHistoryImpliesWereTogether for 4
check foundAfterMove for 3
--check noReflexivePrev for 5
--check prevIsTransitive for 5