SpecForgeユーザーガイド

SpecForgeは、時系列システムを記述するために設計されたドメイン特化言語であるLiloをベースにした、AI駆動の形式仕様作成ツールです。

このガイドでは、インストール方法、Lilo仕様言語、Python SDK、およびVSCodeでのLiloの使用について説明します。

このガイドには英語版もあります。(A version of this guide in English is also available.)

はじめに

Liloの仕様ファイルを作成するには、次の2つが必要です：

• SpecForgeサーバー（Docker経由）
• VSCode拡張機能

SpecForgeサーバー

Dockerイメージ

セットアップ（1回のみ）：

1. 提供されたJSONキーをどこかに保存します。例：some_dir/key.json
2. 作業ディレクトリで以下のコマンドを実行し、Google Artifact Registryで認証を行います：

cat key.json | docker login -u _json_key --password-stdin https://asia-northeast1-docker.pkg.dev

Dockerは今後、ImironのDockerイメージレジストリからプルするためにこのキーを使用します。

イメージの更新（必要な場合）：

最新のイメージをプルするには、以下を実行します：

docker compose pull

設定

SpecForgeサーバーはポート8080で実行されます。

docker-compose.ymlでは、以下の環境変数を設定します：

• OPENAI_KEY: https://platform.openai.com/api-keys から取得できます

- OPENAI_KEY=${OPENAI_KEY}

OpenAI APIキーを設定しない場合、SpecForgeのLLMサポートは無効になります。

アプリの実行

SpecForgeを実行するには、Docker Composeが必要です。これは、Dockerをインストールしていればほとんどの場合既に利用可能です。docker-compose.ymlが現在のディレクトリにある状態で以下を実行します：

docker compose up --abort-on-container-exit

[!NOTE] --abort-on-container-exitは、起動時のエラーでコンテナが素早く失敗するために必要です。

Visual Studio Code用SpecForge

ステップ1：Dockerコンテナが実行中であることを確認

• SpecForgeの最新イメージをプルし、Dockerコンテナを実行します。
  • 手順については前のセクションを参照してください。

ステップ2：SpecForge用VSCode拡張機能

このフォルダにはlilo-language-X.X.X.vsixファイルが含まれています。この拡張機能をインストールするには、VSCodeの拡張機能タブまたはコマンドパレットを使用します。

拡張機能タブ

• 拡張機能タブを開きます（Ctrl+Shift+XまたはCmd+Shift+X）
• 右上の3つの点をクリックします
• VSIXからインストール...を選択します

コマンドパレット

• コマンドパレットを開きます（Ctrl+Shift+PまたはCmd+Shift+P）
• Extensions: Install from VSIX...と入力します
• .vsixファイルを選択します

Lilo言語

Liloは、複雑な時間依存システムの動作を記述、検証、監視するために設計された形式仕様言語です。

Liloにより以下のことができます：

• 時間軸にまたがる性質を定義するための強力な時相演算子を備えつつも馴染みのある構文を使用して式を記述できます。
• レコードを使用してシステムのデータをモデル化するためのデータ構造を定義できます。
• システムと呼ばれる機構を使用して仕様を構造化できます。

型と式

Liloは式ベースの言語です。つまり、単純な算術から複雑な時相プロパティまで、ほとんどの構造は時系列値に評価される式です。このセクションでは、Lilo式の基本的な構成要素について詳しく説明します。

コメント

コメントブロックは/*で始まり、*/で終わります。これらのマーカー間のすべては無視されます。

行コメントは//で始まり、行の残りがコメントであることを示します。

ドキュメント文字列は//の代わりに///で始まり、さまざまな言語要素にドキュメントを添付します。

プリミティブ型

Liloは型付き言語です。プリミティブ型は次のとおりです：

• Bool： ブール値。trueとfalseが該当します。
• Int： 整数値。例：42
• Float： 浮動小数点値。例：42.3
• String： テキスト文字列。二重引用符で囲まれて書かれます。例："hello world"

型エラーは次のようにユーザーに通知されます：

def x: Float = 1.02

def n: Int = 42

def example = x + n

このドキュメントページのコードブロックは編集可能です。例えば、型エラーを修正するためにnの型をFloatに変更してみてください。

演算子

Liloは以下の演算子を使用します。優先順位の高い順（最高から最低）にリストされています。

• 前置否定：-xはxの符号反転、!xはxの否定です。

• 乗算と除算：x * y、x / y

• 加算と減算：x + y、x - y

