%% Sample specification for the locker.

-module(lock_eqc).

-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_fsm.hrl").
-compile(export_all).

%% We specify each state via a function that returns a list of
%% transitions---pairs of target states and symbolic call generators.

unlocked(S) ->
    read_transition(S) ++
    [{locked,{call,lock,lock,[]}}].

locked(S) ->
    read_transition(S) ++
    [{unlocked,{call,lock,unlock,[]}},
     {locked,{call,lock,write,[key(),value()]}}].

%% Common transitions can be factored out into a separate function;
%% note the use of 'history' as a target state to represent a
%% transition that returns to the same state, no matter what state it
%% is embedded in.

read_transition(S) ->
    [{history,{call,lock,read,[elements(proplists:get_keys(S))]}}].

%% The parameter S is the state data--in this example, just the
%% keys and values held in the locker.

%% It just remains to generate the keys and values.

key() ->
    elements([a,b,c,d]).

value() ->
    int().

%% The following call-backs define the behaviour of the locker, and
%% closely resemble the corresponding call-backs in eqc_statem.

initial_state() ->
    unlocked.

initial_state_data() ->
    [].

next_state_data(_,_,S,_,{call,_,write,[Key,Value]}) ->
    [{Key,Value}|proplists:delete(Key,S)];
next_state_data(_,_,S,_,{call,_,_,_}) ->
    S.

postcondition(_,_,S,{call,_,read,[Key]},R) ->
    R == proplists:get_value(Key,S);
postcondition(_,_,_,_,R) ->
    R == ok.

precondition(_,_,S,{call,_,read,[Key]}) ->
    proplists:is_defined(Key,S);
precondition(_,_,_,_) ->
    true.

%% Finally, a property which tests the locker, and collects statistics
%% on the transitions that were tested.

prop_locker() ->
    ?FORALL(Cmds,commands(lock_eqc),
	    begin
		lock:start(),
		{H,_S,Res} = run_commands(lock_eqc,Cmds),
		lock:stop(),
		aggregate(zip(state_names(H),command_names(Cmds)),
			  Res == ok)
	    end).

%% This last definition is only needed for QuickCheck's analysis: it
%% just tells QuickCheck how often we expect the precondition of read
%% to fail.

precondition_probability(locked,_,{call,_,read,_}) ->
    0.6;
precondition_probability(unlocked,_,{call,_,read,_}) ->
    0.4;
precondition_probability(_,_,_) ->
    1.