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
  • Satisfiability: Check whether a spec, inline expression, or whole system is satisfiable
  • Validity: Check whether a spec or expression is provable under the system’s assumptions
  • Equivalence: Check whether two specs or expressions are logically equivalent
  • 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 | None): Name of the spec to monitor. If None, monitors all specs in the system at once (system-wide monitoring).
  • 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)
  • partial_data (bool): Allow monitoring even when the data does not cover all signals declared in the system (default: True). When enabled, signals that are missing from the data are treated as unknown rather than causing an error. Set to False to require that the data provides values for every signal.
  • return_timeseries (bool): If True, return DataFrame; if False, display JSON (default: False)

When definition=None, the monitor evaluates every spec in the system against the provided data and returns a combined result. This is useful for getting a quick overview of which specs pass and which fail across the entire system.

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
  • params_file (str/Path): Path to a JSON file containing system parameter values
  • params (dict): Direct system parameters as a dictionary
    • Note: Provide at most one of params_file or params
  • 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
)

# Animate with system parameters
specforge.animate(
    system="temperature_sensor",
    svg_file="temp.svg",
    data_file="sensor_data.csv",
    params={"temp_threshold": 25.0}
)

# Animate with parameters from file
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, ...)

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)
    • Use one of EXPORT_LILO, EXPORT_JSON, or EXPORT_RTAMT defined in the library
  • 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
)

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

Check satisfiability of a single spec, an inline expression, or the whole system.

Key Parameters:

  • system (str): The system containing the definition(s)
  • definition (str | None): Name of the spec to check
  • expression (str | None): Inline Lilo boolean expression to check in the given system context
    • Note: Provide at most one of definition or expression
  • If both definition and expression are None, the SDK checks the whole system
  • timeout (int | float): Timeout in seconds for the satisfiability query (default: 30)
  • return_details (bool): If True, return the structured satisfiability response instead of a bool (default: False)

Returns:

  • bool: True when satisfiable, False otherwise.

  • If return_details=True, returns a dictionary with two keys:

    • "status": The satisfiability outcome. Check result["status"]["tag"] for one of:
      • "Consistent" – the spec is satisfiable.
      • "InConsistent" – the spec is unsatisfiable. The "contents" field contains an UnsatInfo object with details about the unsat core.
      • "Unknown" – the solver could not determine satisfiability.
      • "TimedOut" – the solver timed out. The "contents" field contains the timeout duration in microseconds.
    • "param_situation": Describes how system parameters (param declarations) were handled during the check:
      • "UsingDefaults" – the solver fixed all parameters to their declared default values and found the result with those defaults. This is the first strategy attempted.
      • "UnfixedParams" – the solver left all parameters free (unconstrained). This happens when the check with default values did not yield a "Consistent" result, so the solver retried with parameters as free variables.

    The meaningful combinations of status and param_situation are:

    • ("Consistent", "UsingDefaults") – the spec is satisfiable when the parameters are fixed to their declared defaults.
    • ("Consistent", "UnfixedParams") – the spec is satisfiable, but not when the parameters are fixed to their declared defaults.
    • ("InConsistent", "UnfixedParams") – for all possible values of the parameters, the spec remains unsatisfiable.

Examples:

# Check a single spec
is_satisfiable = specforge.check_satisfiability(
    system="temperature_sensor",
    definition="always_in_bounds"
)
print(is_satisfiable)

# Get the detailed response to inspect the param situation
details = specforge.check_satisfiability(
    system="temperature_sensor",
    definition="always_in_bounds",
    return_details=True
)
print(details["status"]["tag"])        # e.g. "Consistent"
print(details["param_situation"])      # e.g. "UsingDefaults" or "UnfixedParams"

# Check the whole system as a bool
system_is_satisfiable = specforge.check_satisfiability(
    system="temperature_sensor"
)
print(system_is_satisfiable)

# Check an inline expression in the system context
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, ...)

