Iterative process
	• Iterate SMV version of specification • Clarify and refine temporal formula • Model environment more precisely • Refine specification