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

SpecForge Python SDK

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

Python環境でのSDKのインストールと設定については、Python SDKのセットアップガイドを参照してください。

クイックスタート

from specforge_sdk import SpecForgeClient

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

# APIのヘルスチェック(接続確認)
if specforge.health_check():
    print("✓ SpecForge APIに接続しました")
    print(f"APIバージョン: {specforge.version()}")
else:
    print("✗ SpecForge APIに接続できません")

主な機能

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

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

ドキュメント

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

  • 詳細な使用例
  • Jupyter notebookとの統合
  • カスタムレンダリング機能

APIメソッド

SpecForgeClient(base_url, ...)

SpecForge APIクライアントを初期化します。

パラメータ:

  • base_url (str): SpecForge APIサーバーのベースURL(デフォルト: "http://localhost:8080")
  • project_dir (str/Path): オプションのプロジェクトディレクトリパス。指定しない場合、カレントディレクトリからlilo.tomlを検索します
  • timeout (int): リクエストのタイムアウト秒数(デフォルト: 30)
  • check_version (bool): 初期化時にバージョンの不一致をチェックするかどうか(デフォルト: True)

例:

specforge = SpecForgeClient(
    base_url="http://localhost:8080",
    project_dir="/path/to/project",
    timeout=60
)

monitor(system, definition, ...)

データに対して仕様をモニタリングします。評価結果とオプションでロバストネスメトリクスを返します。

主なパラメータ:

  • system (str): 定義を含むシステム
  • definition (str): モニタリングする仕様の名前
  • data_file (str/Path): データファイルのパス(CSV、JSON、またはJSONL)
  • data (list/DataFrame): 辞書のリストまたはpandas DataFrameとしての直接データ
    • 注意: data_fileまたはdataのいずれか1つのみを指定してください
  • params_file (str/Path): システムパラメータファイルのパス
  • params (dict): 辞書としての直接システムパラメータ
    • 注意: params_fileまたはparamsのうち最大1つを指定してください
  • encoding (dict): レコードエンコーディング設定
  • verdicts (bool): 評価情報を含める(デフォルト: True)
  • robustness (bool): ロバストネス解析を含める(デフォルト: False)
  • return_timeseries (bool): Trueの場合DataFrameを返す、Falseの場合JSONを表示(デフォルト: False)

例:

# データファイルとパラメータファイルでモニタリング
specforge.monitor(
    system="temperature_sensor",
    definition="always_in_bounds",
    data_file="sensor_data.csv",
    params_file="temperature_config.json"
)

# データファイルとパラメータ辞書でモニタリング
specforge.monitor(
    system="temperature_sensor",
    definition="always_in_bounds",
    data_file="sensor_data.csv",
    params={"min_temperature": 10.0, "max_temperature": 24.0}
)

# DataFrameでモニタリングし、結果をDataFrameとして取得
result_df = specforge.monitor(
    system="temperature_sensor",
    definition="temperature_in_bounds",
    data=synthetic_df,
    encoding=nested_encoding(),
    params={"min_temperature": 10.0, "max_temperature": 24.0},
    return_timeseries=True
)

# ロバストネス解析付きでモニタリング
specforge.monitor(
    system="temperature_sensor",
    definition="temperature_in_bounds",
    data_file="sensor_data.csv",
    params={"min_temperature": 10.0, "max_temperature": 24.0},
    robustness=True
)

animate(system, svg_file, ...)

仕様、データ、SVGテンプレートからアニメーションを作成します。

主なパラメータ:

  • system (str): アニメーション定義を含むシステム
  • svg_file (str/Path): SVGテンプレートファイルのパス
  • data_file (str/Path): データファイルのパス
  • data (list/DataFrame): 辞書のリストまたはpandas DataFrameとしての直接データ
    • 注意: data_fileまたはdataのいずれか1つのみを指定してください
  • encoding (dict): レコードエンコーディング設定
  • return_gif (bool): Trueの場合、base64エンコードされたGIF文字列を返す(デフォルト: False)
  • save_gif (str/Path): GIFファイルを保存するオプションのパス

例:

# Jupyterでアニメーションフレームを表示
specforge.animate(
    system="temperature_sensor",
    svg_file="temp.svg",
    data_file="sensor_data.csv"
)

# アニメーションをGIFファイルとして保存
specforge.animate(
    system="scene",
    svg_file="scene.svg",
    data_file="scene.json",
    save_gif="output.gif"
)

