Options for Quint subprocess invocation, replay, and verification.
state_path narrows the comparable state. nondet_path points at a sum-type
action record when a spec does not use Quint's built-in MBT metadata.
Summary
Functions
Default configuration, merging QUINT_VERBOSE and QUINT_SEED when set.
Builds a validated config from keyword options.
Types
@type path() :: [String.t()]
@type t() :: %QuintConnect.Config{ apalache_config: String.t() | nil, apalache_version: String.t() | nil, backend: String.t() | nil, hide: [String.t()], inductive_invariant: String.t() | nil, init_action: String.t(), invariant: String.t() | nil, invariants: [String.t()], main_module: String.t() | nil, max_samples: pos_integer() | nil, max_steps: pos_integer() | nil, mbt: boolean(), n_threads: pos_integer() | nil, n_traces: pos_integer(), nondet_path: path(), quint_executable: String.t(), random_transitions: boolean(), seed: String.t() | nil, server_endpoint: String.t() | nil, state_path: path(), step_action: String.t(), temporal: String.t() | nil, test_name: String.t() | nil, tlc_config: String.t() | nil, verbosity: String.t() | integer() | nil, witnesses: [String.t()] }