10日間大学時代の気分に戻ってLTLで仕様を書いてみた
会社のイベントで1週間何しててもいい期間があったので、大学時代に研究していた形式手法の1分野であるLTL仕様からオートマトン合成の分野に触れていました。
タイムライン
- 以前使っていたAcacia+というツールがリンク切れになっていたことに驚く
- LTLからオートマトン合成のコンペティションが2014年から開催されており使いやすく高性能なLTL合成ツールの発展に貢献していた
- TLSFという生のLTLをラップした仕様形式がベンチマークの共通形式として普及していた。入出力のシグナルとオプションがLTLとセットで管理できる。
- Strixというツールが2019年のコンペで1位になっていたのでOnlineでもページで遊んでみる
- Strixが良さそうなのでDockerfile作ってインストールして触ってみる
- Strixの内部でowlというLTLパースとωオートマトン変換をやるJavaライブラリ使っていて、便利な共通ライブラリできてることに感動
- 仕様を書いて遊んでみるがなかなか欲しいオートマトンが出てこなくて苦戦
- LTLオペレーターのUntilを誤用していてWeak Untilを使わないといけなかったことに気づく
- 大学のときは仕様を書くこと自体はあまりやってなかったので大きな仕様を書くのは大変で便利なパーツを定義していって組み合わせることの重要性を認識する
- Owlのonline demoでLTLからオートマトンを作って検証しながらパーツを作っていくとやりやすかった。学生の時よりωオートマトンそのものをちゃんとトレースした気がする
- 会社のシステム開発で使えないかなーと思ってTimeout付きのシステムの仕様を書いた。
- LTLから合成されるオートマトンを見ることで必要最低限な内部状態がわかるので、システム設計のときに無駄な状態作ってないか調べるのには使えるかも。
- 上のが終わったので大学時代に一番書いてたエレベーターの仕様を書いた。何故か研究室ではエレベーターの仕様がよく使われていたが、簡単そうに見えて状態が複雑でちょうどいい題材だと気づいた。
- 呼ばれてもないのに1F->2F->3F->2F->1Fとぐるぐるまわるエレベーターはすぐ書けたが、呼ばれてないときは止まってるエレベーターを書くのは1日かかった
- 手元のMacBookProだと3F建てはできるけど、4F建てやリフト2機のエレベーターはすごく時間がかかる。
- ボタンを押したらいつか来る(
G(req -> F(grant)))仕様はできてもK時間以内に籠が来るエレベーターは3F建てが限界だった。 - 4F建て1機の必要ないときは動かないエレベーターが作れた
- 可視化してみた
成果物
感想
2014年から6年経ち2020年になったが、LTLからオートマトンを合成する計算オーダーが2-EXPなのでいくらツールが良くなっても大きい複雑な仕様は難しかった。
