passing config eqc tests

src/rafter.erl

@@ -32,8 +32,7 @@ get_leader(Peer) ->
 test() ->
     application:start(lager),
     application:start(rafter),
-    [rafter:start_node(P, rafter_sm_echo) || P <- [a, b, c]],
-    rafter:set_config(a, [a, b, c, d, e]).
+    [rafter:start_node(P, rafter_sm_echo) || P <- [a, b, c, d, e]].
 
 start_cluster() ->
     application:start(lager),

src/rafter_consensus_fsm.erl

@@ -165,14 +165,21 @@ follower(#append_entries{term=Term, from=From, prev_log_index=PrevLogIndex,
 %% entry in every log.
 follower({set_config, {Id, NewServers}}, From, 
           #state{me=Me, followers=F, config=#config{state=blank}=C}=State) ->
-    {Followers, Config} = reconfig(Me, F, C, NewServers, State),
-    NewState = State#state{config=Config, followers=Followers,
-                           init_config=[Id, From]},
-    %% Transition to candidate state. Once we are elected leader we will
-    %% send the config to the other machines. We have to do it this way so that the entry we log
-    %% will have a valid term and can be committed without a noop.
-    %% Note that all other configs must be blank on the other machines.
-    {next_state, candidate, NewState, 0};
+    case rafter_config:has_vote(Me, C) of
+        true ->
+            {Followers, Config} = reconfig(Me, F, C, NewServers, State),
+            NewState = State#state{config=Config, followers=Followers,
+                                   init_config=[Id, From]},
+            %% Transition to candidate state. Once we are elected leader we will
+            %% send the config to the other machines. We have to do it this way
+            %% so that the entry we log  will have a valid term and can be 
+            %% committed without a noop.  Note that all other configs must 
+            %% be blank on the other machines.
+            {next_state, candidate, NewState, 0};
+        false ->
+            Error = {error, not_consensus_group_member},
+            {reply, Error, follower, State, ?timeout()}
+    end;
 follower({set_config, _}, _From, #state{leader=Leader}=State) ->
     Reply = {error, {redirect, Leader}},
     {reply, Reply, follower, State, ?timeout()};

test/rafter_config_eqc.erl

@@ -59,38 +59,22 @@ cleanup(_) ->
 
 initial_state() ->
     #state{running = [a, b, c, d, e],
-           config = #config{state=blank}}.
+           config = blank}.
 
 command(_S) ->
     oneof([{call, rafter, set_config, [server(), servers()]}]).
 
+%% Ensure the peer we are talking to is at least running. If there is no config
+%% yet then it should also be a member of the group it's trying to create.
+precondition(#state{running=Running, config=blank}, 
+             {call, rafter, set_config, [Peer, NewServers]}) ->
+    lists:member(Peer, Running) andalso lists:member(Peer, NewServers);
 
-%% There is no point of talking to a node that isn't running. That would be user error.
-%% The peer we want to talk to should either be a member of the current consensus
-%% group or the config is blank and the peer is part of the new config.
-precondition(#state{running=Running, config=C}, {call, rafter, set_config, [Peer, NewServers]}) ->
-    lists:member(Peer, Running) andalso (rafter_config:has_vote(Peer, C) orelse 
-        (C#config.state =:= blank andalso lists:member(Peer, NewServers))).
-
-%% Transition to stable state, because it's likely the new servers aren't 
-%% running during tests.
-next_state(#state{config=#config{state=blank}}=S, _, 
-           {call, rafter, set_config, [_Peer, NewServers]}) ->
-    S#state{config=#config{state=stable, oldservers=NewServers}};
-
-%% The config succeeded
-next_state(S, {ok, Config, _}, {call, rafter, set_config, [_Peer, _NewServers]}) ->
-    S#state{config=Config};
-
-%% We aren't sure what the config is after a timeout. In this case we 'reload' our config
-%% Timeouts during config should only occur when a majority of servers aren't up. Since the
-%% server we are talking to is up and leader, it will keep trying to set this config.
-%% In this case we set the 'proposed config' so that the postconditions 
-%% can be verified for a timeout.
-next_state(S, {error, timeout, _}, {call, rafter, set_config, [Peer, _NewServers]}) ->
-    Config = rafter_log:get_config(Peer ++ "_log"),
-    S#state{config=Config};
+precondition(#state{running=Running}, {call, rafter, set_config, [Peer, _]}) ->
+    lists:member(Peer, Running).
 
+next_state(#state{config=blank}=S, _, _) ->
+    S#state{config=normal};
 next_state(S, _, _) ->
     S.
 
@@ -99,33 +83,46 @@ postcondition(_S, {call, rafter, set_config, [Peer, _NewServers]}, {error, {redi
     rafter:get_leader(Peer) =:= Leader;
 
 %% Config set successfully
-postcondition(_s, {call, rafter, set_config, _args}, {ok, _newconfig, _id}) ->
+postcondition(_S, {call, rafter, set_config, _args}, {ok, _newconfig, _id}) ->
     true;
 
-postcondition(#state{config=C, running=Running}, {call, rafter, set_config, [Peer, _]},
+postcondition(#state{running=Running}, {call, rafter, set_config, [Peer, _]},
               {error, peers_not_responding}) ->
-    majority_not_running(Peer, C, Running);
+    Config = get_config(Peer),
+    majority_not_running(Peer, Config, Running);
 
-postcondition(#state{config=C, running=Running}, {call, rafter, set_config, [Peer, _]},
+postcondition(#state{running=Running}, {call, rafter, set_config, [Peer, _]},
               {error, election_in_progress}) ->
-    majority_not_running(Peer, C, Running);
+    Config = get_config(Peer),
+    majority_not_running(Peer, Config, Running);
 
 %% We either can't reach a majority of peers or this peer is not part of the consensus group
-postcondition(#state{config=C, running=Running}, 
+postcondition(#state{running=Running}, 
              {call, rafter, set_config, [Peer, _NewServers]}, {error, timeout, _}) ->
+    C = get_config(Peer),
     majority_not_running(Peer, C, Running) orelse not lists:member(Peer, C#config.oldservers);
 
-postcondition(#state{config=C}, {call, rafter, set_config, _}, {error, config_in_progress}) ->
+postcondition(_S, {call, rafter, set_config, [Peer, _]}, 
+             {error, not_consensus_group_member}) ->
+    C = get_config(Peer),
+    false =:= rafter_config:has_vote(Peer, C);
+
+postcondition(_S, {call, rafter, set_config, [Peer, _]}, {error, config_in_progress}) ->
+    C = get_config(Peer),
     C#config.state =:= transitional;
 
-postcondition(#state{config=C}, 
-              {call, rafter, set_config, [_Peer, NewServers]}, {error, not_modified}) ->
+postcondition(#state{}, 
+              {call, rafter, set_config, [Peer, NewServers]}, {error, not_modified}) ->
+    C = get_config(Peer),
     C#config.oldservers =:= NewServers.
 
 %% ====================================================================
 %% EQC Properties
 %% ====================================================================
 
+get_config(Name) ->
+    rafter_log:get_config(logname(Name)).
+
 logname(FsmName) ->
     list_to_atom(atom_to_list(FsmName) ++ "_log").