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 under the current state.
precondition(unregistered, ok, _, {call, _, Call, _}) ->
    Call =:= success;
precondition(ok, To, #data{errors=N, limit=L}, {call,_,err,_}) ->
    (To =:= tripped andalso N+1 =:= L) orelse (To =:= ok andalso N+1 =/= L);
precondition(ok, To, #data{timeouts=N, limit=L}, {call,_,timeout,_}) ->
    (To =:= tripped andalso N+1 =:= L) orelse (To =:= ok andalso N+1 =/= L);
precondition(_From, _To, _Data, _Call) ->
    true.

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

• (To =:= tripped andalso 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 andalso N+1 =/= L) means that 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.
next_state_data(ok, _To, Data=#data{errors=N}, _Res, {call,_,err,_}) ->
    Data#data{errors=N+1};
next_state_data(ok, _To, Data=#data{timeouts=N}, _Res, {call,_,timeout,_}) ->
    Data#data{timeouts=N+1};
next_state_data(_From, _To, Data, _Res, {call,_,manual_deblock,_}) ->
    Data#data{errors=0, timeouts=0};
next_state_data(_From, _To, Data, _Res, {call,_,manual_reset,_}) ->
    Data#data{errors=0, timeouts=0};
next_state_data(_From, _To, Data, _Res, {call, _Mod, _Fun, _Args}) ->
    Data.

Error and timeout calls both increment their count by 1, and deblocking and resetting turn them 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.