小さいモデル（状態機械）の連結で苦しんでいて、あまりに想像がつかないのでモデル検査にかけてみたら deadlock 見つけられた時の顔をしています