VSCode拡張機能

SpecForge VSCode拡張機能は、Lilo仕様を記述および解析するための包括的な開発環境を提供します。言語サポート、対話型解析ツール、および視覚化機能が、統一されたインターフェースで繋がっています。

セットアップについては、VSCode拡張機能のインストールガイドを参照してください。

概要

この拡張機能は以下を提供します：

• 言語サポート：Language Server Protocol（LSP）実装による構文強調表示、型検査、およびオートコンプリート
• 診断：型エラー、未使用の定義、および最適化提案のリアルタイムチェック
• コードレンズ：コードに直接埋め込まれた対話型解析ツール
• 仕様ステータスペイン：仕様と保存された解析をナビゲートするための専用サイドバー
• 仕様解析ペイン：仕様のモニタリング、実証化、反証化などのための対話型GUI
• ノートブック統合：JupyterノートブックでのSpecForge結果の視覚化のサポート
• LLM機能：AI駆動の仕様生成と診断の説明

設定

拡張機能には、実行中のSpecForgeサーバーが必要です。VSCodeの設定でサーバー接続を構成します：

• API Base URL：SpecForgeサーバーのURI（デフォルト：http://localhost:8080）

  • 設定 → 拡張機能 → SpecForge → Api Base Urlからアクセス
  • または設定ID：specforge.apiBaseUrlを使用

• Enable Preview Features：仕様ステータスサイドバーを含む実験的機能を有効化

  • 設定 → 拡張機能 → SpecForge → Enable Preview Featuresからアクセス
  • または設定ID：specforge.enablePreviewFeaturesを使用

言語機能

解析と型検査

拡張機能は、仕様を記述する際にリアルタイムでチェックを実行します。エラーには下線が引かれます。該当箇所のコードにカーソルを合わせると、エラーが表示されます：

拡張機能は構文エラー、型エラーなどをチェックします。

ドキュメントアウトライン

拡張機能は、仕様ファイルの階層的なアウトラインを提供します：

• VSCodeのエクスプローラーサイドバーで「アウトライン」ビューを開く
• すべての仕様、定義、シグナル、およびパラメータを一目で確認
• 任意のシンボルをクリックして定義にジャンプ
• アウトラインは自動的に更新されます

診断

拡張機能は自動的にさまざまなチェックを実行し、フィードバックを提供します。

診断にカーソルを合わせると、メッセージが表示されます。

診断には以下が含まれます：

• 未使用のsignal、param、defなどの警告
• 最適化の提案
• 間隔で時間依存の式を使用することに関する警告（設定されている場合）

コードレンズ

コードレンズは、コード内の仕様の上に表示される対話型ボタンで、警告などの情報と（場合により）それに応じてできることを提示します。

充足可能性チェック

各仕様の上に、仕様が充足可能かどうかを示すコードレンズが表示されます：

以下はSpecForgeが充足不可能である可能性があると検出した仕様の例です：

ユーザーは説明を求めることができます：

SpecForgeが充足可能性を判断できなかった場合、タイムアウトを長くして解析を再試行することができます。

冗長性

システムが仕様が冗長である可能性があると検出した場合、警告がコードレンズとして表示されます：

この仕様はnoSolarAtNightとdiverseMixによって暗黙的に必ず成り立つため、書く必要がないということをSpecForgeが示しています。Explainをクリックすると、冗長性の説明が生成されます：

仕様スタブ

specが本体を持たない場合、それは仕様スタブです。この場合、コードレンズはAIを使用した仕様生成を提案します。

Generate with LLMをクリックすると、現在のシステムで機能する仕様の定義が生成されます。仕様があまりにも曖昧である場合、または生成に他の障害がある場合は、エラーメッセージが表示されます。

仕様ステータスペイン

仕様ステータスパネルにアクセスするには、VSCodeの左側にあるSpecForgeアイコンをクリックします：

サイドバーには、すべての仕様ファイルと定義されている仕様がリストされます：

仕様の横にあるAnalyzeをクリックすると、仕様解析ウィンドウが表示されます。これを使用して、さまざまな仕様解析タスクを起動できます：モニタリング、実証化、エクスポート、アニメーション、および反証化。

たとえば、仕様をモニタリングするには、ドロップダウンからMonitorを選択し、モニタリングするデータファイルを選択して、Run Analysisをクリックします。

解析の結果が表示されます。青い領域は、仕様が真である時間を表します。大きなデータファイルの場合、ブール値の結果のみが表示されます。仕様がある時点で偽である理由をよりよく理解するには、ポイントを選択してDrill Downをクリックします。

