| % Licensed under the Apache License, Version 2.0 (the "License"); you may not |
| % use this file except in compliance with the License. You may obtain a copy of |
| % the License at |
| % |
| % http:%www.apache.org/licenses/LICENSE-2.0 |
| % |
| % Unless required by applicable law or agreed to in writing, software |
| % distributed under the License is distributed on an "AS IS" BASIS, WITHOUT |
| % WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the |
| % License for the specific language governing permissions and limitations under |
| % the License. |
| |
| -module(hqueue_statem). |
| |
| -include_lib("proper/include/proper.hrl"). |
| -include_lib("eunit/include/eunit.hrl"). |
| |
| |
| -behaviour(proper_statem). |
| |
| |
| -export([ |
| hqueue_works/0 |
| ]). |
| -export([ |
| command/1, |
| initial_state/0, |
| next_state/3, |
| postcondition/3, |
| precondition/2 |
| ]). |
| |
| |
| -type priority() :: float(). |
| -type val() :: integer(). |
| -type job() :: {priority(), val()}. |
| |
| |
| -record(state, { |
| queue :: [job()] |
| }). |
| |
| |
| hqueue_works_test_() -> |
| { |
| timeout, |
| 100000, |
| ?_assertEqual( |
| true, |
| proper:quickcheck( |
| ?MODULE:hqueue_works(), |
| [{to_file, user}, {numtests, 100}])) |
| }. |
| |
| |
| hqueue_works() -> |
| ?FORALL(Cmds, commands(?MODULE), |
| ?TRAPEXIT( |
| begin |
| {ok, HQ} = hqueue:new(), |
| {History,State,Result} = run_commands(?MODULE, Cmds, [{hq, HQ}]), |
| ?WHENFAIL(io:format("History: ~w\nState: ~w\nResult: ~w\n", |
| [History,State,Result]), |
| aggregate(command_names(Cmds), Result =:= ok)) |
| |
| end)). |
| |
| |
| initial_state() -> |
| #state{queue=[]}. |
| |
| |
| command(_) -> |
| frequency([ |
| {30, {call, hqueue, insert, [{var, hq}, non_neg_float(), integer()]}}, |
| {30, {call, hqueue, extract_max, [{var, hq}]}}, |
| {1, {call, hqueue, size, [{var, hq}]}}, |
| {1, {call, hqueue, is_empty, [{var, hq}]}}, |
| {1, {call, hqueue, max_elems, [{var, hq}]}} |
| ]). |
| |
| |
| precondition(_, _) -> |
| true. |
| |
| |
| next_state(#state{queue=Q0}=S, _RV, {call, _, insert, [_, P, V]}) -> |
| Q1 = lists:reverse(lists:keysort(1, [{P, V} | Q0])), |
| S#state{queue=Q1}; |
| next_state(#state{queue=[]}=S, _RV, {call, _, extract_max, [_]}) -> |
| S; |
| next_state(#state{queue=[_|Q]}=S, _RV, {call, _, extract_max, [_]}) -> |
| S#state{queue=Q}; |
| next_state(S, _RV, {call, _, size, [_]}) -> |
| S; |
| next_state(S, _RV, {call, _, is_empty, [_]}) -> |
| S; |
| next_state(S, _RV, {call, _, max_elems, [_]}) -> |
| S. |
| |
| |
| postcondition(_S, {call, _, insert, _}, Result) -> |
| ok =:= Result; |
| postcondition(#state{queue=[]}, {call, _, extract_max, [_]}, {error, empty}) -> |
| true; |
| postcondition(#state{queue=[{_P1,V}|_]}, {call, _, extract_max, [_]}, |
| {_P2, Result}) -> |
| V =:= Result; |
| postcondition(#state{queue=Q}, {call, _, size, [_]}, Result) -> |
| length(Q) =:= Result; |
| postcondition(#state{queue=Q}, {call, _, is_empty, [_]}, Result) -> |
| (length(Q) =:= 0) =:= Result; |
| postcondition(_S, {call, _, max_elems, [_]}, Result) -> |
| 0 < Result. |
| |