Syntheos is a tool for checking the realizability of specifications expressed in Linear Temporal Logic with theories (LTLt). The atomic propositions in the specification are Z3 predicates, which can refer to the previous value of a quantitative variable x with y(x).

To install Syntheos, clone this repository and install it (in editable mode, so changes to the source take effect immediately) into a virtual environment:

 git clone https://github.com/imdea-software/syntheos.git
 cd syntheos
 python3 -m venv .venv
 source .venv/bin/activate
 python3 -m pip install -e .

This installs the syntheos and syntheos-shield console commands, along with the pinned dependencies declared in pyproject.toml.

Additionally, ensure that the Strix tool is in the same folder as Syntheos, as it is required for execution (or pass --strix-bin <path> / put strix on your PATH).

To check the realizability of an LTL specification, activate the virtual environment, then run:

syntheos --yaml <yaml_file>

(equivalently, without installing the package: python3 syntheos.py --yaml <yaml_file>, run from the repository root)

Remember to activate the virtual environment with:

 source .venv/bin/activate

when you start a new session.

The YAML file should contain:

• property: The LTLt specification, where the z3 expressions are enclosed in square brackets.
• variables: A list of variables, each specifying its name, type, and owner (either system or environment).

property: "XXG([x>y(y(x))])"
variables:
  - name: "x"
    type: "Int"
    owner: "system"

Given a YAML file spec.yaml:

syntheos --yaml spec.yaml

Will check the realizability of the specificaiton in spec.yaml. If the --yaml flag is not provided, the specification will be read from standard input in YAML format.

You can provide a filename to save the mealy machine in case the specification is realizable with the flag --save-mealy and a filename. The output file will also be a YAML.

syntheos --save-mealy controller.yaml --yaml spec.yaml

• Python 3.13
• Strix (must be placed in the same folder as Syntheos)

You can build and run a Docker image of Syntheos using Podman:

Build the image with tag syntheos using:

podman build --platform linux/amd64 -t syntheos .

You can run the image and provide the content of a YAML specification file via standard input:

podman run --platform linux/amd64 -i syntheos < spec.yaml

You can execute a controller that interprets the mealy machine that has been saved with --save-mealy controller.yaml with the syntheos-shield command (or python shield.py if you haven't installed the package).

syntheos-shield --mealy controller.yaml

This controller will read lines from stdin, where each line is a list of two elements.

The first element is a dictionary that maps each input variable to a concrete value. This represents the values provided by the environment at a specific time step.

The second element is a dictionary that maps output variables to proposed values determined by the system. This entry can contain only a subset of the system variables, indicating that the rest can be any value that the controller finds suitable.

If the proposed output values do not constitute a valid system response, the shield will provide a safe move to play instead.

python3 -m pip install -e ".[dev]"
python3 -m pytest

The unit tests (tests/unit/) don't need Strix. The regression suite (tests/integration/) replays a fixed set of specifications through the real Strix backend and checks the realizability verdict against a recorded baseline (tests/golden/baseline.json); it's automatically skipped if the strix binary isn't present, and takes a few minutes since it runs ~60 full CEGAR loops.

The syntheos package (not tests/) is fully type-annotated and checked with mypy:

python3 -m pip install -e ".[dev]"
python3 -m mypy

z3, ply and sympy ship no type stubs; syntheos/z3_support.py is the one module that imports z3 names directly (everything else reaches Z3 through mnz3.X), and z3/ply/sympy are configured as ignore_missing_imports in pyproject.toml so the rest of the codebase can still be held to disallow_untyped_defs.