• 数値比較：

  • ==： 等しい
  • !=： 等しくない
  • >=： 以上
  • <=： 以下
  • >： 真に大きい
  • <： 真に小さい 比較は同方向のものを連鎖させることができます。例えば0 < x <= 10は0 < x && x <= 10と同じ意味です。

• 時相演算子

  • always φ： φは将来の全ての時点で真
  • eventually φ： φは将来のある時点で真
  • past φ： φは過去のある時点で真だった
  • historically φ： φは過去の全ての時点で真だった
  • will_change φ： φは将来のある時点で値が変わる
  • did_change φ： φは過去のある時点で値が変わった
  • φ since ψ： ψが過去のある時点で真で、それ以前の全ての時点でφが真だった
  • φ until ψ： ψが真になるまでの将来の全ての時点でφが真
  • next φ： φは1つ次の（離散的な）時点で真
  • previous φ： φは1つ前の（離散的な）時点で真

  時相演算子は区間で修飾できます：

  • always [a, b] φ： a時間単位先からb時間単位先までの間の全ての時点でφが真
  • eventually [a, b] φ： a時間単位先からb時間単位先までの間のある時点でφが真
  • φ until [a, b] ψ： a時間単位先からb時間単位先までの間のある時点でψが真になり、それまでの全ての時点でφが真
  • 同様の区間修飾が他の時相演算子でも使えます。
  • 区間でinfinityを使用できます：[0, infinity]。

• 連言 x && y： xとyの両方が真

• 選言 x || y： xまたはyのいずれかが真

• 含意と等価：

  • x => y： xが真の場合、yも真でなければならない
  • x <=> y： xが真であるのは、yが真であるとき、かつそのときに限る

組み込み関数

いくつかの組み込み関数が用意されています：

• floatはIntからFloatを生成します：

  def n: Int = 42
  
  def x: Float = float(n)
  

• timeはシグナルの現在時刻を返します。

条件分岐

条件分岐を使用すると、特定の式の真偽に基づいて仕様を異なる値へと評価させることができます。if-then-else構文を使用します。

if x > 0 then "positive" else "non-positive"

Liloの重要な機能は、if/then/elseが文ではなく式であることです。つまり、常に値に評価されるため、else分岐は必須です。

if直後の式はBoolに評価される必要があります。then節とelse節は互換性のある型の値を生成する必要があります。例えば、then節がIntに評価される場合、else節もIntに評価される必要があります。

条件分岐は式が期待される場所ならどこでも使用でき、より複雑なロジックを処理するためにネストできます。

// ゼロ除算を回避
def safe_ratio(numerator: Float, denominator: Float): Float =
  if denominator != 0.0 then
    numerator / denominator
  else
    0.0 // デフォルト値を返す

// ネストされた条件式
def describe_temp(temp: Float): String =
  if temp > 30.0
    then "hot"
  else if temp < 10.0
    then "cold"
  else
    "moderate"

if _ then _ else _は時点ごと(pointwise)であることに注意してください。つまり、条件はすべての時点に独立して適用されます。

レコード

レコードは、フィールドと呼ばれる名前付きの値をグループ化する複合データ型で、仕様内で構造化データをモデル化するために不可欠です。

Lilo言語は、匿名の、構造的に型付けされた、拡張可能なレコードをサポートしています。

構築と型

中括弧で囲まれたfield = valueペアのカンマ区切りリストを提供することで、レコード値を構築できます。レコードの型は、フィールド名とそれらに対応する値の型から推論されます。

例えば、次の式は2つのフィールドを持つレコードを作成します：型Intのfooと型Stringのbar。

{ foo = 42, bar = "hello" }

結果の値は構造的型{ foo: Int, bar: String }を持ちます。コンストラクタ内のフィールドは順不同です。

type宣言を使用して名前付きレコード型を宣言することもできます。明確性と再利用性の観点から、レコード型はtype宣言で定義することを強く推奨します。

/// 2D座標系の点を表します。
type Point = { x: Float, y: Float }

// Point型の値を構築
def origin: Point = { x = 0.0, y = 0.0 }

フィールドパニング

レコードに同名で格納されるべき名前がすでにスコープ内にある場合、明示的な割り当てを省略してフィールドをパン (pun) できます。例えば{ foo }は{ foo = foo }の省略形です。

def foo: Int = 42
def bar: String = "hello"

def record_with_puns = { foo, bar }

