最後の段落しか読んでなかった
unboundとは。temporal logicも雰囲気しかわからない
> impossible to write an unbound model
->
> guaranteed that every spec is over a finite state space
REPLはそう