A Finite Semantics of Simply-Typed Lambda Terms for Infinite Runs of Automata