Search⌘ K
AI Features

Modeling the Circuit Breaker: The Test Module

Explore how to model and test a circuit breaker module using finite state machine properties in PropEr. Learn to define preconditions, update state data, and validate postconditions to ensure correct behavior in complex Erlang systems.

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 =:=
...