refineFinite

在进行trace abstraction验证终止性的过程中，一条infeasible的前缀被视为weak Büchi automaton——有一个唯一的终止状态（标记false）以及 $Σ$ 自圈。