Check validity of a single spec or an inline expression under the system’s assumptions.

Key Parameters:

  • system (str): The system containing the definition or in whose context the expression is parsed
  • definition (str | None): Name of the spec to prove
  • expression (str | None): Inline Lilo boolean expression to prove in the given system context
    • Note: Provide exactly one of definition or expression
  • timeout (int | float): Timeout in seconds for the validity query (default: 30)
  • return_details (bool): If True, return the structured validity response instead of a bool (default: False)

Returns:

  • bool: True when the target is valid, False otherwise.
  • If return_details=True, returns the structured validity result from the SpecForge API. Check result["status"]["tag"] for the outcome and result["param_situation"] for how defaulted parameters were handled.

Examples:

# Check a single spec
is_valid = specforge.check_validity(
    system="temperature_sensor",
    definition="always_in_bounds"
)
print(is_valid)

# Check an inline expression in the system context
expr_is_valid = specforge.check_validity(
    system="temperature_sensor",
    expression="always (min_temperature <= temperature <= max_temperature)"
)
print(expr_is_valid)

# Get the detailed response when you need it
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, ...)

Check whether two specs or inline expressions are logically equivalent under the system’s assumptions.

Key Parameters:

  • system (str): The system in whose context both sides are parsed
  • left (str): First spec name or inline Lilo expression
  • right (str): Second spec name or inline Lilo expression
  • timeout (int | float): Timeout in seconds (default: 30)
  • return_details (bool): If True, return the structured equivalence response instead of a bool (default: False)

Returns:

  • bool: True when the two targets are equivalent, False otherwise.
  • If return_details=True, returns the structured equivalence result from the SpecForge API. Check result["status"]["tag"] for the outcome and result["param_situation"] for how defaulted parameters were handled.

Examples:

# Check that two formulations agree
are_equivalent = specforge.check_equivalence(
    system="temperature_sensor",
    left="always_in_bounds",
    right="always (min_temperature <= temperature <= max_temperature)"
)
print(are_equivalent)

# Mix of inline expressions
are_equivalent = specforge.check_equivalence(
    system="temperature_sensor",
    left="x > 0 && y > 0",
    right="y > 0 && x > 0"
)
print(are_equivalent)

# Get the detailed response
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, ...)

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: []). Each assumption is a dictionary with:
    • "expression" (str): A Lilo boolean expression (or the name of an existing spec/def) to assume during generation.
    • "rigidity" (str): Either "Hard" or "Soft". See Rigidity Levels below.
  • 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: True)
  • at_beginning (bool): If True (the default), the exemplifier searches for a trace whose first time point already satisfies the spec. If False, the spec may only become satisfied at a later point in the generated trace. Setting this to True is useful when you want the generated example to demonstrate satisfaction from the start; setting it to False gives the solver more freedom and can help when the spec involves temporal operators like past that are naturally satisfied later in the trace.
  • fix_defaults (bool): Defaults to True. When True, the exemplifier is forced to fix any params with default values to those defaults. When False, the exemplifier ignores default values and treats params as free variables. See Fixing Params to Default Values for more details.
  • return_timeseries (bool): If True, return DataFrame; if False, display JSON (default: False)

Rigidity Levels

Each assumption has a rigidity level ("Hard" or "Soft") that controls whether the solver treats it as an inviolable constraint or a preference. See Exemplification and Satisfiability for a full explanation.

Examples:

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

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

# Mix hard and soft assumptions
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
)

# 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
)

# Allow the spec to be satisfied later in the trace (not necessarily at the first point)
specforge.exemplify(
    system="temperature_sensor",
    definition="recovery_spec",
    n_points=20,
    at_beginning=False
)

# 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
)

list_defs(system, specs_only=False)

List all the definitions in the given lilo system.

Parameters:

  • system (str): The lilo system to list definitions from
  • specs_only (bool): If True, only list specifications, not other definitions (default: False)

Returns: list of str - List of definition names

Example:

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

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