QuintConnect.Config (quint_connect v0.1.0)

Options for Quint subprocess invocation and replay.

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

Types

path()

t()

Functions

default()

Default configuration, merging QUINT_VERBOSE and QUINT_SEED when set.

new(opts \\ [])

Builds a validated config from keyword options.

Types

path()

@type path() :: [String.t()]

t()

@type t() :: %QuintConnect.Config{
  backend: String.t() | nil,
  init_action: String.t(),
  main_module: String.t() | nil,
  max_samples: pos_integer() | nil,
  max_steps: pos_integer() | nil,
  mbt: boolean(),
  n_traces: pos_integer(),
  nondet_path: path(),
  quint_executable: String.t(),
  seed: String.t() | nil,
  state_path: path(),
  step_action: String.t(),
  test_name: String.t() | nil,
  verbosity: String.t() | integer() | nil
}

Functions

default()

@spec default() :: t()

Default configuration, merging QUINT_VERBOSE and QUINT_SEED when set.

new(opts \\ [])

@spec new(keyword()) :: {:ok, t()} | {:error, term()}

Builds a validated config from keyword options.