rx/flow_model

Types

Command

pub type Command {
  Start(Int)
  Emit(Int)
  CancelActive(Int)
  Fail
  Drain
}

Constructors

```
Start(Int)
```
```
Emit(Int)
```
```
CancelActive(Int)
```
```
Fail
```
```
Drain
```

Event

</>

pub type Event {
  Enqueue
  CompleteSuccess(Int)
  CompleteFailure(Int)
  FinishInput
  Cancel
}

Constructors

```
Enqueue
```
```
CompleteSuccess(Int)
```
```
CompleteFailure(Int)
```
```
FinishInput
```
```
Cancel
```

Order

</>

Pure reference model for the asynchronous flattening state machine.

The production runtime stores typed start/deliver/cancel closures. This model intentionally stores only sequence numbers, making it deterministic and easy to exhaustively explore without BEAM timing or callback effects.

pub type Order {
  CompletionOrder
  InputOrder
}

Constructors

```
CompletionOrder
```
```
InputOrder
```

State

</>

pub type State {
  State(
    concurrency: Int,
    order: Order,
    next_sequence: Int,
    next_emit: Int,
    pending: List(Int),
    active: List(Int),
    completed: List(Int),
    input_done: Bool,
    status: Status,
  )
}

Constructors

State(
  concurrency: Int,
  order: Order,
  next_sequence: Int,
  next_emit: Int,
  pending: List(Int),
  active: List(Int),
  completed: List(Int),
  input_done: Bool,
  status: Status,
)

Status

</>

pub type Status {
  Running
  Failed
  Cancelled
  Drained
}

Constructors

```
Running
```
```
Failed
```
```
Cancelled
```
```
Drained
```

Values

invariants_hold

</>

pub fn invariants_hold(state: State) -> Bool

new

</>

pub fn new(concurrency: Int, order: Order) -> State

transition

</>

pub fn transition(
  state: State,
  event: Event,
) -> #(State, List(Command))