Skip to content

Commit 32e31ee

Browse files
authored
Merge pull request #40 from lasp-lang/is_bottom
Add is_bottom/1 to state_type API
2 parents 26e3374 + 808cf52 commit 32e31ee

12 files changed

+159
-11
lines changed

src/state_bcounter.erl

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747

4848
-export([new/0, new/1]).
4949
-export([mutate/3, delta_mutate/3, merge/2]).
50-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
50+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
5151
-export([join_decomposition/1]).
5252

5353
-export_type([state_bcounter/0, delta_state_bcounter/0, state_bcounter_op/0]).
@@ -186,6 +186,16 @@ equal({?TYPE, {PNCounter1, GMap1}}, {?TYPE, {PNCounter2, GMap2}}) ->
186186
?PNCOUNTER_TYPE:equal(PNCounter1, PNCounter2) andalso
187187
?GMAP_TYPE:equal(GMap1, GMap2).
188188

189+
%% @doc Some BCounter state is bottom is both components
190+
%% of the pair (the PNCounter and the GMap)
191+
%% are bottom.
192+
-spec is_bottom(delta_or_state()) -> boolean().
193+
is_bottom({?TYPE, {delta, BCounter}}) ->
194+
is_bottom({?TYPE, BCounter});
195+
is_bottom({?TYPE, {PNCounter, GMap}}) ->
196+
?PNCOUNTER_TYPE:is_bottom(PNCounter) andalso
197+
?GMAP_TYPE:is_bottom(GMap).
198+
189199
%% @doc Given two `state_bcounter()', check if the second is an
190200
%% inflation of the first.
191201
%% We have and inflation if we have an inflation component wise.

src/state_gcounter.erl

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747

4848
-export([new/0, new/1]).
4949
-export([mutate/3, delta_mutate/3, merge/2]).
50-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
50+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
5151
-export([join_decomposition/1]).
5252

5353
-export_type([state_gcounter/0, delta_state_gcounter/0, state_gcounter_op/0]).
@@ -134,6 +134,13 @@ equal({?TYPE, GCounter1}, {?TYPE, GCounter2}) ->
134134
Fun = fun(Value1, Value2) -> Value1 == Value2 end,
135135
orddict_ext:equal(GCounter1, GCounter2, Fun).
136136

137+
%% @doc Check if a GCounter is bottom.
138+
-spec is_bottom(delta_or_state()) -> boolean().
139+
is_bottom({?TYPE, {delta, GCounter}}) ->
140+
is_bottom({?TYPE, GCounter});
141+
is_bottom({?TYPE, GCounter}) ->
142+
orddict:is_empty(GCounter).
143+
137144
%% @doc Given two `state_gcounter()', check if the second is an inflation
138145
%% of the first.
139146
%% Two conditions should be met:
@@ -275,6 +282,12 @@ equal_test() ->
275282
?assertNot(equal(Counter1, Counter3)),
276283
?assertNot(equal(Counter1, Counter4)).
277284

285+
is_bottom_test() ->
286+
Counter0 = new(),
287+
Counter1 = {?TYPE, [{1, 2}]},
288+
?assert(is_bottom(Counter0)),
289+
?assertNot(is_bottom(Counter1)).
290+
278291
is_inflation_test() ->
279292
Counter1 = {?TYPE, [{1, 2}, {2, 1}, {4, 1}]},
280293
DeltaCounter1 = {?TYPE, {delta, [{1, 2}, {2, 1}, {4, 1}]}},

src/state_gmap.erl

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@
4343

4444
-export([new/0, new/1]).
4545
-export([mutate/3, delta_mutate/3, merge/2]).
46-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
46+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
4747
-export([join_decomposition/1]).
4848

4949
-export_type([state_gmap/0, delta_state_gmap/0, state_gmap_op/0]).
@@ -135,6 +135,13 @@ equal({?TYPE, {Type, GMap1}}, {?TYPE, {Type, GMap2}}) ->
135135
end,
136136
orddict_ext:equal(GMap1, GMap2, Fun).
137137

