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

The SpecForge python SDK is used for interacting with the SpecForge API, enabling formal specification monitoring, animation, export, and exemplification.

Refer to the Setting up the Python SDK guide for instructions on installing and configuring the SDK in a Python environment.

Quick Start

from specforge_sdk import SpecForgeClient

# Initialize client
specforge = SpecForgeClient(base_url="http://localhost:8080")

# Check API health
if specforge.health_check():
    print("✓ Connected to SpecForge API")
    print(f"API Version: {specforge.version()}")
else:
    print("✗ Cannot connect to SpecForge API")

Core Features

The SDK provides access to core SpecForge capabilities:

  • Monitoring: Check specifications against data
  • Animation: Create visualizations over time
  • Export: Convert specifications to different formats
  • Exemplification: Generate example data that satisfies specifications

Documentation

See the comprehensive demo notebook at sample-project/demo.ipynb for:

  • Detailed usage examples
  • Jupyter notebook integration
  • Custom rendering features

API Methods

SpecForgeClient(base_url, ...)

Initialize a SpecForge API client.

Parameters:

  • base_url (str): The base URL of the SpecForge API server (default: "http://localhost:8080")
  • project_dir (str/Path): Optional project directory path; if not provided, searches up from current directory for lilo.toml
  • timeout (int): Request timeout in seconds (default: 30)
  • check_version (bool): Whether to check for version mismatches on initialization (default: True)

Example:

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

monitor(system, definition, ...)

Monitor a specification against data. Returns analysis results with verdicts and optional robustness metrics.

Key Parameters:

  • system (str): The system containing the definition
  • definition (str): Name of the spec to monitor
  • data_file (str/Path): Path to data file (CSV, JSON, or JSONL)
  • data (list/DataFrame): Direct data as list of dicts or pandas DataFrame
    • Note: Provide exactly one of data_file or data
  • params_file (str/Path): Path to system parameters file
  • params (dict): Direct system parameters as dictionary
    • Note: Provide at most one of params_file or params
  • encoding (dict): Record encoding configuration
  • verdicts (bool): Include verdict information (default: True)
  • robustness (bool): Include robustness analysis (default: False)
  • return_timeseries (bool): If True, return DataFrame; if False, display JSON (default: False)

Examples:

# Monitor with data file and params file
specforge.monitor(
    system="temperature_sensor",
    definition="always_in_bounds",
    data_file="sensor_data.csv",
    params_file="temperature_config.json"
)

# Monitor with data file and params dict
specforge.monitor(
    system="temperature_sensor",
    definition="always_in_bounds",
    data_file="sensor_data.csv",
    params={"min_temperature": 10.0, "max_temperature": 24.0}
)

# Monitor with DataFrame and get results as 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
)

# Monitor with robustness analysis
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, ...)

Create an animation from specification, data, and SVG template.

Key Parameters:

  • system (str): The system containing the animation definition
  • svg_file (str/Path): Path to the SVG template file
  • data_file (str/Path): Path to data file
  • data (list/DataFrame): Direct data as list of dicts or pandas DataFrame
    • Note: Provide exactly one of data_file or data
  • encoding (dict): Record encoding configuration
  • return_gif (bool): If True, returns base64-encoded GIF string (default: False)
  • save_gif (str/Path): Optional path to save the GIF file

Examples:

# Display animation frames in Jupyter
specforge.animate(
    system="temperature_sensor",
    svg_file="temp.svg",
    data_file="sensor_data.csv"
)

# Save animation as GIF file
specforge.animate(
    system="scene",
    svg_file="scene.svg",
    data_file="scene.json",
    save_gif="output.gif"
)

# Get GIF data as base64 string
gif_data = specforge.animate(
    system="temperature_sensor",
    svg_file="temp.svg",
    data=synthetic_df,
    encoding=nested_encoding(),
    return_gif=True
)

export(system, definition, ...)

Export a specification to different formats (e.g., LILO format).

Key Parameters:

  • system (str): The system containing the definition
  • definition (str): Name of the spec to export
  • export_type (dict): Export format configuration (defaults to LILO)
  • params_file (str/Path): Path to system parameters file
  • params (dict): Direct system parameters as dictionary
    • Note: Provide at most one of params_file or params
  • encoding (dict): Record encoding configuration
  • return_string (bool): If True, return exported string; if False, display JSON (default: False)

Examples:

# Export to LILO format as string
lilo_result = specforge.export(
    system="temperature_sensor",
    definition="always_in_bounds",
    export_type=EXPORT_LILO,
    return_string=True
)
print(lilo_result)

# Export with params file
export_result = specforge.export(
    system="temperature_sensor",
    definition="always_in_bounds",
    export_type=EXPORT_LILO,
    params_file="temperature_config.json",
    return_string=True
)

# Export with params dict
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
)

# Export to JSON format (display in Jupyter)
specforge.export(
    system="temperature_sensor",
    definition="humidity_correlation",
    export_type=EXPORT_JSON
)

exemplify(system, definition, ...)

Generate example data that satisfies a specification.

Key Parameters:

  • system (str): The system containing the definition
  • definition (str): Name of the spec to exemplify
  • assumptions (list): Additional assumptions to constrain generation (default: [])
  • n_points (int): Number of data points to generate (default: 10)
  • params_file (str/Path): Path to system parameters file
  • params (dict): Direct system parameters as dictionary
    • Note: Provide at most one of params_file or params
  • params_encoding (dict): Record encoding for the parameters
  • timeout (int): Timeout in seconds for exemplification (default: 30)
  • also_monitor (bool): Whether to also monitor the generated data (default: False)
  • return_timeseries (bool): If True, return DataFrame; if False, display JSON (default: False)

Examples:

# Generate an example with 20 samples
specforge.exemplify(
    system="temperature_sensor",
    definition="always_in_bounds",
    n_points=20
)

# Generate example with assumptions
humidity_assumption = {
    "expression": "eventually (humidity > 25)",
    "rigidity": "Hard"
}
specforge.exemplify(
    system="temperature_sensor",
    definition="humidity_correlation",
    assumptions=[humidity_assumption],
    n_points=20
)

# Generate example with partial params (solver fills in missing values)
specforge.exemplify(
    system="temperature_sensor",
    definition="humidity_correlation",
    assumptions=[{"expression": "always_in_bounds", "rigidity": "Hard"}],
    params={"min_temperature": 38.0},
    n_points=20
)

# Generate example and get as DataFrame
example_df = specforge.exemplify(
    system="temperature_sensor",
    definition="temperature_in_bounds",
    n_points=15,
    also_monitor=False,
    return_timeseries=True
)

health_check()

Check if the SpecForge API is available and responding.

Returns: bool - True if API is healthy, False otherwise

Example:

if specforge.health_check():
    print("✓ Connected to SpecForge API")
else:
    print("✗ Cannot connect to SpecForge API")

version()

Get the API server version and SDK version.

Returns: dict with keys "api" and "sdk"

Example:

versions = specforge.version()
print(f"API Version: {versions['api']}")
print(f"SDK Version: {versions['sdk']}")

File Format Support

  • Specifications: .lilo files
  • Data: .csv, .json, .jsonl files
  • Visualizations: .svg files

Requirements

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