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の主要な機能へのアクセスを提供します：

モニタリング: データに対して仕様をチェック
充足可能性: 仕様、インライン式、またはシステム全体が充足可能かどうかをチェック
妥当性: システムの仮定のもとで仕様または式が証明可能かどうかをチェック
同値性: 2つの仕様または式が論理的に同値かどうかをチェック
アニメーション: 時系列の可視化を作成
エクスポート: 仕様を異なる形式に変換
例示: 仕様を満たすサンプルデータを生成

ドキュメント

包括的なデモノートブック 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): オプションのプロジェクトディレクトリパス。指定しない場合、カレントディレクトリからspecforge.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 | None): モニタリングする仕様の名前。Noneの場合、システム内のすべての仕様を一度にモニタリングします（システム全体のモニタリング）
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）
partial_data (bool): データがシステムで宣言されたすべての信号を含まない場合でも、モニタリングを許可します（デフォルト: True）。有効にすると、データにない信号はエラーの原因とはならず、不明として扱われます。すべての信号の値をデータに含めることを必須にするにはFalseに設定します
return_timeseries (bool): Trueの場合DataFrameを返す、Falseの場合JSONを表示（デフォルト: False）

definition=Noneの場合、モニターはシステム内のすべての仕様を提供されたデータに対して評価し、結果をまとめて返します。システム全体でどの仕様が合格し、どの仕様が不合格かをすばやく把握するのに役立ちます。

例:

# データファイルとパラメータファイルでモニタリング
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つのみを指定してください
params_file (str/Path): システムパラメータの値を含むJSONファイルのパス
params (dict): 辞書としての直接システムパラメータ
- 注意: params_fileまたはparamsのうち最大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
)

# システムパラメータを指定してアニメーションを作成
specforge.animate(
    system="temperature_sensor",
    svg_file="temp.svg",
    data_file="sensor_data.csv",
    params={"temp_threshold": 25.0}
)

# ファイルからパラメータを読み込んでアニメーションを作成
specforge.animate(
    system="temperature_sensor",
    svg_file="temp.svg",
    data_file="sensor_data.csv",
    params_file="temperature_config.json",
    save_gif="output.gif"
)

`export(system, definition, ...)`

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

主なパラメータ:

system (str): 定義を含むシステム
definition (str): エクスポートする仕様の名前
export_type (dict): エクスポート形式の設定（デフォルト: LILO）
- ライブラリで定義されているEXPORT_LILO、EXPORT_JSON、EXPORT_RTAMTのいずれかを使用します
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
)

`check_satisfiability(system, definition=None, expression=None, ...)`

単一の仕様、インライン式、またはシステム全体の充足可能性を検査します。

主なパラメータ:

system (str): 定義を含むシステム
definition (str | None): 検査する仕様の名前
expression (str | None): 指定されたシステムのコンテキストで検査するインラインLiloブール式
- 注意: definitionまたはexpressionのうち最大1つを指定してください
definitionとexpressionが両方ともNoneの場合、SDKはシステム全体を検査します
timeout (int | float): 充足可能性検査のタイムアウト秒数（デフォルト: 30）
return_details (bool): Trueの場合、ブール値の代わりに構造化された充足可能性検査のレスポンスを返します（デフォルト: False）

戻り値:

bool: 充足可能な場合はTrue、そうでない場合はFalse
return_details=Trueの場合、次の2つのキーを持つ辞書を返します：
- "status": 充足可能性検査の結果。result["status"]["tag"]を確認すると、次のいずれかの値になります：
  - "Consistent" – 仕様は充足可能です
  - "InConsistent" – 仕様は充足不能です。"contents"フィールドには、充足不能コアの詳細を示すUnsatInfoオブジェクトが含まれます
  - "Unknown" – ソルバーは充足可能性を判定できませんでした
  - "TimedOut" – ソルバーがタイムアウトしました。"contents"フィールドにはマイクロ秒単位のタイムアウト時間が含まれます