138+
%% @doc Check if a GMap is bottom
139+
-spec is_bottom(delta_or_state()) -> boolean().
140+
is_bottom({?TYPE, {delta, GMap}}) ->
141+
is_bottom({?TYPE, GMap});
142+
is_bottom({?TYPE, {_Type, GMap}}) ->
143+
orddict:is_empty(GMap).
144+
138145
%% @doc Given two `state_gmap()', check if the second is an inflation
139146
%% of the first.
140147
%% Two conditions should be met:
@@ -234,6 +241,12 @@ equal_test() ->
234241
?assertNot(equal(Map1, Map2)),
235242
?assertNot(equal(Map1, Map3)).
236243

244+
is_bottom_test() ->
245+
Map0 = new(),
246+
Map1 = {?TYPE, {?GCOUNTER_TYPE, [{<<"key1">>, {?GCOUNTER_TYPE, [{1, 1}]}}]}},
247+
?assert(is_bottom(Map0)),
248+
?assertNot(is_bottom(Map1)).
249+
237250
is_inflation_test() ->
238251
Map1 = {?TYPE, {?GCOUNTER_TYPE, [{<<"key1">>, {?GCOUNTER_TYPE, [{1, 1}]}}]}},
239252
DeltaMap1 = {?TYPE, {delta, {?GCOUNTER_TYPE, [{<<"key1">>, {?GCOUNTER_TYPE, [{1, 1}]}}]}}},

src/state_gset.erl

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@
4242

4343
-export([new/0, new/1]).
4444
-export([mutate/3, delta_mutate/3, merge/2]).
45-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
45+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
4646
-export([join_decomposition/1]).
4747

4848
-export_type([state_gset/0, delta_state_gset/0, state_gset_op/0]).
@@ -115,6 +115,13 @@ merge({?TYPE, GSet1}, {?TYPE, GSet2}) ->
115115
equal({?TYPE, GSet1}, {?TYPE, GSet2}) ->
116116
ordsets_ext:equal(GSet1, GSet2).
117117

118+
%% @doc Check if a GSet is bottom.
119+
-spec is_bottom(delta_or_state()) -> boolean().
120+
is_bottom({?TYPE, {delta, GSet}}) ->
121+
is_bottom({?TYPE, GSet});
122+
is_bottom({?TYPE, GSet}) ->
123+
ordsets:size(GSet) == 0.
124+
118125
%% @doc Given two `state_gset()', check if the second is an inflation
119126
%% of the first.
120127
%% The second `state_gset()' is an inflation if the first set is
@@ -217,6 +224,12 @@ equal_test() ->
217224
?assert(equal(Set1, Set1)),
218225
?assertNot(equal(Set1, Set2)).
219226

227+
is_bottom_test() ->
228+
Set0 = new(),
229+
Set1 = {?TYPE, [<<"a">>]},
230+
?assert(is_bottom(Set0)),
231+
?assertNot(is_bottom(Set1)).
232+
220233
is_inflation_test() ->
221234
Set1 = {?TYPE, [<<"a">>]},
222235
DeltaSet1 = {?TYPE, {delta, [<<"a">>]}},

src/state_ivar.erl

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@
3535

3636
-export([new/0, new/1]).
3737
-export([mutate/3, delta_mutate/3, merge/2]).
38-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
38+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
3939
-export([join_decomposition/1]).
4040

4141
-export_type([state_ivar/0, delta_state_ivar/0, state_ivar_op/0]).
@@ -94,6 +94,13 @@ merge({?TYPE, Value}, {?TYPE, Value}) ->
9494
equal({?TYPE, Value1}, {?TYPE, Value2}) ->
9595
Value1 == Value2.
9696

97+
%% @doc Check if an IVar is bottom.
98+
-spec is_bottom(delta_or_state()) -> boolean().
99+
is_bottom({?TYPE, {delta, Value}}) ->
100+
is_bottom({?TYPE, Value});
101+
is_bottom({?TYPE, Value}) ->
102+
Value == undefined.
103+
97104
%% @doc Given two `state_ivar()', check if the second is and inflation
98105
%% of the first.
99106
%% The second `state_ivar()' is and inflation if the first set is
@@ -163,6 +170,12 @@ equal_test() ->
163170
?assert(equal(Var1, Var1)),
164171
?assertNot(equal(Var1, Var2)).
165172

173+
is_bottom_test() ->
174+
Var0 = new(),
175+
Var1 = {?TYPE, [<<"a">>]},
176+
?assert(is_bottom(Var0)),
177+
?assertNot(is_bottom(Var1)).
178+
166179
is_inflation_test() ->
167180
Var0 = new(),
168181
Var1 = {?TYPE, [<<"a">>]},

src/state_lexcounter.erl

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@
4242

4343
-export([new/0, new/1]).
4444
-export([mutate/3, delta_mutate/3, merge/2]).
45-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
45+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
4646
-export([join_decomposition/1]).
4747

4848
-export_type([state_lexcounter/0, delta_state_lexcounter/0, state_lexcounter_op/0]).
@@ -143,6 +143,13 @@ equal({?TYPE, LexCounter1}, {?TYPE, LexCounter2}) ->
143143
Fun = fun({Left1, Right1}, {Left2, Right2}) -> Left1 == Left2 andalso Right1 == Right2 end,
144144
orddict_ext:equal(LexCounter1, LexCounter2, Fun).
145145

146+
%% @doc Check if a LexCounter is bottom.
147+
-spec is_bottom(delta_or_state()) -> boolean().
148+
is_bottom({?TYPE, {delta, LexCounter}}) ->
149+
is_bottom({?TYPE, LexCounter});
150+
is_bottom({?TYPE, LexCounter}) ->
151+
orddict:is_empty(LexCounter).
152+
146153
%% @doc Given two `state_lexcounter()', check if the second is and
147154
%% inflation of the first.
148155
%% We have an inflation if, for every key present in the first
@@ -261,6 +268,12 @@ equal_test() ->
261268
?assertNot(equal(Counter1, Counter3)),
262269
?assertNot(equal(Counter1, Counter4)).
263270

