A Finite-Domain Semantics for Testing Temporal Logic Specifications