パニングは、レコードリテラルや更新を含む、レコードフィールドがリストされる場所ならどこでも機能します。各パンは、型チェック中に通常のfield = valueペアに展開されます。

パスフィールド構築

ネストされたレコードは、ドット区切りのパスで各フィールドを記述することで、一度に作成または拡張できます。最後のフィールドに至るまでの各セグメントはその断片を含むレコードを指すものであり、コンパイラは各断片をレコード式へと適切に統合してくれます。

type Engine = { status: { throttle: Int, fault: Bool } }

def default_engine: Engine =
  { status.throttle = 0, status.fault = false }

フィールドはやはり順不同で、どのような順序で記述されていても適切なレコードにマージされます。ドット区切りのパスはパニングと組み合わせることはできません。ドット区切りのパスで指定する場合は、{ status.throttle }の代わりに{ status.throttle = throttle }と書きます。

withによるレコード更新

{ base with fields }を使用して、既存のレコードをコピーし、特定のフィールドを上書きします。更新は、レコード構築と同じ構文規則に従います：通常の割り当て、パン、ドット付きパスを混在させることができます。

type Engine = { status: { throttle: Int, fault: Bool } }

def base: Engine =
  { status.throttle = 0, status.fault = false }

def warmed_up: Engine =
  { base with status.throttle = 70 }

def acknowledged: Engine =
  { warmed_up with status.fault = false }

更新されたすべてのフィールドは、ベースレコードにすでに存在している必要があります。パス更新を使用すると、構造全体を再構築することなく、深くネストされた部分を書き換えることができます。

射影

レコード内のフィールドの値にアクセスするには、ドット（.）構文を使用します。pがxという名前のフィールドを持つレコードの場合、p.xはこの値にアクセスする式です。

type Point = { x: Float, y: Float }

def is_on_x_axis(p: Point): Bool =
  p.y == 0.0

レコードはネストでき、射影は連鎖できます。

type Point = { x: Float, y: Float }
type Circle = { center: Point, radius: Float }

def is_unit_circle_at_origin(c: Circle): Bool =
  c.center.x == 0.0 && c.center.y == 0.0 && c.radius == 1.0

ローカルバインディング

ローカルバインディングを使用すると、式に名前を割り当てることができ、その後の式で使用できます。これはletキーワードを使用して実現され、仕様の明確性、構造、効率を向上させるために非常に貴重です。

ローカルバインディングはlet name = expression1; expression2という形式をとります。これはexpression1の結果をnameにバインドします。バインディングnameは、バインディングのスコープであるexpression2内でのみ表示されます。

letバインディングの主な目的は次のとおりです：

1. 可読性：複雑な式をより小さな名前付きの部分に分割することで、ロジックを理解しやすくします。
2. 再利用：部分式が複数回使用される場合、それを名前にバインドすることで繰り返しと潜在的な再計算を回避できます。

辺の長さa、b、cから三角形の外接円の面積を計算する次の式を考えてみましょう：

def circumcircle(a: Float, b: Float, c: Float): Float =
  (a * b * c) / sqrt((a + b +c) * (b + c - a) * (c + a - b) * (a + b - c))

letバインディングを使用すると、ロジックがはるかに明確になります：

def circumcircle(a: Float, b: Float, c: Float): Float =
  let pi = 3.14;
  let s = (a + b + c) / 2.0;
  let area = sqrt(s * (s - a) * (s - b) * (s - c));
  let circumradius = (a * b * c) / (4.0 * area);
  circumradius * circumradius * pi

バインドされた変数（s、area、circumradius）の型は、それが割り当てられた式から自動的に推論されます。複数のletバインディングを連鎖させて、計算を段階的に構築することもできます。

システム

最終的に、Liloはシステムを指定するために使用されます。システムは、時系列入力シグナル、（非時系列の）パラメータ、および仕様の宣言をまとめたものです。システムには補助的な定義も含まれます。

システムファイルは、システム宣言で始まる必要があります。例：

system Engine

システムの名前はファイル名と一致する必要があります。

型宣言

新しい型はtypeキーワードで宣言されます。例えば、新しいレコード型Pointを定義するには以下のように記述します：

type Point = { x: Float, y: Float }

その後、ファイル内の他の場所でPointを型として使用できます。

シグナル

システムの時間変化する値はシグナルと呼ばれます。これらはsignalキーワードで宣言されます。例：

signal x: Float
signal y: Float
signal speed: Float
signal rain_sensor: Bool
signal wipers_on: Bool

システムの定義と仕様は、システムのシグナルを自由に参照できます。

