Function synthesize_from_ltl 

pub fn synthesize_from_ltl(
    spec: &VerifyExpr,
    inputs: &[SignalDecl],
    outputs: &[SignalDecl],
) -> SynthesisResult

Synthesize a controller from an LTL specification.

For safety specs: finds a memoryless strategy via Z3. For response specs: finds a bounded-state controller. For contradictory specs: returns Unrealizable.