31
31
-define (ACTOR , oneof ([a , b , c ])).
32
32
-define (L (T ), list ({T , ? ACTOR })).
33
33
34
+ % % primitives
35
+ -define (TRUE , true ).
36
+
34
37
% % counters
35
38
-define (INC , increment ).
36
39
-define (DEC , decrement ).
43
46
-define (ADDRMV , oneof ([? ADD , ? RMV ])).
44
47
45
48
49
+ % % primitives
50
+ prop_boolean_decomposition () ->
51
+ ? FORALL (L , ? L (? TRUE ),
52
+ check_decomposition (create (? BOOLEAN_TYPE , L ))).
53
+ prop_boolean_redundant () ->
54
+ ? FORALL (L , ? L (? TRUE ),
55
+ check_redundant (create (? BOOLEAN_TYPE , L ))).
56
+
57
+ prop_max_int_decomposition () ->
58
+ ? FORALL (L , ? L (? INC ),
59
+ check_decomposition (create (? MAX_INT_TYPE , L ))).
60
+ prop_max_int_redundant () ->
61
+ ? FORALL (L , ? L (? INC ),
62
+ check_redundant (create (? MAX_INT_TYPE , L ))).
63
+
64
+
65
+ % % counters
46
66
prop_gcounter_decomposition () ->
47
67
? FORALL (L , ? L (? INC ),
48
68
check_decomposition (create (? GCOUNTER_TYPE , L ))).
@@ -57,6 +77,7 @@ prop_pncounter_redundant() ->
57
77
? FORALL (L , ? L (? INCDEC ),
58
78
check_redundant (create (? PNCOUNTER_TYPE , L ))).
59
79
80
+ % % sets
60
81
prop_gset_decomposition () ->
61
82
? FORALL (L , ? L (? ADD ),
62
83
check_decomposition (create (? GSET_TYPE , L ))).
@@ -78,6 +99,13 @@ prop_awset_redundant() ->
78
99
? FORALL (L , ? L (? ADDRMV ),
79
100
check_redundant (create (? AWSET_TYPE , L ))).
80
101
102
+ prop_orset_decomposition () ->
103
+ ? FORALL (L , ? L (? ADDRMV ),
104
+ check_decomposition (create (? ORSET_TYPE , L ))).
105
+ prop_orset_redundant () ->
106
+ ? FORALL (L , ? L (? ADDRMV ),
107
+ check_redundant (create (? ORSET_TYPE , L ))).
108
+
81
109
% % @private
82
110
check_decomposition ({Type , _ }= CRDT ) ->
83
111
Bottom = state_type :new (CRDT ),
0 commit comments