ドリルダウンは、デバッグツリーを表示するために、完全なデータソースの十分に小さいセグメントを選択しました。これは、仕様全体のモニタリング結果のツリーを表示します。各ノードは折りたたみまたは展開できます。タイムライン上にカーソルを合わせると、サブ式の結果タイムラインで関連する領域も強調表示されます。タイムライン上にカーソルを合わせると、そのサブ式のその時点での結果が真または偽である理由の説明が表示されます。

このような仕様解析は、Save Analysisボタンをクリックすることで保存できます。

プロジェクト内で解析を保存する場所を選択します。

保存された解析は、関連する仕様の下の仕様ステータスサイドパネルに表示されます。

解析タイプ

GUIは5種類の解析をサポートしています：

1. Monitor

記録されたシステムの動作が仕様を満たしているかどうかをチェックします。

入力：

• Signal Data：時系列データを含むCSV、JSON、またはJSONLファイル
  • CSV：列ヘッダーはシグナル名と一致する必要があります
  • JSON/JSONL：シグナル名と一致するキーを持つオブジェクト
• Parameters：パラメータ値を含むJSONオブジェクト
• Options：モニタリング設定（モニタリングオプションを参照）

出力：

• 時間経過に伴う仕様の充足を示すモニタリングツリー
• サブ式へのドリルダウン
• シグナル値の視覚化

例：

{
  "min_temperature": 10.0,
  "max_temperature": 30.0
}

2. Exemplify

仕様を満たす例のトレースを生成します。

入力：

• Number of Points：生成する時間ポイントの数（デフォルト：10）
• Timeout：生成に費やす最大時間（デフォルト：5秒）
• Also Monitor：生成されたトレースのモニタリングツリーも表示するかどうか
• Assumptions：満たすべき追加の制約（仕様式の配列）

出力：

• 時系列として生成されたシグナルデータ
• 「Also Monitor」が有効な場合のオプションのモニタリングツリー
• 生成されたデータのCSV/JSONエクスポート

ユースケース：

• 有効な動作がどのようなものかを理解する
• リアルなデータで他のコンポーネントをテストする
• テストフィクスチャの作成
• 仕様が意味をなすことを検証する

3. Falsify

外部モデルを使用して、仕様に違反する反例を検索します。

前提条件：

• lilo.tomlに反証スクリプトを登録する必要があります：

[[system_falsifier]]
name = "Temperature Model"
system = "temperature_control"
script = "falsifiers/temperature.py"

反証スクリプトプロトコル：

スクリプトは次のコマンドライン引数を受け取ります：

• --system：システム名
• --spec：仕様名
• --options：オプションを含むJSON文字列
• --params：パラメータ値を含むJSON文字列
• --project-dir：プロジェクトルートへのパス

スクリプトは以下を行う必要があります：

1. 仕様に従ってシステムをシミュレートする
2. 仕様に違反するトレースを検索する
3. 成功または失敗のいずれかで正しい形式のJSONを出力する

入力：

• Falsifier：設定された反証器から選択（ドロップダウン）
• Timeout：反証の最大時間（デフォルト：240秒）
• Parameters：パラメータ値を含むJSONオブジェクト

出力：

• 反例が見つかった場合：
  1. 失敗したトレースを示す反証結果
  2. 反例の自動モニタリング
  3. 仕様が失敗する場所/方法の視覚化
• 反例が見つからなかった場合：成功メッセージ

スクリプトが実行可能であることを確認してください：

chmod +x falsifiers/temperature.py

4. Export

仕様を他の形式に変換します。

エクスポート形式：

• Lilo：オプションの変換を伴う.lilo形式としてエクスポート
• JSON：機械可読のJSON表現

入力：

• Export Type：ターゲット形式を選択
• Parameters：パラメータ値（エクスポートに必要な場合）

出力：

• 選択された形式でエクスポートされた仕様
• ファイルに保存できます

ユースケース：

• 他のツールとの統合
• ドキュメント生成
• 仕様のアーカイブ

5. Animate

時間の経過とともに仕様の動作を示すアニメーションを作成します。

入力：

• SVG Template：プレースホルダーを含むSVGファイルへのパス
• Signal Data：時系列データを含むCSV、JSON、またはJSONLファイル

出力：

• システムの進化を示すフレームごとのSVG画像
• アニメーション化された視覚化に組み合わせることができます

SVGテンプレート形式：

SVGテンプレートには、シグナル値のdata-属性を含める必要があります。例：

<svg
  xmlns="http://www.w3.org/2000/svg"
  width="100"
  height="100"
  viewBox="0 0 40 40"
  role="img"
  aria-label="Transformed ball"