- "param_situation": 検査中にシステムパラメータ（param宣言）がどのように扱われたかを示します：
  - "UsingDefaults" – ソルバーはすべてのパラメータを宣言されたデフォルト値に固定し、その値で結果を得ました。最初に試行される方法です
  - "UnfixedParams" – ソルバーはすべてのパラメータを自由変数（制約なし）として扱いました。デフォルト値を使用した検査で"Consistent"という結果が得られなかった場合に、自由変数として再検査します
statusとparam_situationの意味のある組み合わせは次のとおりです：
- ("Consistent", "UsingDefaults") – パラメータを宣言されたデフォルト値に固定すると、仕様は充足可能です
- ("Consistent", "UnfixedParams") – 仕様は充足可能ですが、パラメータを宣言されたデフォルト値に固定した場合は充足可能ではありません
- ("InConsistent", "UnfixedParams") – パラメータのどのような値に対しても、仕様は充足不能です

例:

# 単一の仕様を検査
is_satisfiable = specforge.check_satisfiability(
    system="temperature_sensor",
    definition="always_in_bounds"
)
print(is_satisfiable)

# パラメータの扱いを確認するために詳細なレスポンスを取得
details = specforge.check_satisfiability(
    system="temperature_sensor",
    definition="always_in_bounds",
    return_details=True
)
print(details["status"]["tag"])        # 例: "Consistent"
print(details["param_situation"])      # 例: "UsingDefaults"または"UnfixedParams"

# システム全体を検査してブール値を取得
system_is_satisfiable = specforge.check_satisfiability(
    system="temperature_sensor"
)
print(system_is_satisfiable)

# システムのコンテキストでインライン式を検査
expr_is_satisfiable = specforge.check_satisfiability(
    system="temperature_sensor",
    expression="always (min_temperature <= temperature <= max_temperature)"
)
print(expr_is_satisfiable)

`check_validity(system, definition=None, expression=None, ...)`

システムの仮定のもとで、単一の仕様またはインライン式の妥当性を検査します。

主なパラメータ:

system (str): 定義を含むシステム、または式が解析されるコンテキストとなるシステム
definition (str | None): 証明する仕様の名前
expression (str | None): 指定されたシステムのコンテキストで証明するインラインLiloブール式
- 注意: definitionまたはexpressionのいずれか1つのみを指定してください
timeout (int | float): 妥当性検査のタイムアウト秒数（デフォルト: 30）
return_details (bool): Trueの場合、ブール値の代わりに構造化された妥当性検査のレスポンスを返します（デフォルト: False）

戻り値:

bool: 対象が妥当な場合はTrue、そうでない場合はFalse
return_details=Trueの場合、SpecForge APIから返された構造化された妥当性検査の結果を返します。結果についてはresult["status"]["tag"]を、デフォルト値を持つパラメータの扱いについてはresult["param_situation"]を確認してください。

例:

# 単一の仕様を検査
is_valid = specforge.check_validity(
    system="temperature_sensor",
    definition="always_in_bounds"
)
print(is_valid)

# システムのコンテキストでインライン式を検査
expr_is_valid = specforge.check_validity(
    system="temperature_sensor",
    expression="always (min_temperature <= temperature <= max_temperature)"
)
print(expr_is_valid)

# 必要に応じて詳細なレスポンスを取得
details = specforge.check_validity(
    system="temperature_sensor",
    definition="always_in_bounds",
    return_details=True
)
print(details["status"]["tag"], details["param_situation"])

`check_equivalence(system, left, right, ...)`

システムの仮定のもとで、2つの仕様またはインライン式が論理的に同値かどうかを検査します。

主なパラメータ:

system (str): 両辺が解析されるコンテキストとなるシステム
left (str): 1つ目の仕様名またはインラインLilo式
right (str): 2つ目の仕様名またはインラインLilo式
timeout (int | float): タイムアウト秒数（デフォルト: 30）
return_details (bool): Trueの場合、ブール値の代わりに構造化された同値性検査のレスポンスを返します（デフォルト: False）

戻り値:

