NuSMVで書いたエレベータシステムを拡張性などを考えてモジュール化してみることに。 仕様書を見る限り、モジュールの引数には原子式のみが対応していると思われるので、各モジュールの変数を引数に指定することになる。 しかし問題がある。 引数に変数を指…