1%% -*- erlang-indent-level: 4;indent-tabs-mode: nil -*-
2%% ex: ts=4 sw=4 et
3%%
4%% This file is part of Triq - Trifork QuickCheck
5%%
6%% Copyright (c) 2011-2013 by Trifork
7%%
8%% Licensed under the Apache License, Version 2.0 (the "License");
9%% you may not use this file except in compliance with the License.
10%% You may obtain a copy of the License at
11%%
12%%     http://www.apache.org/licenses/LICENSE-2.0
13%%
14%% Unless required by applicable law or agreed to in writing, software
15%% distributed under the License is distributed on an "AS IS" BASIS,
16%% WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
17%% See the License for the specific language governing permissions and
18%% limitations under the License.
19%%
20
21%% TODO: Share code with triq_statem_fsm. Until then make sure you
22%% apply any changes to triq_statem_fsm as well.
23
24-module(triq_statem).
25
26-define(TRIES,100).
27-define(FORALL(X,Gen,Property),
28        {'prop:forall', Gen, ??X, fun(X)-> begin Property end end, ??Property}).
29
30-import(triq_dom,
31        [pick/2,
32         domain/3]).
33-import(triq_expr,
34        [eval/2,
35         free_vars/1]).
36-export([commands/1,
37         commands/2,
38         run_commands/2,
39         run_commands/3,
40         state_after/2,
41         prop_statem/1,
42         command_names/1,
43         zip/2]).
44
45
46commands(Module) ->
47    domain(commands,
48           fun(_,Size) ->
49                   gen_commands(Module,
50                                Module:initial_state(),
51                                [],[],[],
52                                Size, Size, ?TRIES)
53           end,
54           undefined).
55
56commands(Module, InitialState) ->
57    domain(commands,
58           fun(_,Size) ->
59                   gen_commands(Module,
60                                InitialState,
61                                [],[],[],
62                                Size, Size, ?TRIES)
63           end,
64           undefined).
65
66gen_commands(Module,_,SymbolicStates,CallDoms,Commands,_,0,_) ->
67    {shrinkable_commands(Module,
68                         lists:reverse(SymbolicStates),
69                         lists:reverse(CallDoms)),
70     lists:reverse(Commands)};
71gen_commands(Module,State,_,_,_,_,_,0) ->
72    erlang:error({cannot_generate,Module,State});
73gen_commands(Module,State,States,Domains,[],Size,Count,Tries) ->
74    gen_commands(Module,State,States,Domains,[{init,State}],Size,Count,Tries);
75gen_commands(Module,State,States,Domains,Commands,Size,Count,Tries) ->
76    CmdDom = Module:command(State),
77    {CD,C} = pick(CmdDom,Size),
78
79    case Module:precondition(State, C) of
80        true ->
81            Var = {var, Size-Count},
82            NextState = Module:next_state(State, Var, C),
83            Command = {set, Var, C},
84            gen_commands(Module,
85                         NextState,
86                         [State|States],
87                         [CD|Domains],
88                         [Command|Commands],
89                         Size,
90                         Count-1, ?TRIES);
91        _ ->
92            %% try again, up to Tries times...
93            gen_commands(Module,State,States,Domains,Commands,Size,Count,
94                         Tries-1)
95    end.
96
97shrinkable_commands(Module,SymbolicStates,Domains) ->
98    domain
99      (shrinking_commands,
100       undefined,
101       fun(Dom,Commands) ->
102               commands_shrink(Module,SymbolicStates,Domains,Dom,Commands,
103                               ?TRIES)
104       end).
105
106-define(MIN(A,B), (if (A<B) -> A; (B<A) -> B; (A==B) -> A end)).
107
108commands_shrink(_,_,_,_,[],_) -> {[],[]};
109commands_shrink(_,_,_,Dom,Commands,0) -> {Dom,Commands};
110commands_shrink(Module,SymbolicStates,Domains, Dom, Commands,Tries) ->
111    Len = length(Commands),
112    true = (Len > 0),
113
114    %% choose a segment of commands to delete...
115    RemIdx = random:uniform(Len),
116    RemLen = if RemIdx==Len ->
117                     0;
118                true ->
119                     random:uniform(?MIN(5, Len-RemIdx))
120             end,
121
122    NewCommands = without(RemIdx,RemLen,Commands),
123    NewStates = without(RemIdx,RemLen,SymbolicStates),
124    NewDomains = without(RemIdx,RemLen,Domains),
125
126    StartState =
127        if RemIdx == 1 -> hd(SymbolicStates);
128           true -> Module:initial_state()
129        end,
130
131    case validate(Module,
132                  StartState,
133                  NewStates,
134                  NewCommands) of
135
136        %% yay! removing that transition left us with a valid set of states
137        true ->
138            {shrinkable_commands(Module,NewStates,NewDomains),
139             NewCommands};
140
141        %% oops, removing transition at RemIdx didn't validate...
142        _ ->
143            commands_shrink(Module,SymbolicStates,Domains,Dom,Commands,Tries-1)
144    end.
145
146%%
147%% validate a shrunken command sequence
148%%
149validate(Mod, State, _States, Commands) ->
150    validate2(Mod, State, Commands, []).
151
152validate2(_Mod,_State,[], _KnownVars) ->
153    true;
154validate2(Module,_State,[{init,S}|Commands], _KnownVars) ->
155    validate2(Module,S,Commands, []);
156validate2(Module,State,[{set,Var,Call}|Commands], KnownVars) ->
157    FreeVars = free_vars(Call),
158    UnknownVars = FreeVars -- KnownVars,
159    (UnknownVars == [])
160        andalso (Module:precondition(State,Call)==true)
161        andalso begin
162                    NextState = Module:next_state(State, Var, Call),
163                    validate2(Module,NextState, Commands, [Var|KnownVars])
164                end.
165
166run_commands(Module,Commands) ->
167    run_commands(Module,Commands,[]).
168
169run_commands(Module,Commands,Env) ->
170    do_run_command(Commands,
171                   Env,
172                   Module,
173                   [],
174                   Module:initial_state()).
175
176do_run_command(Commands, Env, Module, History, State) ->
177    case Commands of
178        [] ->
179            {History, eval(Env,State), ok};
180
181        [{init,S}|Rest] ->
182            do_run_command(Rest, Env, Module, History, S);
183
184        [{set, {var,V}=Var, {call,M,F,A}=SymCall}|Rest] ->
185            M2=eval(Env,M),
186            F2=eval(Env,F),
187            A2=eval(Env,A),
188
189            %% Same as eval(Env, SymCall), but we need to log in History.
190            Res = apply(M2,F2,A2),
191
192            SubstCall = {call, M2,F2,A2},
193            History2 = [{SubstCall,Res}|History],
194
195            case Module:postcondition(State,SubstCall,Res) of
196                true ->
197                    Env2 = [{V,Res}|proplists:delete(V,Env)],
198                    State2 = Module:next_state(State,Var,SymCall),
199                    do_run_command(Rest, Env2, Module, History2, State2);
200
201                Other ->
202                    {History, eval(Env,State), {postcondition, Other}}
203            end
204    end.
205
206%%-----------------------------------------------------------------
207%% @doc Evaluate command list, and return final state.
208%%
209%% Given a `Module' and `Commands', a value picked from the domain
210%% `triq_statem:commands(Module)'
211%% @end
212%%-----------------------------------------------------------------
213state_after(Module,Commands) ->
214    NextState = fun(S,V,C) -> Module:next_state(S,V,C) end,
215    lists:foldl(fun({init,S}, _) ->
216                        S;
217                   ({set,Var,Call},S) ->
218                        NextState(S,Var,Call)
219                end,
220                Module:initial_state(),
221                Commands).
222
223%%-----------------------------------------------------------------
224%% @doc Boiler-plate property for testing state machines.
225%% <pre>
226%% prop_statem(Module) ->
227%%     ?FORALL(Commands, commands(Module),
228%%        begin
229%%          {_,_,ok} = run_commands(Module, Commands),
230%%          true
231%%        end).
232%% </pre>
233%% @end
234%%-----------------------------------------------------------------
235prop_statem(Module) ->
236    ?FORALL(Commands, commands(Module),
237            begin
238                {_,_,ok} = run_commands(Module, Commands),
239                true
240            end).
241
242%%
243%% utility to delete Count elements at RemIndex of List
244%%
245without(_, 0, List) -> List;
246without(RemIdx, Count, List) ->
247    without(RemIdx, Count-1, without(RemIdx, List)).
248
249without(RemIdx,List) when is_list(List) ->
250    {First,Rest} = lists:split(RemIdx-1,List),
251    First ++ tl(Rest);
252without(RemIdx,Tup) when is_tuple(Tup) ->
253    list_to_tuple(without(RemIdx, tuple_to_list(Tup))).
254
255%%
256%% simplify command names
257%%
258command_names(Calls) ->
259    [{M,F,length(Args)} || {call, M, F, Args} <- Calls].
260
261zip(X, Y) ->
262    zip(X, Y, []).
263
264zip([], _, Acc) -> lists:reverse(Acc);
265zip(_, [], Acc) -> lists:reverse(Acc);
266zip([A|T1], [B|T2], Acc) ->
267    zip(T1, T2, [{A,B}|Acc]).
268