An alternative: counterexample checking
	• D. Jackson and C. Damon (Nitpick) suggested an alternative: check a state space of a Z-like specification up to a selected finite bound • That is, determine if there is an inconsistency within a certain bounded state space • If a counterexample is reported, one has determined a real error • If not, one can not distinguish between a consistent specification and one in which the inconsistencies are beyond the chosen bound