Return Moore transducer if formula is realizable.

Variable dicts have variable names as keys and their type as value. The types should be 'boolean'. These parameters are only used if formula is of type str. Else, the variable dictionaries associated with the LTL or GRSpec object are used.

Parameters:

• formula (str, LTL, or GRSpec) - linear temporal logic formula
• env_vars (dict or None) - uncontrolled variables (inputs); used only if formula is of type str
• sys_vars (dict or None) - controlled variables (outputs); used only if formula is of type str

Returns: MooreMachine

symbolic Moore transducer (guards are conjunctions, not sets)

Return Moore transducer from Lily strategy graph g.

Caution

The resulting transducer is symboic, in that the guards denote conjunctions, *not* subsets of ports.

Parameters:

• g (networkx.MultiDiGraph) - Moore strategy game graph as output by Lily

Returns: MooreMachine