-- LIVENESS : LTL検査式を指定する必要がある．
LTLSPEC G (p0_state = waiting -> F p0_state = cs)
LTLSPEC G (p1_state = waiting -> F p1_state = cs)