>
  <rect width="100%" height="100%" fill="white" />
  <g transform="translate(0,50) scale(1,-1)">
    <circle cx="20" data-cy="temperature" cy="0" r="3" fill="black" stroke="white" />
  </g>
</svg>

この例では、<circle>要素のcy属性は、data-cy="temperature"属性のおかげで、temperatureシグナルの値によってアニメーション化されます。

モニタリングオプション

MonitorまたはFalsify解析を実行する際に、次のオプションを構成できます：

• Time Bounds：モニタリングを特定の時間範囲に制限
• Sampling：時間解像度を調整
• Signal Filtering：特定のシグナルのみをモニタリング
• （追加のオプションが利用可能な場合があります）

結果の操作

モニタリングツリー

モニタリングツリーには以下が表示されます：

• Root：全体的な仕様の結果（真/偽/不明）
• Sub-expressions：仕様が真または偽である理由をドリルダウン
• Timeline：任意の式にカーソルを合わせて、いつ真/偽であるかを確認
• Highlighting：カーソルを合わせると、関連するセグメントが強調表示されます

保存された解析の読み込み

保存された.analysis.sfファイルを開くと、次のことができます：

• 元の設定を確認する
• 同じ設定で解析を再実行する
• パラメータを変更して再実行する
• 結果をエクスポートする

解析エディターは、メインの解析GUIと同じインターフェースを提供しますが、保存された設定で事前に入力されています。

解析はファイルです。解析を変更した場合は、保存する必要があります。

Jupyterノートブック統合

拡張機能には、JupyterノートブックでSpecForgeの結果を表示するためのノートブックレンダラーが含まれています。

アクティベーション

レンダラーは次の場合に自動的にアクティブになります：

• Jupyterノートブック（.ipynbファイル）
• VSCode対話型Pythonウィンドウ

Python SDKでの使用

SpecForge Python SDKを使用する場合、結果は自動的にレンダリングされます：

from specforge import SpecForge

sf = SpecForge()
result = sf.monitor(
    spec_file="temperature_control.lilo",
    definition="always_in_bounds",
    data="sensor_logs.csv",
    params={"min_temperature": 10.0, "max_temperature": 30.0}
)

# resultはノートブックで自動的にレンダリングされます
result

スニペット

拡張機能は、一般的なSpecForge操作（monitor、exemplify、export）のためのPythonコードスニペットを提供します。スニペット名を入力してTabキーを押すと、プレースホルダーを挿入してナビゲートできます。

トラブルシューティング

拡張機能が動作しない

SpecForgeサーバーを確認してください：

• サーバーが実行中であることを確認します（SpecForgeのセットアップを参照）
• 設定のAPI base URLがサーバーと一致することを確認します
• サーバーログでエラーを確認します

言語サーバーを再起動してください：

• コマンドパレットからSpecForge: Restart Language Serverを実行します
• 「出力」パネル（表示 → 出力）を確認し、ドロップダウンから「SpecForge」を選択します

診断が表示されない

更新をトリガーしてください：

• ファイルを保存します（Ctrl+S / Cmd+S）
• ファイルを閉じて再度開きます
• 言語サーバーを再起動します

サーバー接続を確認してください：

• ステータスバーで接続ステータスを確認します
• 設定されたURLでサーバーにアクセスできることを確認します

コードレンズが表示されない

設定を確認してください：

• VSCodeでコードレンズが有効になっていることを確認します：Editor > Code Lens
• ファイルを保存してコードレンズの計算をトリガーします

エラーを確認してください：

• 解析を妨げる解析エラーまたは型エラーを探します
• コード内の赤い波線を修正します

解析GUIが読み込まれない

webviewを確認してください：

• 開発者ツールを開きます：ヘルプ > 開発者ツールの切り替え
• コンソールタブでエラーを探します
• webview iframeが読み込まれたかどうかを確認します

サーバー接続を確認してください：

• API base URLが正しいことを確認します
• ブラウザでURLをテストします（JSON応答が表示されるはずです）

反証スクリプトエラー

スクリプトのセットアップを確認してください：

• lilo.tomlのスクリプトパスを確認します
• スクリプトが実行可能であることを確認します：chmod +x script.py
• 例の引数でスクリプトを手動でテストします

スクリプト出力を確認してください：

• スクリプトは有効なJSONを出力する必要があります
• 正しい結果形式を使用します（Falsifyを参照）
• エラーメッセージのためにスクリプトログを確認します

一般的な問題：

• ENOENT：スクリプトファイルが見つかりません（パスを確認）
• EACCES：スクリプトが実行可能ではありません（chmod +xを実行）
• 解析エラー：無効なJSON出力（スクリプト出力形式を確認）