Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

プロジェクト設定

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

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

specforge.tomlを使用する場合、[project].sourceを指定する必要があります。その他の欠落しているフィールドには適切なデフォルト値が適用されます。Python SDKとVS Code拡張機能は、このファイルを読み取り、それに応じてセマンティクスを適用します。

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

  • プロジェクト名と明示的なソースパスの設定
  • 言語の動作のカスタマイズ（インターバルモード、フリーズ）
  • 診断設定の調整（整合性、冗長性、最適化、未使用の定義）とそのタイムアウト
  • エディタが表示する解析コードレンズのカスタマイズ
  • 反証解析のためのsystem_falsifierエントリの登録
  • 仕様検索の検証のためのvalidation_rulesの定義

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

スキーマとデフォルト値

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

  • project

    • name (文字列).
      • デフォルト: ""。
      • 初期化時: 指定された名前に設定されます。指定がない場合は、プロジェクトルートディレクトリの名前になります。
    • source (パス文字列). specforge.tomlが存在する場合は必須。ソースファイルがプロジェクトルートにある場合は"."を使用します。

  • language

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

  • diagnostics

    • consistency.enabled (ブール値). デフォルト: true
    • consistency.timeouts — 整合性チェックのSMTソルバータイムアウト:
      • named (秒、浮動小数点数). 個々の名前付き仕様ごとのタイムアウト. デフォルト: 0.5
      • system (秒、浮動小数点数). システム全体の整合性チェック（すべての仕様を一括チェック）のタイムアウト. デフォルト: 1.0
    • redundancy.enabled (ブール値). デフォルト: true
    • redundancy.timeout (秒、浮動小数点数). 個々の名前付き仕様ごとのタイムアウト. デフォルト: 0.5
    • guard_analysis.enabled (ブール値). デフォルト: true
    • guard_analysis.timeout (秒、浮動小数点数). 個々のガード付き仕様ごとのタイムアウト. デフォルト: 0.5
    • optimize.enabled (ブール値). デフォルト: true
    • unused_defs.enabled (ブール値). デフォルト: true

  • code_lenses

    • satisfiability.enabled (ブール値). 充足可能性解析のコードレンズを表示します. デフォルト: true
    • satisfiability.timeouts — 充足可能性コードレンズのSMTソルバータイムアウト:
      • named (秒、浮動小数点数). 個々の名前付き仕様ごとのタイムアウト. デフォルト: diagnostics.consistency.timeouts.namedを継承
      • system (秒、浮動小数点数). システム全体の整合性チェックのタイムアウト. デフォルト: diagnostics.consistency.timeouts.systemを継承
    • redundancy.enabled (ブール値). 冗長性解析のコードレンズを表示します. デフォルト: false
    • redundancy.timeout (秒、浮動小数点数). 個々の名前付き仕様ごとのタイムアウト. デフォルト: diagnostics.redundancy.timeoutを継承

    省略されたコードレンズのフィールドは、対応する診断設定を継承しますが、code_lenses.redundancy.enabledは例外で、デフォルトはfalseです。

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

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

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

    • 各エントリ: antecedent (クエリ文字列)、consequent (クエリ文字列)
    • --antecedent/--consequentを指定せずにspecforge validateを実行したときに使用されます。検証を参照してください。
    • 存在しないか空の場合、このキーはファイルから省略され、空のリストとして扱われます

デフォルトファイル:

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

specforge.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
timeout = 0.5

[diagnostics.guard_analysis]
enabled = true
timeout = 0.5

[diagnostics.unused_defs]
enabled = false

[code_lenses.satisfiability]
enabled = true

[code_lenses.redundancy]
enabled = true
timeout = 0.5

[[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"

[[validation_rules]]
antecedent = "label:todo"
consequent = "priority:>50"

[[validation_rules]]
antecedent = "label:blue OR label:green"
consequent = "label:grue"