CSSE 373 -- Formal Methods in Specification and Design

                                Quiz 9



Name:_________________________________________    Grade:______________


1. Why does Alloy's int[] operator (for converting from Int atoms to
   integer values) return a sum?






2. Rewrite the Alloy model below to not use a Boolean type.

	sig Lift {
		goingUp: Time -> Boolean,
		goingDown: Time -> Boolean
	}