QuintConnect.Driver behaviour (quint_connect v0.1.0)

Copy Markdown View Source

Behaviour for replaying a Quint trace step on your implementation.

A driver is an imperative shell around your implementation. step/2 receives a decoded QuintConnect.Step and returns the next implementation state.

Summary

Types

step()

Callbacks

config()

Optional default config for this driver.

init(opts)

Optional one-time setup before first step/2.

step(impl_state, step)

Apply one specification step to the implementation.

Types

step()

@type step() :: QuintConnect.Step.t()

Callbacks

config()

(optional) 
@callback config() :: QuintConnect.Config.t()

Optional default config for this driver.

init(opts)

(optional) 
@callback init(opts :: keyword()) :: {:ok, impl_state :: term()} | {:error, term()}

Optional one-time setup before first step/2.

step(impl_state, step)

@callback step(impl_state :: term(), step :: step()) :: {:ok, term()} | {:error, term()}

Apply one specification step to the implementation.