シグナルは、関数型を含んでいない任意の型、つまりプリミティブ型とレコードの組み合わせにすることができます。

システムパラメータ

時間的に定数であるシステムの変数はシステムパラメータと呼ばれ、paramキーワードで宣言されます。例：

param temp_threshold: Float
param max_errors: Int

システムの定義と仕様は、システムのパラメータを自由に参照できます。システムパラメータは、監視 (monitoring) を開始する前に事前に提供する必要があることに注意してください。一方で、例示 (exemplification) に際してはシステムパラメータの値は省略できます。つまり、指定された場合、例はそれらに準拠して作成され、指定されなかった場合、例示のプロセスはそのシステムパラメータとして有効な値を見つけようとします。

定義

定義はdefキーワードで宣言されます：

def foo: Int = 42

定義はパラメータに依存することができます：

def foo(x: Float) = x + 42

定義の戻り値の型を指定することもできます：

def foo(x: Float): Float = x + 42

パラメータの型アノテーションと戻り値の型は両方とも省略可能で、指定されなかった場合は推論されます。ただし、これらの型註釈はある種のドキュメントとして常に書いておくことをお勧めします。

定義のパラメータもレコード型にすることができます。例：

type S = { x: Float, y: Float }

def foo(s: S) = eventually [0,1] s.x > s.y

定義は他の定義で使用できます。例：

type S = { x: Float, y: Float }

def more_x_than_y(s: S) = s.x > s.y

def foo(s: S) = eventually [0,1] more_x_than_y(s)

定義は、循環依存を作成しない限り、任意の順序で指定できます。

定義は、パラメータとして宣言することなく、システムの任意のシグナルを自由に使用できます。

仕様

仕様は、システムについて真であるべきことを記述したもので、システムのすべてのsignalとdefを参照でき、specキーワードを使用して宣言されます。defによく似ていますが、次の点が異なります：

• 戻り値の型は常にBoolです（指定する必要はありません）
• パラメータを持つことはできません。

例：

signal speed: Float

def above_min = 0 <= speed

def below_max = speed <= 100

spec valid_speed =
  always (above_min && below_max)

モジュール

Lilo言語はモジュールをサポートしています。モジュールはモジュール宣言で始まり、（システムと同様に）いくつかの定義から成っています：

module Util

def add(x: Float, y: Float) = x + y

pub def calc(x: Float) = add(x, x)

モジュールにはdefとtypeのみを含めることができます。

他のモジュールからアクセス可能にしたい定義は、pub（「public」の意）を付与する必要があります。

モジュールを使用するには、例えばimport Utilのようにインポートする必要があります。その後、Utilのpubな定義が修飾名で使用できるようになります。例：

import Util

def foo(x: Float) = Util::calc(x) + 42

モジュールをエイリアスで修飾してインポートすることもできます。例：

import Util as U

def foo(x: Float) = U::calc(x) + 42

修飾子なしでシンボルを使用するには、useキーワードを使用します：

import Util use { calc }

def foo(x: Float) = calc(x) + 42

静的解析

システムコードはいくつかのコード品質チェックを通過します。

一貫性チェック

仕様は一貫性がチェックされます。仕様が充足不可能かもしれない場合、警告が生成されます：

signal x: Float

spec main = always (x > 0 && x < 0)

これは、どのシステムもこの仕様を満たすことができないため、仕様に問題があることを意味します。

仕様間の不整合もユーザーに報告されます：

signal x: Float

spec always_positive = always (x > 0)
spec always_negative = always (x < 0)

この場合、各仕様は単独では充足可能ですが、いかなるシステムもこれら両方ともを満たすことはできません。

冗長性チェック

ある仕様が、システムの他の仕様によって暗黙的に示されているために冗長である場合、これも検出されます：

signal x: Float

spec positive_becomes_negative = always (x > 0 => eventually x < 0)

spec sometimes_positive = eventually x > 0

spec sometimes_negative = eventually x < 0

この場合、sometimes_negativeという仕様が冗長であることをユーザーに警告します。なぜなら、このプロパティはpositive_becomes_negativeとsometimes_positiveの組み合わせによって既に暗示されているためです。実際、sometimes_positiveはx > 0となる時点が存在することを意味し、positive_becomes_negativeに基づけば、その時点以後に x < 0となる時点が存在しなければならないと結論付けられます。

追加機能

属性

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)]を使用して、定義に対する特定の静的解析を無効にします。

パラメータのデフォルト値

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

