Skip to content
Browse files

Triq: Bugfix in command sequence shrinking (validation should ensure …

…that all used variables are bound).

Moved eval() to new module.
  • Loading branch information...
1 parent 3e96d90 commit c22969015e8d838250503bea3a5690d2f72a8df6 @eriksoe eriksoe committed Sep 12, 2011
Showing with 87 additions and 82 deletions.
  1. +1 −59 src/triq_dom.erl
  2. +68 −0 src/triq_expr.erl
  3. +18 −23 src/triq_statem.erl
View
60 src/triq_dom.erl
@@ -102,7 +102,7 @@
%% using a generator
-export([bind/2, bindshrink/2, suchthat/2, pick/2, shrink/2, sample/1, sampleshrink/1,
- seal/1, open/1, peek/1, eval/1, eval/2,
+ seal/1, open/1, peek/1,
domain/3, shrink_without_duplicates/1]).
@@ -1201,64 +1201,6 @@ domain(Name,PickFun,ShrinkFun) ->
#?DOM{kind=Name, pick=PickFun, shrink=ShrinkFun}.
-%%-----------------------------------------------------------------------
-%% @doc Evaluate `Body'. Occurrences of `{call,M,F,A}'
-%% is replaced by the result of calling `erlang:apply(M,F,A)', and
-%% occurrences of `{var,Name}' in `Body' are not substituted.
-%%
-%% This is a plain function, not a compile_transform or anything like that,
-%% so nested functions are not traversed in the substitution. However, nested
-%% occurrences of `{call,M,F,A}' are substituted as one would think:
-%% depth first, left-to-right.
-%%
-%% @spec eval(Body::any()) -> any()
-%% @equiv eval([],Body)
-%% @end
-%% -----------------------------------------------------------------------
-eval(Term) ->
- eval([], Term).
-
-%%-----------------------------------------------------------------------
-%% @doc Evaluate `Body', replacing occurrences of `{call,M,F,A}' and `{var,N}'.
-%% Occurrences of `{call,M,F,A}' is replaced by `erlang:apply(M,F,A)', and
-%% `{var,Name}' is replaced by the value with key `Name' in `PropList'.
-%%
-%% Exceptions happening when calling `erlang:apply/3' are not caught.
-%% If `Name' is unbound i.e., `Name' does not appear in `PropList' or if
-%% `Name' is not an atom, `{var,Name}' is unchanged.
-%%
-%% This is a plain function, not a compile_transform or anything like that,
-%% so nested functions are not traversed in the substitution. However, nested
-%% occurrences of `{call,M,F,A}' are substituted as one would think:
-%% depth first, left-to-right.
-%%
-%% @spec eval(PropList::[{atom(),any()}], Body::any()) -> any()
-%% @end
-%%-----------------------------------------------------------------------
-eval(PropList, [H|T]) ->
- [eval(PropList,H) | eval(PropList,T)];
-
-eval(PropList, Tuple) when is_tuple(Tuple) ->
- case eval(PropList, tuple_to_list(Tuple)) of
- [call, Mod, Fun, Args] ->
- M = eval(PropList, Mod),
- F = eval(PropList, Fun),
- A = eval(PropList, Args),
- erlang:apply(M,F,A);
-
- [var, Name] when is_integer(Name) ->
- case proplists:lookup(Name, PropList) of
- none -> {var, Name};
- {Name, Value} -> Value
- end;
-
- List ->
- list_to_tuple(List)
- end;
-
-eval(_, Term) ->
- Term.
-
%%
%% Utility funcitons
%%
View
68 src/triq_expr.erl
@@ -0,0 +1,68 @@
+-module(triq_expr).
+
+-export([eval/1, eval/2, free_vars/1]).
+
+%%-----------------------------------------------------------------------
+%% @doc Evaluate `Body'. Occurrences of `{call,M,F,A}'
+%% is replaced by the result of calling `erlang:apply(M,F,A)', and
+%% occurrences of `{var,Name}' in `Body' are not substituted.
+%%
+%% This is a plain function, not a compile_transform or anything like that,
+%% so nested functions are not traversed in the substitution. However, nested
+%% occurrences of `{call,M,F,A}' are substituted as one would think:
+%% depth first, left-to-right.
+%%
+%% @spec eval(Body::any()) -> any()
+%% @equiv eval([],Body)
+%% @end
+%% -----------------------------------------------------------------------
+eval(Term) ->
+ eval([], Term).
+
+%%-----------------------------------------------------------------------
+%% @doc Evaluate `Body', replacing occurrences of `{call,M,F,A}' and `{var,N}'.
+%% Occurrences of `{call,M,F,A}' is replaced by `erlang:apply(M,F,A)', and
+%% `{var,Name}' is replaced by the value with key `Name' in `PropList'.
+%%
+%% Exceptions happening when calling `erlang:apply/3' are not caught.
+%% If `Name' is unbound i.e., `Name' does not appear in `PropList' or if
+%% `Name' is not an atom, `{var,Name}' is unchanged.
+%%
+%% This is a plain function, not a compile_transform or anything like that,
+%% so nested functions are not traversed in the substitution. However, nested
+%% occurrences of `{call,M,F,A}' are substituted as one would think:
+%% depth first, left-to-right.
+%%
+%% @spec eval(PropList::[{atom(),any()}], Body::any()) -> any()
+%% @end
+%%-----------------------------------------------------------------------
+eval(PropList, [H|T]) ->
+ [eval(PropList,H) | eval(PropList,T)];
+
+eval(PropList, Tuple) when is_tuple(Tuple) ->
+ case tuple_to_list(Tuple) of
+ [call, Mod, Fun, Args] ->
+ M = eval(PropList, Mod),
+ F = eval(PropList, Fun),
+ A = eval(PropList, Args),
+ erlang:apply(M,F,A);
+
+ [var, Name] when is_integer(Name) ->
+ case proplists:lookup(Name, PropList) of
+ none -> {var, Name};
+ {Name, Value} -> Value
+ end;
+
+ List ->
+ list_to_tuple(eval(PropList,List))
+ end;
+
+eval(_, Term) ->
+ Term.
+
+
+free_vars([H|T]) -> free_vars(H) ++ free_vars(T);
+free_vars({var, Name}=Var) when is_integer(Name) -> [Var];
+free_vars(Tuple) when is_tuple(Tuple) ->
+ lists:concat(lists:map(fun free_vars/1, tuple_to_list(Tuple)));
+free_vars(_Term) -> [].
View
41 src/triq_statem.erl
@@ -4,7 +4,8 @@
-define(FORALL(X,Gen,Property),
{'prop:forall', Gen, ??X, fun(X)-> begin Property end end, ??Property}).
--import(triq_dom, [eval/2, pick/2, domain/3]).
+-import(triq_dom, [pick/2, domain/3]).
+-import(triq_expr, [eval/2, free_vars/1]).
-export([commands/1, run_commands/2, run_commands/3, state_after/2, prop_statem/1]).
@@ -101,20 +102,22 @@ commands_shrink(Module,SymbolicStates,Domains, Dom, Commands,Tries) ->
%%
%% validate a shrunken command sequence
%%
-validate(_Mod,_State,_States,[]) -> true;
-
-validate(Module,_State,[_|States],[{init,S}|Commands]) ->
- validate(Module,S,States,Commands);
-
-validate(Module,State,[_|States],[{set,Var,Call}|Commands]) ->
- case Module:precondition(State,Call) of
- true ->
- case Module:next_state(State, Var, Call) of
- NextState ->
- validate(Module,NextState, States, Commands)
- end;
- _ -> false
- end.
+validate(Mod, State, _States, Commands) ->
+ validate2(Mod, State, Commands, []).
+
+validate2(_Mod,_State,[], _KnownVars) ->
+ true;
+validate2(Module,_State,[{init,S}|Commands], _KnownVars) ->
+ validate2(Module,S,Commands, []);
+validate2(Module,State,[{set,Var,Call}|Commands], KnownVars) ->
+ FreeVars = free_vars(Call),
+ UnknownVars = FreeVars -- KnownVars,
+ (UnknownVars == [])
+ andalso (Module:precondition(State,Call)==true)
+ andalso begin
+ NextState = Module:next_state(State, Var, Call),
+ validate2(Module,NextState, Commands, [Var|KnownVars])
+ end.
run_commands(Module,Commands) ->
run_commands(Module,Commands,[]).
@@ -209,11 +212,3 @@ without(RemIdx,List) when is_list(List) ->
without(RemIdx,Tup) when is_tuple(Tup) ->
list_to_tuple(without(RemIdx, tuple_to_list(Tup))).
-
-
-
-
-
-
-
-

0 comments on commit c229690

Please sign in to comment.
Something went wrong with that request. Please try again.