Search⌘ K
AI Features

Modeling the Circuit Breaker: The Property

Explore how to model and test a circuit breaker using state machine properties in Erlang. Understand the role of generators, state transitions, and preconditions in defining a property-based test model that captures realistic system behavior.

We'll cover the following...

The property

Let’s start by looking at the property.

Erlang
prop_test() ->
?FORALL(Cmds, proper_fsm:commands(?MODULE),
begin
{ok, Pid} = circuit_breaker:start_link(),
{History,State,Result} = proper_fsm:run_commands(?MODULE, Cmds),
gen_server:stop(Pid, normal, 5000), %(1)
?WHENFAIL(io:format("History: ~p\nState: ~p\nResult: ~p\n",
[History,State,Result]),
aggregate(zip(proper_fsm:state_names(History),
command_names(Cmds)),
Result =:= ok))
end).

There will be four generators:

  1. ok/1
  2. tripped/1
  3. blocked/1,
  4. unregistered/1
  • This generator is added because manual calls aren’t available until the circuit breaker’s service id is registered, and this occurs automatically on first use. This peculiarity will be encoded in the state machine itself.

Here we’ll begin the circuit breaker process by hand, which is paired with a call to gen_server:stop/3 at line 6. The circuit breaker module doesn’t expose a callback to terminate the breaker, usually preferring to let a supervision tree do that work. The gen_server behavior, however, exposes functions that let us ...