aboutsummaryrefslogtreecommitdiff
path: root/aoc2023/build/packages/pqueue/test/pqueue_proper.erl
blob: 6702960d3c03362290e94e5f151622ec65674fcb (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
-module(pqueue_proper).
-ifdef(TEST).
-include_lib("proper/include/proper.hrl").

-behaviour(proper_statem).

-export([qc_pq/0, qc_pq2/0, qc_pq3/0, qc_pq4/0, correct/1]).

-export([command/1, initial_state/0, next_state/3, postcondition/3,
         precondition/2]).

-type value() :: integer().
-record(state, { in_queue :: [{value(), term()}] }).
-define(SERVER, queue_srv).

priority() ->
    integer(-20, 20).

%% Selects priorities we have added
priority(InQ) ->
    elements([P || {P, _} <- InQ]).

value() ->
    integer().

initial_state() ->
    #state { in_queue = [] }.

command(#state { in_queue = InQ }) ->
    oneof([{call, ?SERVER, in, [value()]},
           {call, ?SERVER, in, [value(), priority()]},
           {call, ?SERVER, is_empty, []},
           {call, ?SERVER, is_queue, []},
           {call, ?SERVER, len, []},
           {call, ?SERVER, out, []}] ++
          [{call, ?SERVER, out, [priority(InQ)]} || InQ =/= []] ++
          [{call, ?SERVER, pout, []},
           {call, ?SERVER, to_list, []}]).

next_state(#state { in_queue = InQ } = S, _V, {call, _, out, []}) ->
    S#state { in_queue = listq_rem(InQ) };
next_state(#state { in_queue = InQ } = S, _V, {call, _, out, [Prio]}) ->
    S#state { in_queue = listq_rem(InQ, Prio) };
next_state(#state { in_queue = InQ } = S, _V, {call, _, pout, _}) ->
    S#state { in_queue = listq_rem(InQ) };
next_state(S, _V, {call, _, to_list, _}) -> S;
next_state(S, _V, {call, _, is_queue, _}) -> S;
next_state(S, _V, {call, _, is_empty, _}) -> S;
next_state(S, _V, {call, _, len, _}) -> S;
next_state(#state { in_queue = InQ } = S, _V, {call, _, in, [Value, Prio]}) ->
    S#state { in_queue = listq_insert({Prio, Value}, InQ) };
next_state(#state { in_queue = InQ } = S, _V, {call, _, in, [Value]}) ->
    S#state { in_queue = listq_insert({0, Value}, InQ) }.

precondition(_S, _Call) ->
    true. % No limitation on the things we can call at all.

postcondition(#state { in_queue = InQ }, {call, _, out, [Prio]}, R) ->
    R == listq_prio_peek(InQ, Prio);
postcondition(#state { in_queue = InQ }, {call, _, pout, _}, R) ->
    R == listq_ppeek(InQ);
postcondition(#state { in_queue = InQ }, {call, _, out, _}, R) ->
    R == listq_peek(InQ);
postcondition(S, {call, _, to_list, _}, R) ->
    R == listq_to_list(S#state.in_queue);
postcondition(S, {call, _, len, _}, L) ->
    L == listq_length(S#state.in_queue);
postcondition(_S, {call, _, is_queue, _}, true) -> true;
postcondition(S, {call, _, is_empty, _}, Res) ->
    Res == (S#state.in_queue == []);
postcondition(_S, {call, _, in, _}, _) ->
    true;
postcondition(_, _, _) ->
    false.

correct(M) ->
    ?FORALL(Cmds, commands(?MODULE),
            ?TRAPEXIT(
                begin
                    ?SERVER:start_link(M),
                    {History,State,Result} = run_commands(?MODULE, Cmds),
                    ?SERVER:stop(),
                    ?WHENFAIL(io:format("History: ~w\nState: ~w\nResult: ~w\n",
                                        [History,State,Result]),
                              aggregate(command_names(Cmds), Result =:= ok))
                end)).

qc_opts() ->
    [{numtests, 10000}].
     
qc_pq() ->
    proper:quickcheck(pqueue_proper:correct(pqueue), qc_opts()).

qc_pq2() ->
    proper:quickcheck(pqueue_proper:correct(pqueue2), qc_opts()).

qc_pq3() ->
    proper:quickcheck(pqueue_proper:correct(pqueue3), qc_opts()).

qc_pq4() ->
    proper:quickcheck(pqueue_proper:correct(pqueue4), qc_opts()).

%% ----------------------------------------------------------------------

%% A listq is a sorted list of priorities
listq_insert({P, V}, []) ->
    [{P, [V]}];
listq_insert({P, V}, [{P1, _} | _] = LQ) when P < P1 ->
    [{P, [V]} | LQ];
listq_insert({P, V}, [{P1, Vs} | Next]) when P == P1 ->
    [{P, Vs ++ [V]} | Next];
listq_insert({P, V}, [{P1, Vs} | Next]) when P > P1 ->
    [{P1, Vs} | listq_insert({P, V}, Next)].

listq_to_list(L) ->
    lists:concat(
      [ Vals || {_Prio, Vals} <- L]).

listq_length(L) ->
    lists:sum(
      [ length(Vs) || {_Prio, Vs} <- L]).

listq_rem([]) ->
    [];
listq_rem([{_P, [_V]} | Next]) ->
    Next;
listq_rem([{P, [_V1 | Vs]} | Next]) ->
    [{P, Vs} | Next].

listq_rem([], _P) ->
    [];
listq_rem([{P, [_]} | Next], P) ->
    Next;
listq_rem([{P, [_ | Vs]} | Next], P) ->
    [{P, Vs} | Next];
listq_rem([{P1, Vs} | Next], P) ->
    [{P1, Vs} | listq_rem(Next, P)].

listq_peek([]) ->
    empty;
listq_peek([{_P, [V | _]} | _]) ->
    {value, V}.

listq_prio_peek([{P, [V | _]} | _], P) ->
    {value, V};
listq_prio_peek([{_P1, _} | Next], P) ->
    listq_prio_peek(Next, P);
listq_prio_peek([], _P) ->
    empty.

listq_ppeek([]) ->
    empty;
listq_ppeek([{P, [V | _]} | _]) ->
    {value, V, P}.

-endif.