param temperature: Float = 25.0

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

def pi: Float = 3.14159

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

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

system main

signal p: Int
param bound: Int = 1

spec foo = p > 1 && p < bound

• 例示化（Exemplification）
  • 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

規約

一部の言語では、名前のクラスを区別するために、特定の名前を大文字始まりにする必要があったりしますが、Liloは命名に関して柔軟性があり、仕様を記述するシステムの命名規則に合わせることができます。とはいえ、本ドキュメント内の例では以下の規約に基づいた名前を使用します：

• モジュールとシステムの名前は小文字のみからなるスネークケースです。例えば、ClimateControlではなくclimate_controlとします。
• signal、param、def、specの名前、引数、レコードフィールド名は小文字のみからなるスネークケースです。例えば、signal WindSpeedやsignal windSpeedではなくsignal wind_speedとします。
• ユーザー定義のものも含め、型の名前は大文字で始まるキャメルケースにする必要があります：

  type Plane = {
    wind_speed: Float,
    ground_speed: Float
  }
  

SpecForge Python SDK

SpecForge Python SDKは、SpecForge APIと連携し、形式仕様のモニタリング、アニメーション、エクスポート、および例示を可能にするためのSDKです。

インストール

cd tools/python
pip install -e .

クイックスタート

from specforge_sdk import SpecForgeClient

# クライアントの初期化
client = SpecForgeClient(base_url="http://localhost:8080")

# APIの健全性チェック
if client.health_check():
    print("✓ SpecForge APIに接続しました")
    print(f"APIバージョン: {client.version()}")
else:
    print("✗ SpecForge APIに接続できません")

主な機能

SDKは、SpecForgeの主要な機能へのアクセスを提供します：

• モニタリング: データに対して仕様をチェック
• アニメーション: 時系列の可視化を作成
• エクスポート: 仕様を異なる形式に変換
• 例示: 仕様を満たすサンプルデータを生成

ドキュメント

包括的なデモノートブック sample-project/demo.ipynb をご覧ください。以下の内容が含まれています：

• 詳細な使用例
• Jupyter notebookとの統合
• カスタムレンダリング機能
• エラーハンドリングパターン
• 完全なAPIリファレンス

APIメソッド

• monitor(spec_file, definition, data_file, ...) - 仕様のモニタリング
• animate(spec_file, data_file, svg_file, ...) - アニメーションの作成
• export(spec_file, definition, export_type, ...) - 仕様のエクスポート
• exemplify(spec_file, definition, n_points, ...) - サンプルの生成
• health_check() - APIの可用性チェック
• version() - APIバージョンの取得

対応ファイル形式

• 仕様: .lilo ファイル
• データ: .csv, .json, .jsonl ファイル
• 可視化: .svg ファイル

必要要件

• Python 3.12+
• requests>=2.25.0
• urllib3>=1.26.0

SpecForge SDK サンプルプロジェクト

このディレクトリには、SpecForge Python SDKの機能を実演する完全な例が含まれています。

ファイル

• temperature_monitoring.lilo - 温度監視のためのサンプル仕様
• sensor_data.csv - サンプルセンサーデータ（温度と湿度を含む31のデータポイント）
• demo.ipynb - すべてのSDK機能を実演するJupyterノートブック
• temperature_config.json - 温度監視例のための設定ファイル（パラメーター）
• util.lilo - サンプル仕様のためのユーティリティ関数

セットアップ

[!NOTE] 以下、ユーザーは sample_project フォルダをVSCodeで開くことを推奨します。

1. 仮想環境の作成とアクティベート

一般的に（必須ではありませんが）、仮想環境でこれを行うことが推奨されます。以下の手順に従ってください：

# サンプルプロジェクトディレクトリに移動
cd sample_project

# 仮想環境を作成
python -m venv .venv

# 仮想環境をアクティベート
# Windowsの場合：
.venv\Scripts\activate
# macOS/Linuxの場合：
source .venv/bin/activate

2. 依存関係のインストール

# SpecForge SDK Wheelをインストール
pip install ../specforge_sdk-xxx.whl

# サンプルプロジェクトの追加依存関係をインストール
pip install jupyter pandas matplotlib numpy

3. インストールの確認

# SDKが正しくインストールされたかを確認
python -c "from specforge_sdk import SpecForgeClient; print('✓ SDKが正常にインストールされました')"

サンプル例の実行

前提条件