271+
is_bottom_test() ->
272+
Counter0 = new(),
273+
Counter1 = {?TYPE, [{1, {2, 0}}, {2, {1, 2}}, {4, {1, 2}}]},
274+
?assert(is_bottom(Counter0)),
275+
?assertNot(is_bottom(Counter1)).
276+
264277
is_inflation_test() ->
265278
Counter1 = {?TYPE, [{<<"1">>, {2, 0}}]},
266279
DeltaCounter1 = {?TYPE, {delta, [{<<"1">>, {2, 0}}]}},

src/state_max_int.erl

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@
3838

3939
-export([new/0, new/1]).
4040
-export([mutate/3, delta_mutate/3, merge/2]).
41-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
41+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
4242
-export([join_decomposition/1]).
4343

4444
-export_type([state_max_int/0, delta_state_max_int/0, state_max_int_op/0]).
@@ -97,6 +97,13 @@ merge({?TYPE, Value1}, {?TYPE, Value2}) ->
9797
equal({?TYPE, Value1}, {?TYPE, Value2}) ->
9898
Value1 == Value2.
9999

100+
%% @doc Check if a Max Int is bottom.
101+
-spec is_bottom(delta_or_state()) -> boolean().
102+
is_bottom({?TYPE, {delta, Value}}) ->
103+
is_bottom({?TYPE, Value});
104+
is_bottom({?TYPE, Value}) ->
105+
Value == 0.
106+
100107
%% @doc Given two `state_max_int()', check if the second is an inflation
101108
%% of the first.
102109
%% The second is an inflation if its value is greater or equal
@@ -186,6 +193,12 @@ equal_test() ->
186193
?assert(equal(MaxInt1, MaxInt1)),
187194
?assertNot(equal(MaxInt1, MaxInt2)).
188195

196+
is_bottom_test() ->
197+
MaxInt0 = new(),
198+
MaxInt1 = {?TYPE, 17},
199+
?assert(is_bottom(MaxInt0)),
200+
?assertNot(is_bottom(MaxInt1)).
201+
189202
is_inflation_test() ->
190203
MaxInt1 = {?TYPE, 23},
191204
DeltaMaxInt1 = {?TYPE, {delta, 23}},

src/state_orset.erl

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@
3939

4040
-export([new/0, new/1]).
4141
-export([mutate/3, delta_mutate/3, merge/2]).
42-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
42+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
4343
-export([join_decomposition/1]).
4444

4545
-export_type([state_orset/0, delta_state_orset/0, state_orset_op/0]).
@@ -201,6 +201,13 @@ merge({?TYPE, ORSet1}, {?TYPE, ORSet2}) ->
201201
equal({?TYPE, ORSet1}, {?TYPE, ORSet2}) ->
202202
ORSet1 == ORSet2.
203203

204+
%% @doc Check if an ORSet is bottom.
205+
-spec is_bottom(delta_or_state()) -> boolean().
206+
is_bottom({?TYPE, {delta, ORSet}}) ->
207+
is_bottom({?TYPE, ORSet});
208+
is_bottom({?TYPE, ORSet}) ->
209+
orddict:is_empty(ORSet).
210+
204211
%% @doc Given two `state_orset()', check if the second is and inflation
205212
%% of the first.
206213
%% The second is an inflation if, at least, has all the elements
@@ -393,6 +400,12 @@ equal_test() ->
393400
?assertNot(equal(Set1, Set3)),
394401
?assertNot(equal(Set2, Set3)).
395402

