Spex.ImplModel (spex v0.1.0)

Represents the observed implementation model built from runtime transitions.

Summary

serialisation()

t()

Deserialises .spex content into an implementation model.

Creates an empty implementation model for a specification in learning mode.

Observes a transition and returns its status and resulting model.

Serialises an implementation model into .spex text format.

@type observation_status() ::
  :ok | :deviation_still_bisimilar | :deviation_not_bisimilar

@type serialisation() :: String.t()

@type t() :: %Spex.ImplModel{
  learning_mode?: boolean(),
  specification: Spex.Specification.t(),
  transitions: MapSet.t(Spex.transition())
}

@spec deserialise(serialisation()) ::
  {:ok, t()} | {:error, Spex.Errors.ImplModelError.t()}

Deserialises .spex content into an implementation model.

@spec initialise(Spex.Specification.t()) :: t()

Creates an empty implementation model for a specification in learning mode.

@spec observe_transition(t(), Spex.transition()) :: {observation_status(), t()}

Observes a transition and returns its status and resulting model.

In learning mode, the transition is added. Outside learning mode, the model is checked for bisimilarity impact without mutating stored transitions.

@spec serialise(t()) :: serialisation()

Serialises an implementation model into .spex text format.