RTAMTへのエクスポート

SpecForgeには、Liloで記述された仕様をサードパーティのモニタリングツールで使用できるようにエクスポートする機能があります。現在は、Nickovic氏らによって開発・維持されているSignal Temporal Logic（STL）のモニタリングツールRTAMTのみをサポートしています。

エクスポート機能の呼び出し

エクスポート機能は、以下のスクリーンショットに示されているように、SpecForge VSCode拡張機能のeasy analysis UIから呼び出せます。

また、PythonスクリプトやJupyter NotebookでPython SDKを使用して呼び出すこともできます。この方法の詳細については、Python SDKドキュメントを参照してください。

rtamt_formula = specforgeClient.export(
    system="f16",
    definition="afloat",
    export_type=EXPORT_RTAMT,
    return_string=True  # Get the exported string
)
print("Exported RTAMT formula:", rtamt_formula)

RTAMTに関する補足事項

RTAMTはPythonライブラリとして配布されています。インストールと使用方法については、RTAMTドキュメントを参照してください。

RTAMTにエクスポートする際、SpecForgeは定義をインライン展開して単一の式を生成します。パラメータはデフォルト値、またはエクスポートの引数として指定された値で置き換えられます。値が提供されていないパラメータは、同じ名前の自由変数で置き換えられます。パラメータにデフォルト値がある場合でも自由変数で置き換えたい場合は、パラメータ値をJSON値nullに設定してください。

RTAMTの体系はLiloよりも単純であるため、LiloのRTAMTへのエクスポートが一部のケースでできない場合があります。RTAMTでサポートされていないLiloの機能には、文字列やレコード、time変数、区間内の非自明な式、if、did_change、will_change、previous_with、next_withなどがあります。SpecForgeが適用する最適化によってサポートされていない機能が除去される場合は、エクスポートが成功します。

スライディングウィンドウの量的演算子max_future、min_future、max_past、min_pastは、RTAMTでは対応する時相演算子（eventually、past、always、historically）に変換されます。これはRTAMTのロバストネスモードでは、式の型検査を行わないため機能します。