追加機能

属性

Liloの定義、仕様、パラメータ、シグナルは、/// で始まるdocstringに加え、属性でも注釈を付けることができます。属性は、注釈対象の直前に配置する必要があります。

属性は、ツール（特にVSCode拡張機能）によって使用される、注釈付き項目に関するメタデータを伝えるために使用されます。

#[key = "value", fn(arg), flag]
spec foo = true

未使用変数の警告を抑制する： #[disable(unused)]
- この属性を定義、パラメータ、またはシグナルに使用すると、未使用であることに関する警告が抑制されます。
- 仕様または公開されている定義は、常に使用されているとみなされます。
静的解析のタイムアウト
- 静的解析のデフォルトのタイムアウトをオーバーライドするには、timeoutを秒単位で指定できます。
- 次のようにして静的解析の項目ごとのタイムアウトを個別に指定できます： #[timeout(satisfiability = 20, redundancy = 30)]
- または、次のようにして両方を10秒に設定することもできます： #[timeout(10)]
静的解析を無効にする
- #[disable(satisfiability)]または#[disable(redundancy)]を使用して、定義に対する特定の静的解析を無効にします。
ソフト仮定： #[rigidity = "soft"]
- assumptionに適用すると、ソフト制約としてマークされます。ソルバーはこの制約を満たすように試みますが、ハード制約と矛盾する場合は緩和することがあります。詳細は厳格度レベルを参照してください。

属性を使用することで，仕様に対してラベル、エイリアス、カスタムフィールドで注釈を付けることができます。

ラベルの色はlilo.toml設定ファイルの[labels.colors]セクションで設定できます。色は16進コードまたは標準的なHTML5の色名で表されます。

[labels.colors]
production = "blue"
consumption = "magenta"
renewable = "0x00ff00"
'mitigation strategy' = "yellow"

カスタムフィールドを使用することで、仕様に追加のスカラーメタデータを付加できます。レビューステータス、担当者、優先度など、プロジェクト固有の分類に役立ちます。

#[field(priority = 1, reviewed = true, owner = "ops")]
spec brake_must_work = always (brake_pedal => eventually (deceleration > 0))

カスタムフィールドの値はスカラー値（文字列、数値、ブール値）でなければなりません。単一の仕様で同じカスタムフィールドが複数回指定された場合、最初の値が使用され、警告が出力されます。

VSCode拡張機能では、仕様ステータスペインでのフィルタリングにカスタムフィールドを使用できます。例：

完全なクエリ構文については、VSCode拡張機能を参照してください。

システムを記述する際、パラメータにはデフォルト値を指定することもできます。こうしたデフォルト値は、典型的な用例ではパラメータがそのデフォルト値でインスタンス化されるであろうことを意図するために使えます。

param temperature: Float = 25.0

デフォルト値は定数を宣言するために使用すべきものではありません。定数には、代わりに def を使用してください。

def pi: Float = 3.14159

モニタリング時、デフォルト値を持つパラメータは入力から省略できます。省略された場合、デフォルト値が使用されます。明示的に指定することもでき、その場合は指定された値が使用されます。
式をエクスポートする際、デフォルト値を持つパラメータは、エクスポート前にデフォルト値で置換されます。
デフォルト値が設定されている場合、例示機能は、ソルバーにパラメータをデフォルト値に固定するよう要求します（デフォルト値が与えられていない場合は、パラメータは自由変数として扱われます）。

エクスポートや例示などの分析を実行する際、設定のフィールドにJSONのnullを指定することができ、これによりSpecForgeは該当パラメータのデフォルト値を無視するようになります。

system main

signal p: Int
param bound: Int = 1

spec foo = p > 1 && p < bound

例示
- params = {}の場合：充足不可能（boundのデフォルト値が使用されます）
- params = { "bound": null }の場合：充足可能（ソルバーは制約を満たすboundの値を自由に選択できます）
エクスポート
- params = {}の場合：出力結果はp > 1 && p < 1
- params = { "bound": 100 }の場合：出力結果はp > 1 && p < 100
- params = { "bound": null }の場合：出力結果はp > 1 && p < bound

JSONのnull自体をLiloプログラム中でデフォルト値として使用することはできません。

ユーザーは、実体を持たない仕様（仕様スタブ）を定義できます。こうしたスタブも、通常の定義と同様にdocstringと属性を持つことができます。スタブはプレースホルダーとして使用でき、Liloの周辺ツールによってtrueとして解釈されます。

VSCode拡張機能は、（設定されている場合は）docstringに基づいてLLMによりスタブの実装を生成するためのコードレンズを表示します。

/// システムは常に最終的にエラーから回復する必要があります。
spec error_recovery

スタブは、まだ形式的に与えられていない仮定にも使用できます。

/// height は常に非負である
assumption height_non_negative