Metadata-Version: 2.4
Name: specforge_sdk
Version: 0.5.8
Summary: SpecForge SDK
Author-email: Imiron Developers <info@imiron.io>
Requires-Python: >=3.12
Description-Content-Type: text/markdown
Requires-Dist: requests<3.0.0,>=2.32.4
Requires-Dist: urllib3<3.0.0,>=2.5.0
Requires-Dist: pandas<3.0.0,>=2.3.1
Requires-Dist: ipython<10.0.0,>=9.4.0
Requires-Dist: tomli<3.0.0,>=2.0.0

# 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](setting-up-python-sdk.md) guide for instructions on installing and configuring the SDK in a Python environment.

## Quick Start

```python
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:**

```python
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:**

```python
# 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:**

```python
# 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:**

```python
# 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:**

```python
# 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:**

```python
# 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:**

```python
# 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](#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](./exemplification-and-satisfiability.md#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](./exemplification-and-satisfiability.md#rigidity-levels) for a full explanation.

**Examples:**

```python
# 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:**

```python
>>> 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:**

```python
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:**

```python
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`
