オンラインモニタリング

SpecForgeには、Liloで記述された仕様をオンラインモニタリングする機能があります。オフラインモニタリングがトレース全体を処理した後に一括して判定を出すのとは対照的に、トレースを取り込みながらストリーミング方式で判定を出すことを意味します。

オンラインモニタを起動するには、specforge CLIのstreammonコマンドを使用してください。必要な引数についてはspecforge streammon --helpを実行してください。specforge streammonコマンドを実行するとモニタが起動し、STDINからトレースを取り込み、STDOUTに出力信号を生成します。

モニタはCSVまたはJSONL形式のトレースを受け付けます。CSVの場合、最初の行はヘッダーでなければならず、そのヘッダーは各信号に対応する列を識別するために使用されます。JSONLの場合、各行が信号名をキーとするJSONオブジェクトでなければなりません。RECORD_ENCODINGサブコマンドを使用して、レコードがflatまたはnested形式でエンコードされているかどうかを指定できます（データに関する章を参照）。

オンラインモニタの現在の実装は、時相演算子の区間が将来または過去の小さなウィンドウに限られている場合に最も良好に動作します。非有界な長さを持つ区間は、たとえ過去の区間であってもサポートされていません。

将来時相の時相演算子はオンラインモニタでサポートされています。それらの判定は、仕様内の最大の将来ウィンドウの分だけ遅延して生成されます。例えば、式eventually [0, 5] fをモニタリングする場合、モニタは現在時刻tの判定を、時刻t + 5までのトレースを取り込んでから生成します。