Assumptions:

Guarantees:

Options:

Set the search strategy: linear (adds one state per step) or exponential (adds one latch per step)
Set the backend encoding: input-symbolic (QBF), explicit (SAT), SMT
Set the specification semantics: mealy (output may depend on current state and input) or moore (output may only depend on the current state).
A comma-separated list of input propositions.
A comma-separated list of output propositions.