やったこと

PTDA

Parametric Timed Data Automata。
和賀さんの論文を読んで、実装してみている。

難しいと思ったのがε遷移のときのクロックの扱いだと気付いた。
どのタイミングで遷移したのか分からなくなるので、クロックのリセットタイミングが範囲 (制約式) になる。
で、そこから別の制約を満たしているかチェックしていくと、次の遷移でそのタイミングがより詳細化されたりして、状況がかなり複雑になる。
ちゃんと実装しようと思うと、PPLみたいな多面体を扱えるライブラリを使って、制約を正しく管理しないといけないっぽい。

ただ、ε遷移でのリセットを禁止すれば、クロックのリセットタイミングが必ず固定値になるので、問題なくやれそうな気がしている。
この方針で実装してみよう。

あと個人的にScala 3がつらい。
インデント構文がかなり苦手だと気付いた。

ミリシタ

なんか次のイベントがすごそう。
文字化け予告も面白かったので、ちょっと楽しみ。