bool: 2つの対象が同値の場合はTrue、そうでない場合はFalse
return_details=Trueの場合、SpecForge APIから返された構造化された同値性検査の結果を返します。結果についてはresult["status"]["tag"]を、デフォルト値を持つパラメータの扱いについてはresult["param_situation"]を確認してください。

例:

# 2つの表現が一致することを検査
are_equivalent = specforge.check_equivalence(
    system="temperature_sensor",
    left="always_in_bounds",
    right="always (min_temperature <= temperature <= max_temperature)"
)
print(are_equivalent)

# インライン式を組み合わせて検査
are_equivalent = specforge.check_equivalence(
    system="temperature_sensor",
    left="x > 0 && y > 0",
    right="y > 0 && x > 0"
)
print(are_equivalent)

# 詳細なレスポンスを取得
details = specforge.check_equivalence(
    system="temperature_sensor",
    left="always_in_bounds",
    right="always (min_temperature <= temperature <= max_temperature)",
    return_details=True
)
print(details["status"]["tag"], details["param_situation"])

`exemplify(system, definition, ...)`

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

主なパラメータ:

system (str): 定義を含むシステム
definition (str): 例示する仕様の名前
assumptions (list): 生成を制約する追加の仮定（デフォルト: []）。各仮定は次の要素を持つ辞書です：
- "expression" (str): 生成時に仮定するLiloブール式（または既存のspec/defの名前）
- "rigidity" (str): "Hard"または"Soft"。厳格度レベルを参照してください
n_points (int): 生成するデータポイント数（デフォルト: 10）
params_file (str/Path): システムパラメータファイルのパス
params (dict): 辞書としての直接システムパラメータ
- 注意: params_fileまたはparamsのうち最大1つを指定してください
params_encoding (dict): パラメータのレコードエンコーディング
timeout (int): 例示のタイムアウト秒数（デフォルト: 30）
also_monitor (bool): 生成されたデータもモニタリングするかどうか（デフォルト: True）
at_beginning (bool): True（デフォルト）の場合、例示器は最初の時点ですでに仕様を満たすトレースを探索します。Falseの場合、生成されたトレースの後の時点で仕様が満たされてもかまいません。生成例が最初から仕様を満たすことを示したい場合はTrueが便利です。Falseにするとソルバーの自由度が増し、トレースの後の時点で自然に満たされるpastなどの時相演算子を仕様が含む場合に役立ちます
fix_defaults (bool): デフォルトはTrueです。Trueの場合、例示器はデフォルト値を持つパラメータをその値に固定します。Falseの場合、例示器はデフォルト値を無視し、パラメータを自由変数として扱います。詳細はパラメータをデフォルト値に固定するを参照してください
return_timeseries (bool): Trueの場合、DataFrameを返す。Falseの場合、JSONを表示（デフォルト: False）

厳格度レベル

各仮定には厳格度レベル（"Hard"または"Soft"）があり、ソルバーがその仮定を絶対に違反できない制約として扱うか、選好として扱うかを制御します。詳しくは例示と充足可能性を参照してください。

例:

# 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"},
        {"expression": "eventually (temperature > 30)", "rigidity": "Soft"}
    ],
    params={"min_temperature": 10.0, "max_temperature": 40.0},
    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
)

# トレースの後の時点で仕様を満たすことを許可（最初の時点で満たす必要はありません）
specforge.exemplify(
    system="temperature_sensor",
    definition="recovery_spec",
    n_points=20,
    at_beginning=False
)

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

`list_defs(system, specs_only=False)`

指定されたLiloシステム内のすべての定義を一覧表示します。

パラメータ:

system (str): 定義を一覧表示するLiloシステム
specs_only (bool): Trueの場合、他の定義を除き仕様のみを一覧表示します（デフォルト: False）

戻り値: strのlist - 定義名の一覧

例:

>>> specforgeClient.list_defs(system ='temperature_sensor', specs_only=True)
['temperature_in_bounds',
 'humidity_correlation',
 'emergency_condition',
 'recovery_spec',
 'always_in_bounds']

`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

Keyboard shortcuts

SpecForge ユーザーガイド