Utilities

Spot Formulas

class iglsynth.util.spot.formula(str)

substitute(formula, new_formula, *args)

Substitutes a sub-formula in spot.formula with another spot.formula.

Parameters:

• formula – (spot.formula) Spot formula to be replaced.
• new_formula – (spot.formula) Spot formula with which the ‘formula’ should be replaced with.

translate(*args, dict=<spot.impl.bdd_dict; proxy of <Swig Object of type 'std::shared_ptr< spot::bdd_dict > *'> >, xargs=None)

Translate a formula into an automaton.

Keep in mind that ‘Deterministic’ expresses just a preference that may not be satisfied.

The optional arguments should be strings among the following: - at most one in ‘TGBA’, ‘BA’, or ‘Monitor’, ‘generic’,

‘parity’, ‘parity min odd’, ‘parity min even’, ‘parity max odd’, ‘parity max even’ (type of automaton to build), ‘coBuchi’

• at most one in ‘Small’, ‘Deterministic’, ‘Any’ (preferred characteristics of the produced automaton)
• at most one in ‘Low’, ‘Medium’, ‘High’ (optimization level)
• any combination of ‘Complete’, ‘Unambiguous’, ‘StateBasedAcceptance’ (or ‘SBAcc’ for short), and ‘Colored’ (only for parity acceptance)

The default corresponds to ‘tgba’, ‘small’ and ‘high’.

Additional options can be supplied using a spot.option_map, or a string (that will be converted to spot.option_map), as the xargs argument. This is similar to the -x option of command-line tools; so check out the spot-x(7) man page for details.