Package solvers

Class StrixHelper

  • public class StrixHelper
extends Object
    Bridge to the external Strix reactive-synthesis tool, used by AuRUS to check the realisability of a candidate specification — the status(S') component of the fitness function.

    Every checkRealizability/executeStrix overload does the same three things: (1) turn the specification into the plain-text arguments Strix expects, (2) launch Strix as an external process — either the native binary or, when Settings.USE_DOCKER is set, the run-docker-strix.sh/run-docker-spectra.sh wrapper — and (3) parse its stdout for the REALIZABLE verdict, enforcing Settings.STRIX_TIMEOUT. The two input formats supported — TLSF/LTL and Spectra — are dispatched on Settings.USE_SPECTRA.

    Which path actually runs by default (no Docker, no Spectra). The TLSF specification is not shelled out to syfco for translation. Instead, checkRealizability(Tlsf) simplifies the formula in Java (SyntacticSimplifier), renders it to Strix's LTL syntax (SolverUtils.toSolverSyntax), extracts the input/output signal lists, and calls the 3-argument executeStrix(String, String, String), which invokes lib/new_strix/strix directly.

    Pluggable synthesiser (Docker-free alternative). Setting Settings.SYNTH_TOOL = "ltlsynt" (flag -synth=ltlsynt) makes executeStrix(String, String, String) — used by both the TLSF and Spectra realisability checks — dispatch to ltlsynt instead of Strix, a tool installable directly (e.g. brew install spot on macOS, or conda install -c conda-forge spot on Linux/macOS — see spot.lre.epita.fr/install.html for a Debian/Ubuntu package repository), with no Docker and no architecture-specific vendored binary.

    Author:
    Matías Brizzio
    See Also:
    Settings, AutomataBasedModelCountingSpecificationFitness.compute_status(geneticalgorithm.SpecificationChromosome)

    • Constructor Detail

      • StrixHelper

        public StrixHelper()

    • Method Detail

      • checkRealizability

        public static StrixHelper.RealizabilitySolverResult checkRealizability​(owl.ltl.tlsf.Tlsf tlsf)
                                                                throws IOException,
                                                                       InterruptedException
        Checks the realisability of a parsed TLSF specification.

        When Settings.USE_SPECTRA is set, the specification is first converted to Spectra syntax (TlsfUtils.tlsf2spectra) and written to a .spectra file under Settings.SPECTRA_PATH, then checked via executeStrix(String). Otherwise the formula is simplified and rendered to Strix's LTL syntax directly in Java, and checked via executeStrix(String, String, String), which internally dispatches on Settings.SYNTH_TOOL (Strix, or the Docker-free ltlsynt alternative) — see that method's documentation.

        Parameters:
        tlsf - the specification to check
        Returns:
        the realisability verdict
        Throws:
        IOException - if launching Strix fails
        InterruptedException - if the Strix process is interrupted

      • executeStrix

        public static StrixHelper.RealizabilitySolverResult executeStrix​(String formula,
                                                                 String ins,
                                                                 String outs)
                                                          throws IOException,
                                                                 InterruptedException
        Runs the configured realisability/synthesis tool (Settings.SYNTH_TOOL, flag -synth) on an LTL formula plus explicit input/output signal lists, and returns its verdict.

        Only the command line differs per tool; everything else — timeout handling, stdout/stderr scanning, resource cleanup — is shared:

        • strix (default): the native lib/new_strix/strix binary, or ./run-docker-strix.sh when Settings.USE_DOCKER is set. Empty signal lists are passed as the literal "" Strix's argument parser expects.
        • ltlsynt (flag -synth=ltlsynt): a Docker-free alternative from the Spot library, installable via brew install spot (macOS) or conda install -c conda-forge spot — see spot.lre.epita.fr/install.html for Debian/Ubuntu packages. Resolved from PATH unless Settings.SYNTH_BIN overrides it. Invoked with --realizability, which suppresses controller synthesis.

        Both tools print a bare REALIZABLE/UNREALIZABLE line as their realisability verdict, so a single stdout scan covers both. A verdict found on stdout takes precedence over incidental stderr output — stderr only downgrades the result to StrixHelper.RealizabilitySolverResult.ERROR when no verdict was found on stdout, so a tool that writes harmless notices to stderr on a successful run is not misread as having failed.

        Parameters:
        formula - the specification's formula, in Strix/Spot LTL syntax
        ins - comma-separated list of input signal names (empty string if none)
        outs - comma-separated list of output signal names (empty string if none)
        Returns:
        the realisability verdict
        Throws:
        IOException - if launching the tool fails (e.g. not installed)
        InterruptedException - if the process is interrupted while waiting