403+
is_bottom_test() ->
404+
Set0 = new(),
405+
Set1 = {?TYPE, [{<<"a">>, [{<<"token1">>, true}]}]},
406+
?assert(is_bottom(Set0)),
407+
?assertNot(is_bottom(Set1)).
408+
396409
is_inflation_test() ->
397410
Set1 = {?TYPE, [{<<"a">>, [{<<"token1">>, true}]}]},
398411
DeltaSet1 = {?TYPE, {delta, [{<<"a">>, [{<<"token1">>, true}]}]}},

src/state_pair.erl

Lines changed: 18 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@
4545

4646
-export([new/0, new/1]).
4747
-export([mutate/3, delta_mutate/3, merge/2]).
48-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
48+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
4949
-export([join_decomposition/1]).
5050

5151
-export_type([state_pair/0, delta_state_pair/0, state_pair_op/0]).
@@ -138,6 +138,14 @@ equal({?TYPE, {{FstType, _}=Fst1, {SndType, _}=Snd1}},
138138
FstType:equal(Fst1, Fst2) andalso
139139
SndType:equal(Snd1, Snd2).
140140

141+
%% @doc Check if a Pair is bottom.
142+
-spec is_bottom(delta_or_state()) -> boolean().
143+
is_bottom({?TYPE, {delta, Pair}}) ->
144+
is_bottom({?TYPE, Pair});
145+
is_bottom({?TYPE, {{FstType, _}=Fst, {SndType, _}=Snd}}) ->
146+
FstType:is_bottom(Fst) andalso
147+
SndType:is_bottom(Snd).
148+
141149
%% @doc Check for `state_pair()' inflation.
142150
%% We have an inflation when both of the components are inflations.
143151
-spec is_inflation(delta_or_state(), state_pair()) -> boolean().
@@ -239,6 +247,15 @@ equal_test() ->
239247
?assertNot(equal(Pair1, Pair2)),
240248
?assertNot(equal(Pair3, Pair4)).
241249

250+
is_bottom_test() ->
251+
GCounter0 = ?GCOUNTER_TYPE:new(),
252+
GCounter1 = {?GCOUNTER_TYPE, [{1, 5}, {2, 10}]},
253+
GSet0 = ?GSET_TYPE:new(),
254+
Pair0 = {?TYPE, {GCounter0, GSet0}},
255+
Pair1 = {?TYPE, {GCounter1, GSet0}},
256+
?assert(is_bottom(Pair0)),
257+
?assertNot(is_bottom(Pair1)).
258+
242259
is_inflation_test() ->
243260
GCounter1 = {?GCOUNTER_TYPE, [{1, 5}, {2, 10}]},
244261
GCounter2 = {?GCOUNTER_TYPE, [{1, 7}, {2, 10}]},

src/state_pncounter.erl

Lines changed: 14 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -49,7 +49,7 @@
4949

5050
-export([new/0, new/1]).
5151
-export([mutate/3, delta_mutate/3, merge/2]).
52-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
52+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
5353
-export([join_decomposition/1]).
5454
-export([extract_delta/1]).
5555

@@ -153,6 +153,13 @@ equal({?TYPE, PNCounter1}, {?TYPE, PNCounter2}) ->
153153
Fun = fun({Inc1, Dec1}, {Inc2, Dec2}) -> Inc1 == Inc2 andalso Dec1 == Dec2 end,
154154
orddict_ext:equal(PNCounter1, PNCounter2, Fun).
155155

156+
%% @doc Check if a PNCounter is bottom.
157+
-spec is_bottom(delta_or_state()) -> boolean().
158+
is_bottom({?TYPE, {delta, PNCounter}}) ->
159+
is_bottom({?TYPE, PNCounter});
160+
is_bottom({?TYPE, PNCounter}) ->
161+
orddict:is_empty(PNCounter).
162+
156163
%% @doc Given two `state_pncounter()', check if the second is and inflation
157164
%% of the first.
158165
%% Two conditions should be met:
@@ -288,6 +295,12 @@ equal_test() ->
288295
?assertNot(equal(Counter1, Counter3)),
289296
?assertNot(equal(Counter1, Counter4)).
290297

298+
is_bottom_test() ->
299+
Counter0 = new(),
300+
Counter1 = {?TYPE, [{1, {2, 0}}, {2, {1, 2}}, {4, {1, 2}}]},
301+
?assert(is_bottom(Counter0)),
302+
?assertNot(is_bottom(Counter1)).
303+
291304
is_inflation_test() ->
292305
Counter1 = {?TYPE, [{1, {2, 0}}, {2, {1, 2}}, {4, {1, 2}}]},
293306
DeltaCounter1 = {?TYPE, {delta, [{1, {2, 0}}, {2, {1, 2}}, {4, {1, 2}}]}},

src/state_twopset.erl

Lines changed: 15 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@
4646

4747
-export([new/0, new/1]).
4848
-export([mutate/3, delta_mutate/3, merge/2]).
49-
-export([query/1, equal/2, is_inflation/2, is_strict_inflation/2]).
49+
-export([query/1, equal/2, is_bottom/1, is_inflation/2, is_strict_inflation/2]).
5050
-export([join_decomposition/1]).
5151

5252
-export_type([state_twopset/0, delta_state_twopset/0, state_twopset_op/0]).
@@ -128,6 +128,14 @@ equal({?TYPE, {Added1, Removed1}}, {?TYPE, {Added2, Removed2}}) ->
128128
ordsets_ext:equal(Added1, Added2) andalso
129129
ordsets_ext:equal(Removed1, Removed2).
130130

131+
%% @doc Check if a TwoPSet is bottom.
132+
-spec is_bottom(delta_or_state()) -> boolean().
133+
is_bottom({?TYPE, {delta, Set}}) ->
134+
is_bottom({?TYPE, Set});
135+
is_bottom({?TYPE, {Added, Removed}}) ->
136+
orddict:is_empty(Added) andalso
137+
orddict:is_empty(Removed).
138+
131139
%% @doc Given two `state_twopset()', check if the second is an inflation
132140
%% of the first.
133141
%% The second `state_twopset()' is an inflation if the first set
@@ -234,6 +242,12 @@ equal_test() ->
234242
?assert(equal(Set2, Set2)),
235243
?assertNot(equal(Set1, Set2)).
236244

245+
is_bottom_test() ->
246+
Set0 = new(),
247+
Set1 = {?TYPE, {[<<"a">>], []}},
248+
?assert(is_bottom(Set0)),
249+
?assertNot(is_bottom(Set1)).
250+
237251
is_inflation_test() ->
238252
Set1 = {?TYPE, {[<<"a">>], []}},
239253
DeltaSet1 = {?TYPE, {delta, {[<<"a">>], []}}},

0 commit comments

Comments
 (0)