Skip to content

Commit

Permalink
Fix observation for timedout/1
Browse files Browse the repository at this point in the history
When considering the output of a timedout/1 observation, do not carry
about the order, but only that we return the right amount of elements.
Thus by sorting the output we make sure that we get the right kind of
observation.
  • Loading branch information
jlouis committed Mar 12, 2012
1 parent 90291f0 commit d9a1fa5
Showing 1 changed file with 7 additions and 8 deletions.
15 changes: 7 additions & 8 deletions test/jobs_eqc_queue.erl
Expand Up @@ -83,7 +83,7 @@ timedout_obs(Mod, #model { st = Q} = M) ->
set_time(M),
case Mod:timedout(Q) of
[] -> [];
{TO, _} -> TO
{TO, _} -> lists:sort(TO)
end.

in(Mod, Job, #model { time = T, st = Q} = M) ->
Expand Down Expand Up @@ -162,23 +162,22 @@ prop_queue() ->
catching(fun() ->
R = eval(M),
Ty:representation(R#model.st)
end, e),
end),
catching(fun () ->
R = model(M),
jobs_queue_model:representation(R#model.st)
end, q)))).
end)))).

prop_observe() ->
?FORALL(Obs, obs(),
equals(
catching(fun() -> eval(Obs) end, e),
catching(fun() -> model(Obs) end, m))).
catch eval(Obs),
catch model(Obs))).

catching(F, T) ->
catching(F) ->
try F()
catch C:E ->
io:format("Exception: ~p:~p~n", [C, E]),
T
{exception, C, E}
end.

set_time(#model { time = T}) ->
Expand Down

0 comments on commit d9a1fa5

Please sign in to comment.