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. Until then make sure you apply
22%% any changes to triq_statem as well.
23
24-module(triq_statem_fsm).
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                                triq_fsm_stub:initial_state(Module),
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 = triq_fsm_stub:command(Module, State),
77    {CD,C} = pick(CmdDom,Size),
78
79    case triq_fsm_stub:precondition(Module, State, C) of
80        true ->
81            Var = {var, Size-Count},
82            NextState = triq_fsm_stub:next_state(Module, 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 -> triq_fsm_stub:initial_state(Module)
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 (triq_fsm_stub:precondition(Module,State,Call)==true)
161        andalso begin
162                    NextState = triq_fsm_stub:next_state(Module, State,
163                                                         Var, Call),
164                    validate2(Module, NextState, Commands, [Var|KnownVars])
165                end.
166
167run_commands(Module,Commands) ->
168    run_commands(Module,Commands,[]).
169
170run_commands(Module,Commands,Env) ->
171    do_run_command(Commands,
172                   Env,
173                   Module,
174                   [],
175                   triq_fsm_stub:initial_state(Module)).
176
177do_run_command(Commands, Env, Module, History, State) ->
178    case Commands of
179        [] ->
180            {History, eval(Env,State), ok};
181
182        [{init,S}|Rest] ->
183            do_run_command(Rest, Env, Module, History, S);
184
185        [{set, {var,V}=Var, {call,M,F,A}=SymCall}|Rest] ->
186            M2=eval(Env,M),
187            F2=eval(Env,F),
188            A2=eval(Env,A),
189
190            %% Same as eval(Env, SymCall), but we need to log in History.
191            Res = apply(M2,F2,A2),
192
193            SubstCall = {call, M2,F2,A2},
194            History2 = [{SubstCall,Res}|History],
195
196            case triq_fsm_stub:postcondition(Module,State,SubstCall,Res) of
197                true ->
198                    Env2 = [{V,Res}|proplists:delete(V,Env)],
199                    State2 = triq_fsm_stub:next_state(Module,State,Var,SymCall),
200                    do_run_command(Rest, Env2, Module, History2, State2);
201
202                Other ->
203                    {History, eval(Env,State), {postcondition, Other}}
204            end
205    end.
206
207%%-----------------------------------------------------------------
208%% @doc Evaluate command list, and return final state.
209%%
210%% Given a `Module' and `Commands', a value picked from the domain
211%% `triq_statem:commands(Module)'
212%% @end
213%%-----------------------------------------------------------------
214state_after(Module,Commands) ->
215    NextState = fun(S,V,C) -> triq_fsm_stub:next_state(Module,S,V,C) end,
216    lists:foldl(fun({init,S}, _) ->
217                        S;
218                   ({set,Var,Call},S) ->
219                        NextState(S,Var,Call)
220                end,
221                triq_fsm_stub:initial_state(Module),
222                Commands).
223
224%%-----------------------------------------------------------------
225%% @doc Boiler-plate property for testing state machines.
226%% <pre>
227%% prop_statem(Module) ->
228%%     ?FORALL(Commands, commands(Module),
229%%        begin
230%%          {_,_,ok} = run_commands(Module, Commands),
231%%          true
232%%        end).
233%% </pre>
234%% @end
235%%-----------------------------------------------------------------
236prop_statem(Module) ->
237    ?FORALL(Commands, commands(Module),
238            begin
239                {_,_,ok} = run_commands(Module, Commands),
240                true
241            end).
242
243%%
244%% utility to delete Count elements at RemIndex of List
245%%
246without(_, 0, List) -> List;
247without(RemIdx, Count, List) ->
248    without(RemIdx, Count-1, without(RemIdx, List)).
249
250without(RemIdx,List) when is_list(List) ->
251    {First,Rest} = lists:split(RemIdx-1,List),
252    First ++ tl(Rest);
253without(RemIdx,Tup) when is_tuple(Tup) ->
254    list_to_tuple(without(RemIdx, tuple_to_list(Tup))).
255
256%%
257%% simplify command names
258%%
259command_names(Calls) ->
260    [{M,F,length(Args)} || {call, M, F, Args} <- Calls].
261
262zip(X, Y) ->
263    zip(X, Y, []).
264
265zip([], _, Acc) -> lists:reverse(Acc);
266zip(_, [], Acc) -> lists:reverse(Acc);
267zip([A|T1], [B|T2], Acc) ->
268    zip(T1, T2, [{A,B}|Acc]).
269