プロジェクト設定

Liloプロジェクトには、プロジェクトルートに任意でlilo.tomlという設定ファイルを配置することができます。

初めて使う場合はこの設定をスキップして、.lilo仕様ファイルとデータファイルをプロジェクトのルートに直接配置するだけで構いません。SpecForgeは適切なデフォルト値で動作します。

lilo.tomlを使用する場合、ファイル全体または一部フィールドが欠落していても、適切なデフォルト値が適用されます。Python SDKとVS Code拡張機能は、このファイルを読み取り、それに応じてセマンティクスを適用します。

設定ファイルは以下のような場合に有用です：

• プロジェクト名とカスタムソースパスの設定（デフォルト: プロジェクトルートまたはsrc/）
• 言語の動作のカスタマイズ（インターバルモード、フリーズ）
• 診断設定の調整（整合性、冗長性、最適化、未使用の定義）とそのタイムアウト
• 反証解析のためのsystem_falsifierエントリの登録

以下に、スキーマとデフォルト値、その後に完全な例を示します。

スキーマとデフォルト値

トップレベルのキーと、省略された場合のデフォルト値:

• project

  • name (文字列).
    • デフォルト: ""。
    • 初期化時: 指定された名前に設定されます。指定がない場合は、プロジェクトルートディレクトリの名前になります。
  • source (パス文字列). デフォルト: "src/"

• language

  • interval.mode (文字列). サポート: "static". デフォルト: "static"
  • freeze.enabled (ブール値). デフォルト: true

• diagnostics

  • consistency.enabled (ブール値). デフォルト: true
  • consistency.timeouts.named (秒、浮動小数点数). デフォルト: 0.5
  • consistency.timeouts.system (秒、浮動小数点数). デフォルト: 1.0
  • redundancy.enabled (ブール値). デフォルト: true
  • redundancy.timeouts.named (秒、浮動小数点数). デフォルト: 0.5
  • redundancy.timeouts.system (秒、浮動小数点数). デフォルト: 1.0
  • optimize.enabled (ブール値). デフォルト: true
  • unused_defs.enabled (ブール値). デフォルト: true

• [[system_falsifier]] (テーブルの配列、オプション)

  • 各エントリ: name (文字列)、system (文字列)、script (文字列)
  • 存在しないか空の場合、このキーはファイルから省略され、空のリストとして扱われます

デフォルトファイル:

[project]
name = ""
source = "src/"

lilo.tomlの例

オーバーライドを含むプロジェクトの例。

[project]
name = "my-specs"
source = "src/"

[language]
freeze.enabled = true
interval.mode = "static"

[diagnostics.consistency]
enabled = true

[diagnostics.consistency.timeouts]
named = 5.0
system = 10.0

[diagnostics.optimize]
enabled = true

[diagnostics.redundancy]
enabled = false

[diagnostics.unused_defs]
enabled = false

[[system_falsifier]]
name = "Psitaliro ClimateControl Falsifier"
system = "climate_control"
script = "falsifiers/falsify_climate_control.py"

[[system_falsifier]]
name = "Psitaliro ALKS falisifier"
system = "lane_keeping"
script = "falsifiers/alks.py"