QuintConnect.Step (quint_connect v0.1.0)

One replayable Quint step extracted from an ITF state.

Summary

t()

Returns true when this step represents an action.

Returns required nondeterministic pick by name.

Returns optional nondeterministic pick by name.

@type t() :: %QuintConnect.Step{
  action_taken: String.t(),
  nondet_picks: map(),
  state: term()
}

@spec action?(t(), String.t() | atom()) :: boolean()

Returns true when this step represents an action.

@spec nondet(t(), String.t() | atom()) :: {:ok, term()} | {:error, term()}

Returns required nondeterministic pick by name.

@spec optional_nondet(t(), String.t() | atom()) :: {:ok, term() | nil}

Returns optional nondeterministic pick by name.