graph

Checking a specification, and projecting it onto each participant.

This is the step that makes repetition possible. Walking a specification assigns a state to each distinct continuation, and Loop binds its name to the state at its head, so Continue resolves to that state rather than expanding into it. What comes out is a finite graph with cycles in it. Nothing self-referential is produced, so nothing the Gleam compiler rejects as a type cycle is produced either.

Projection happens here too. A Message is a send for its sender, a receive for its recipient, and nothing at all for anybody else. A Choice is an internal choice for the participant making it, an external choice for the one being told, and for everybody else an obligation to behave the same way whichever arm was taken, since they are never told which.

Merging

That last case is the one worth understanding, because it is where a specification gets rejected for a reason that is not a typo.

spec.Choice(at: "Client", to: "Server", branches: [
  spec.Branch("buy", "Item", spec.Message("Server", "Bank", "charge", "Money", spec.End)),
  spec.Branch("browse", "Nil", spec.Message("Bank", "Server", "rate", "Money", spec.End)),
])

The bank is told nothing about the client’s decision, yet it has to send in one arm and receive in the other. There is no single thing the bank can do that is right either way, so this is rejected as Unmergeable. The fix is always the same: tell the bank, by routing the decision through it.

Views that differ only in what they are willing to receive do merge, because a participant offering more arms than it needs is not wrong. That is the standard full merge, and it is what makes most real protocols project at all.

What is checked

Everything in Error, but the ones that catch real mistakes are Unmergeable above, UnguardedRecursion for a loop that spins without anybody speaking, IdleLoop for a loop one participant sits out entirely and therefore cannot tell has gone round again, and UnmetRequirement for a contact point that demands a guarantee nothing established.

Types

Action

</>

What a participant does at a state.

pub type Action {
  Sends(to: String, label: String, payload: String, next: String)
  Receives(
    from: String,
    label: String,
    payload: String,
    next: String,
  )
  Selects(to: String, arms: List(Arm))
  Offers(from: String, arms: List(Arm))
  Done
}

Constructors

Sends(to: String, label: String, payload: String, next: String)

Transmit to to, then move on.

Receives(
  from: String,
  label: String,
  payload: String,
  next: String,
)

Accept from from, then move on.

```
Selects(to: String, arms: List(Arm))
```
Pick one arm and tell to which.
```
Offers(from: String, arms: List(Arm))
```
from picks, so every arm has to be handled.
```
Done
```
Nothing is owed in any direction.

Arm

</>

One arm of a choice, as seen by one participant.

pub type Arm {
  Arm(label: String, payload: String, next: String)
}

Constructors

Arm(label: String, payload: String, next: String)

Error

</>

Everything that stops a specification becoming a graph.

pub type Error {
  TooFewRoles(count: Int)
  DuplicateRole(role: String)
  UnknownRole(role: String, at: String)
  SelfAddressed(role: String, label: String)
  DegenerateChoice(at: String, arms: Int)
  AmbiguousArms(at: String, label: String)
  UnboundContinue(name: String)
  ShadowedLoop(name: String)
  UnguardedRecursion(name: String)
  IdleLoop(role: String, name: String)
  Unmergeable(role: String, states: List(String))
  DuplicateStateName(name: String)
  Uninvolved(role: String)
  UnmetRequirement(name: String)
  DuplicateAssertion(name: String)
  UnbalancedLoop(name: String, differing: List(String))
}

Constructors

```
TooFewRoles(count: Int)
```
Fewer than two participants is not a protocol.
```
DuplicateRole(role: String)
```
The same participant is named twice in roles.
```
UnknownRole(role: String, at: String)
```
A message or choice named a participant the protocol does not have.
```
SelfAddressed(role: String, label: String)
```
A message was addressed from a participant to itself.
```
DegenerateChoice(at: String, arms: Int)
```
A choice with fewer than two arms is not a choice.
```
AmbiguousArms(at: String, label: String)
```
Two arms of one choice share a label, so the participant being told cannot work out which was taken.
```
UnboundContinue(name: String)
```
Continue named a loop that is not in scope.
```
ShadowedLoop(name: String)
```
A loop nested inside a loop of the same name. Legal in principle, confusing in generated code, and never what was meant.
```
UnguardedRecursion(name: String)
```
A loop whose body can return to its head without anybody communicating, which is a spin rather than a protocol.
```
IdleLoop(role: String, name: String)
```
A loop one participant can sit out entirely, so it has no way of knowing the protocol has gone round again.
```
Unmergeable(role: String, states: List(String))
```
A participant’s view of a choice it is not told about differs between arms, so there is nothing it can do that is right either way.
```
DuplicateStateName(name: String)
```
Two different states were given the same name.
```
Uninvolved(role: String)
```
A participant that never communicates.
```
UnmetRequirement(name: String)
```
Require or Consume demanded a guarantee that nothing established, or that an earlier Consume already spent.
```
DuplicateAssertion(name: String)
```
The same guarantee asserted twice with the first still live.
```
UnbalancedLoop(name: String, differing: List(String))
```
A loop that ends holding different guarantees than it began with, so the second time round is not the same protocol as the first.

Graph

</>

One participant’s view of a protocol, flattened.

pub type Graph {
  Graph(role: String, initial: String, states: List(State))
}

Constructors

Graph(role: String, initial: String, states: List(State))

State

</>

A named position, and the one thing this participant does there.

pub type State {
  State(name: String, action: Action)
}

Constructors

```
State(name: String, action: Action)
```

Values

compile

</>

pub fn compile(
  protocol: spec.Protocol,
) -> Result(List(Graph), Error)

Check a protocol, then project it onto every participant.

Example

let assert Ok([customer, teller]) = graph.compile(atm())

describe

</>

pub fn describe(error: Error) -> String

Render an error as a line suitable for a terminal.

project

</>

pub fn project(
  protocol: spec.Protocol,
  role: String,
) -> Result(Graph, Error)

Project a protocol onto one participant.

Assumes the protocol is well formed, which compile checks first. Calling this directly on an unchecked protocol will report projection errors rather than the specification error that caused them.

state

</>

pub fn state(graph: Graph, name: String) -> Result(State, Nil)

Look a state up by name.

state_names

</>

pub fn state_names(graph: Graph) -> List(String)

The states of a graph, in declaration order. Useful for tests.

successors

</>

pub fn successors(state: State) -> List(String)

The states reachable in one step. Useful for traversal, and for checking that a graph refers only to states it has.

well_asserted

</>

pub fn well_asserted(
  node: spec.Spec,
  given given: List(String),
) -> Bool

Are this fragment’s contact points consistent with the guarantees already in scope?

The same check compile runs, exposed for a fragment rather than a whole protocol, because interleaving composition has to ask it repeatedly about pieces it is part way through assembling.

Example

// A payment that needs a code somebody else has to have issued.
let fragment = spec.Consume("tan", spec.Message("A", "B", "pay", "Money", spec.End))

assert graph.well_asserted(fragment, given: []) == False
assert graph.well_asserted(fragment, given: ["tan"]) == True