quickcheck_example.erl

-module(example_05_eqc).
-compile(export_all).

-include_lib("eqc/include/eqc.hrl").
-include_lib("eqc/include/eqc_statem.hrl").

initial_state() ->
    [].

next_state(S,V,{call,file,write_file,[Name, Content]}) ->
    [{Name,Content} | proplists:delete(Name,S)];
next_state(S,V,{call,file,delete,[Name]}) ->
    proplists:delete(Name,S);
next_state(S,V,{call,file,read_file,[Name]}) ->
    S.

precondition(_S,_) ->
    true.

postcondition(S, {call, _, write_file,[_,_]},R) ->
    R == ok;
postcondition(S, {call, _, delete,[Name]},R) ->
    case R of
        ok -> lists:keymember(Name,1,S);
        {error,enoent} -> not lists:keymember(Name,1,S)
    end;
postcondition(S, {call, _, read_file,[Name]},R) ->
    case R of
        {ok, Content} ->
            lists:member({Name,Content},S);
        {error, enoent} -> not lists:keymember(Name, 1, S)
    end.
        
command(S) ->
    oneof([
    {call,file,write_file,[name(),content()]},
    {call,file,delete,[name()]},
    {call,file,read_file,[name()]}
    ]).
    
name() ->
    oneof(["eqc_file_1","eqc_file_2","eqc_file_3"]).
    
content() ->
    binary().

prop_fileio() ->
    ?FORALL(Cmds,commands(?MODULE),
    begin
        {H,S,Res} = run_commands(?MODULE, Cmds),
        [file:delete(Name) || Name <- proplists:get_keys(S)],
        ?WHENFAIL(io:format("H: ~p~nS: ~p~nRes: ~p~n", [H, S, Res]),
        Res == ok)
    end).