卒研逆行

私の卒業研究の内容として

１．JAVAのソースコードを読み込む
２．読み込んだものをモデル検査用のソースに書き直す
３．モデル検査用のソースによりモデル検査を行う

と言ったものを目標としているわけなのだが、ツールを作る前に例題からどのように記述すればよいかを考えるために

１．NuSMBで動く条件と動かない条件を持った例題を書いて検査する
２．上記が成功したらJAVAに書き下ろす
３．JAVAがその状態遷移を行っていることを確認する

何で逆のことやってるんだろうね。