Hoare.Graph (hoare v0.3.0)

Copy Markdown View Source

The graph a list of transition modules declares: states as vertices, each transition an edge from every state it leaves to the one it reaches.

The list is explicit, kept wherever the record's transitions are known. Assert on edges/1 so a change to the graph is a deliberate diff, or paste to_mermaid/1 into the docs. leaving/2 and entering/2 ask a single state for its edges, so a test can name a sink (leaving/2 is empty) or an unreachable state (entering/2 is empty).

Summary

Types

edge()

Functions

edges(transitions)
entering(transitions, state)

The transitions that reach state.

leaving(transitions, state)

The transitions that leave state.

states(transitions)

The states the transitions name, in first-seen order.

to_mermaid(transitions)

A Mermaid stateDiagram-v2, modules labelled by their last segment.

Types

edge()

@type edge() :: {from :: module(), via :: module(), to :: module()}

Functions

edges(transitions)

@spec edges([module()]) :: [edge()]

entering(transitions, state)

@spec entering([module()], module()) :: [module()]

The transitions that reach state.

leaving(transitions, state)

@spec leaving([module()], module()) :: [module()]

The transitions that leave state.

states(transitions)

@spec states([module()]) :: [module()]

The states the transitions name, in first-seen order.

to_mermaid(transitions)

@spec to_mermaid([module()]) :: String.t()

A Mermaid stateDiagram-v2, modules labelled by their last segment.