1. SpecForge APIサーバーが http://localhost:8080/health で実行中であることを確認してください。
2. 仮想環境をアクティベートしてください**（まだアクティブでない場合）：

   # Windowsの場合：
   venv\Scripts\activate
   # macOS/Linuxの場合：
   source venv/bin/activate
   

サンプル例の実行

拡張機能が機能していることを確認するには、demo.ipynb のセルを実行します。監視コマンドの出力には視覚化が含まれているはずです。

ノートブックが正しいPythonカーネルに接続されていることを確認する必要があるかもしれません。多くの場合、.venv (Python3.X.X) または ipykernel です。これはVSCodeのノートブックインターフェースから設定できます。

サンプルデータの概要

含まれている sensor_data.csv には以下が含まれています：

• 31の時点（0.0から30.0）
• 温度の読み取り値（20.8°Cから25.0°C）
• 湿度の読み取り値（40.9%から51.5%）

このデータは、温度の境界、安定性、および湿度との相関を含むさまざまな仕様をテストするために設計されています。

環境の非アクティベート

サンプルプロジェクトでの作業が完了したら：

deactivate

トラブルシューティング

よくある問題

1. 「Module not found」エラー: 仮想環境がアクティベートされ、SDKが pip install ../specforge_sdk-xxx.whl でインストールされていることを確認してください。
2. 接続拒否: SpecForge APIサーバーが http://localhost:8080/health で実行されていることを確認してください。
3. Jupyterが見つからない: アクティベートされた仮想環境で pip install jupyter を実行してインストールしてください。
4. サンプルファイルが見つからない: sample_project ディレクトリにいることを確認してください。

セットアップの確認

# Python環境を確認
which python
pip list | grep specforge

# API接続をテスト
python -c "from specforge_sdk import SpecForgeClient; client = SpecForgeClient(); print('Health check:', client.health_check())"

変更履歴

すべての注目すべき変更はここに文書化されます。 フォーマットはKeep a Changelogに基づいています。 Liloはセマンティックバージョニングに準拠しています。

未リリース

v0.5.1 - 2025-11-05

追加

• 新しい仕様エクスポート形式：RTAMT。
• 新しいドキュメントサイト：https://docs.imiron.io/。
• gifアニメーションを作成できるようになりました。
• プロジェクトはlilo.tomlファイルで設定できるようになりました。プロジェクト設定を参照してください。
• システム反証器 (system falsifier) をlilo.tomlで登録できるようになりました。
• VSCodeの仕様ステータスに解析結果が表示されるようになりました。
• VSCodeでの仕様解析。
• 仕様解析ペインから反証エンジン (falsification engine) を実行できるようになりました。

変更

• レコード構築/更新の競合に対するより良い型エラー。
• LLMによる説明はユーザーのVSCode設定に従ってローカライズされるようになりました。
• 未定義変数のエラーで、該当スコープにある似た名前の変数が列挙されるようになりました。
• システムのグローバル変数（signalとparam）に、docstringを含め、属性を記述できるようになりました。
• コマンドJSON形式が大幅に変更され、今後は安定している（後方互換性がある）ことが期待されます。特に、ファイル名ではなくシステム名を使用します。
• パラメータにnull（JSON）を指定してデフォルトのパラメータ値を削除できるようになりました。
• LLM仕様生成は、不十分な指定の仕様に対して失敗します。
• CLIインターフェースがモジュールで動作するように更新されました。

v0.5.0 - 2025-10-14

追加

• デフォルトparam：param foo: Float = 42はパラメータfooのデフォルト値として42を設定します。
• タイムアウト属性：

  #[timeout = 3]
  spec foo = ...
  

  は、spec fooの解析タスクのタイムアウトを3秒に設定します。
• サーバー/クライアントバージョンの不一致に対する警告。
• 仕様スタブ：

  spec no_overheat
  

  は「仕様スタブ」（未実装の仕様）を作成します。AIを使用して、docstringを使用した実装を提案するコードアクションもあります。
• より長いタイムアウトでの解析の再試行：解析がタイムアウトした場合、より長いタイムアウトで再試行するコードアクションがあります。
• レコード機能：
  • レコード更新（ディープを含む）
  • フィールドのパン。
  • パス構築とパス更新。
• 未使用のdef、signal、paramに対する警告。
• VSCodeのコード階層。
• モジュール：ユーザーはモジュール（defとtype宣言のみを含む）を作成し、インポートできます。

変更

• VSCodeのコードレンズは一度に1つずつ解決されるため、より応答性の高いエクスペリエンスになります。