Modeling the Circuit Breaker: The Test Module

The preconditions

Let’s start off by taking a look at the preconditions.

### Picks whether a command should be valid
def precondition(:unregistered, :ok, _, {:call, _, call, _}) do
  call == :success
end
def precondition(:ok, to, %{errors: n, limit: l}, {:call, _, :err, _}) do
  (to == :tripped and n + 1 == l) or (to == :ok and n + 1 != l)
end
def precondition(
      :ok,
      to,
      %{timeouts: n, limit: l},
      {:call, _, :timeout, _}
    ) do
  (to == :tripped and n + 1 == l) or (to == :ok and n + 1 != l)
end
def precondition(_from, _to, _data, _call) do
  true
end

Notice how both calls to erroneous cases are only valid in mutually exclusive instances:

• (to == :tripped and n + 1 == l) means that the switch to the tripped state can happen if the next failure (the one being generated) brings the total to the limit l.
• (to == :ok and n + 1 != l) means our state machine can only transition to the ok state if this new failure does not reach the limit.

All other calls are valid, since they only transition from one possible source state to one possible target state, and the circuit breaker requires no other special cases. Using an FSM property simplified this filtering drastically compared to what we’d have with a regular stateful property.

Next, we need to perform the data changes after each command.

The next_state_data

For the data changes after each command, we mostly have to worry about error accounting. Let’s take a look at how it’s done:

### Assuming the postcondition for a call was true, update the model
### accordingly for the test to proceed
def next_state_data(:ok, _, data = %{errors: n}, _, {_, _, :err, _}) do
  %{data | errors: n + 1} 
end
def next_state_data(:ok, _, d = %{timeouts: n}, _, {_, _, :timeout, _}) do 
  %{d | timeouts: n + 1}
end
def next_state_data(_from, _to, data, _, {_, _, :manual_deblock, _}) do
  %{data | errors: 0, timeouts: 0} 
end
def next_state_data(_from, _to, data, _, {_, _, :manual_reset, _}) do 
  %{data | errors: 0, timeouts: 0}
end
def next_state_data(_from, _to, data, _res, {:call, _m, _f, _args}) do
  data
end

Error and timeout calls both increment their count by 1, and deblocking and resetting them move back to 0. Everything else should have no impact on the data we track.

The postcondition

Finally, we have the postcondition. This one is slightly trickier.