# GIFデータをbase64文字列として取得
gif_data = specforge.animate(
    system="temperature_sensor",
    svg_file="temp.svg",
    data=synthetic_df,
    encoding=nested_encoding(),
    return_gif=True
)

export(system, definition, ...)

仕様を異なるフォーマット(例: LILO形式)にエクスポートします。

主なパラメータ:

  • system (str): 定義を含むシステム
  • definition (str): エクスポートする仕様の名前
  • export_type (dict): エクスポート形式の設定(デフォルト: LILO)
  • params_file (str/Path): システムパラメータファイルのパス
  • params (dict): 辞書形式で直接指定されたシステムパラメータ
    • 注意: params_fileまたはparamsのうち最大1つを指定してください
  • encoding (dict): レコードエンコーディング設定
  • return_string (bool): Trueの場合、エクスポートされた文字列を返す。Falseの場合JSONを表示(デフォルト: False)

例:

# LILO形式に文字列としてエクスポート
lilo_result = specforge.export(
    system="temperature_sensor",
    definition="always_in_bounds",
    export_type=EXPORT_LILO,
    return_string=True
)
print(lilo_result)

# パラメータファイルでエクスポート
export_result = specforge.export(
    system="temperature_sensor",
    definition="always_in_bounds",
    export_type=EXPORT_LILO,
    params_file="temperature_config.json",
    return_string=True
)

# パラメータ辞書でエクスポート
export_result = specforge.export(
    system="temperature_sensor",
    definition="always_in_bounds",
    export_type=EXPORT_LILO,
    params={"min_temperature": 10.0, "max_temperature": 24.0},
    return_string=True
)

# JSON形式にエクスポート(Jupyterで表示)
specforge.export(
    system="temperature_sensor",
    definition="humidity_correlation",
    export_type=EXPORT_JSON
)

exemplify(system, definition, ...)

仕様を満たすサンプルデータを生成します。

主なパラメータ:

  • system (str): 定義を含むシステム
  • definition (str): 例示する仕様の名前
  • assumptions (list): 生成を制約する追加の仮定(デフォルト: [])
  • n_points (int): 生成するデータポイント数(デフォルト: 10)
  • params_file (str/Path): システムパラメータファイルのパス
  • params (dict): 辞書としての直接システムパラメータ
    • 注意: params_fileまたはparamsのうち最大1つを指定してください
  • params_encoding (dict): パラメータのレコードエンコーディング
  • timeout (int): 例示のタイムアウト秒数(デフォルト: 30)
  • also_monitor (bool): 生成されたデータもモニタリングするかどうか(デフォルト: False)
  • return_timeseries (bool): Trueの場合、DataFrameを返す。Falseの場合、JSONを表示(デフォルト: False)

例:

# 20サンプルの例を生成
specforge.exemplify(
    system="temperature_sensor",
    definition="always_in_bounds",
    n_points=20
)

# 仮定付きで例を生成
humidity_assumption = {
    "expression": "eventually (humidity > 25)",
    "rigidity": "Hard"
}
specforge.exemplify(
    system="temperature_sensor",
    definition="humidity_correlation",
    assumptions=[humidity_assumption],
    n_points=20
)

# 部分的なパラメータで例を生成(ソルバーが不足値を埋める)
specforge.exemplify(
    system="temperature_sensor",
    definition="humidity_correlation",
    assumptions=[{"expression": "always_in_bounds", "rigidity": "Hard"}],
    params={"min_temperature": 38.0},
    n_points=20
)

# 例を生成してDataFrameとして取得
example_df = specforge.exemplify(
    system="temperature_sensor",
    definition="temperature_in_bounds",
    n_points=15,
    also_monitor=False,
    return_timeseries=True
)

health_check()

SpecForge APIが利用可能で応答しているかどうかをチェックします。

戻り値: bool - APIが正常な場合True、それ以外の場合False

例:

if specforge.health_check():
    print("✓ SpecForge APIに接続しました")
else:
    print("✗ SpecForge APIに接続できません")

version()

APIサーバーのバージョンとSDKバージョンを取得します。

戻り値: "api""sdk"のキーを持つdict

例:

versions = specforge.version()
print(f"APIバージョン: {versions['api']}")
print(f"SDKバージョン: {versions['sdk']}")

対応ファイル形式

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

必要要件

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