NuSMVで書いたエレベータシステムを拡張性などを考えてモジュール化してみることに。
仕様書を見る限り、モジュールの引数には原子式のみが対応していると思われるので、各モジュールの変数を引数に指定することになる。
しかし問題がある。
引数に変数を指定すると、1つのモジュールを作成するのに大量の引数が必要となるのだ。
こうなると一気に可読性が落ち、ソースコードの書き方に問題が出る。
この件についてNuSMVの公式ページにあるサンプルソースを見ていると、モジュールの引数にモジュールが指定されていることを見つける。
というわけで、色々仕様変更をしなければいけなくなりそうなのだが、書きかけのソースコードの中のモジュールの引数にモジュールを設定して再び書いてみる。
基本的な構文エラーが出たが、簡単にバグは取れたので問題なく実行することが出来た。
よって、NuSMVではモジュールの引数にモジュールを渡すことが出来る。
結果として、元のモジュール分割されていないソースコードからモジュール分割を行った結果、100行近くのソースが削れた。
そして心持、LTLでの検証早くなった気がする。
