追加機能

属性

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に適用すると、ソフト制約としてマークされます。ソルバーはこの制約を満たすように試みますが、ハード制約と矛盾する場合は緩和することがあります。詳細は厳格度レベルを参照してください。

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

ラベルは仕様に付与する文字列です。VSCode拡張機能の仕様サイドバーでは、仕様がラベルごとにグループ化されます。これは、安全性に関連する仕様など、仕様の一部に注目する場合に便利です。

#[label("safety", "critical")]
spec brake_must_work = always (brake_pedal => eventually (deceleration > 0))

エイリアスは、特定の言語における別名です。仕様サイドバーには、ソースファイルで使用されている名前とともにエイリアスが表示されます。

#[alias(en = "Brake Must Work", ja = "ブレーキは動作しなければならない")]
spec brake_must_work = always (brake_pedal => eventually (deceleration > 0))

シグナルやパラメータのエイリアスは、データファイル内でそれらを参照するために使用できます。詳細はデータファイルを参照してください。

1つの仕様に複数の#[label]属性や#[alias]属性を付けることができ、そのすべてが適用されます。

エイリアスは一意であることが期待されます。すなわち、あるエイリアスが別のエイリアスや他の宣言の名前と重複してはなりません。

ラベルには、specforge.toml設定ファイルで色（16進コードまたは標準的なHTML5の色名で表現）を関連付けることができます。そのためには、次のように[labels.colors]セクションを追加します。

[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拡張機能を参照してください。

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

#[default = 25.0]
param temperature: Float

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

def pi: Float = 3.14159

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

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

system main

signal p: Int
#[default = 1]
param bound: Int

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