Question 5 - Given a schema, define the Alloy spec.

Look at the following schema (from Software Engineering I)

	[Store_Q5.jpg]

Which one of the following is the correct Alloy translation:

1 -

sig Store {
	store: Word -> Word
}

sig Word {}

fact unique {
	all a: Word, all x,y: Word |
		x -> a in store and y -> a in store
			implies x = y
}


2 -

sig Store {
	store: Word -> Word
}

sig Word {}

fact unique {
	all a,x,y:Word | some s:Store |
		a -> x in s.store and a -> y in s.store
			implies x = y
}

3 -

sig Store {
	store: Word -> lone Word
}

sig Word {}

fact singleStore { one Store }