Erlang中基于模型的属性测试多次运行后失败的排查求助

我在Erlang环境开发基于属性的测试生成器，普通属性测试全部完成且通过，但基于模型的属性测试运行数次后失败。以下是相关代码和失败输出，请求协助排查解决：

模型属性测试代码 #

prop_delete_model() ->
    ?FORALL({K, T}, {atom_key(), bst(atom_key(), int_value())},
        case model_delete(K, model(T)) of
            [] when T =:= leaf -> T =:= leaf;  % Handle the case where the tree is empty
            ModelResult -> equals(delete(K, T), ModelResult)
        end).

-spec model_delete(Key, [{Key, Value}]) -> [{Key, Value}].
model_delete(_, []) -> [];
model_delete(K, [{K, _} | Rest]) -> model_delete(K, Rest);
model_delete(K, [Head | Rest]) -> [Head | model_delete(K, Rest)].

prop_union_model() ->
    ?FORALL({T1, T2}, {bst(atom_key(), int_value()), bst(atom_key(), int_value())},
        equals(union(T1, T2), model_union(model(T1), model(T2)))).

-spec model_union([{Key, Value}], [{Key, Value}]) -> [{Key, Value}].
model_union([], T2) -> T2;
model_union(T1, []) -> T1;
model_union([{K, V1} | Rest1], T2) ->
    case find(K, T2) of
        {found, _} -> [{K, V1} | model_union(Rest1, delete(K, T2))];
        nothing -> [{K, V1} | model_union(Rest1, T2)]
    end.

delete与union业务函数代码 #

delete (_K, leaf) -> leaf;
delete (K, {branch, L, Key, V, R}) ->
  if K < Key    -> {branch, delete(K, L), Key, V, R};
     K > Key    -> {branch, L, Key, V, delete(K, R)};
     K =:= Key  -> join(L, R)
  end.

union (leaf, R) -> R;
union (L, leaf) -> L;
union ({branch, L, K, V, R}, T) ->
  {branch, union(L, below(K, T)), K, V, union(R, above(K, T))}.

测试失败输出 #

prop_delete_model: .......Failed! After 7 tests.
{g,{branch,leaf,c,-1,leaf}}
   {branch, leaf, c, -1, leaf} /= [{c, -1}]
Shrinking .x..(3 times)
{a,{branch,leaf,a,0,leaf}}
   leaf /= []
prop_union_model: Failed! After 1 tests.
{leaf,leaf}
   leaf /= []

问题分析与修复 #

核心问题 #

测试断言直接对比业务函数返回的BST结构和模型返回的键值对列表，两者类型完全不匹配，导致断言失败。比如：

• delete删除唯一节点后返回leaf，但模型返回[]
• union(leaf, leaf)返回leaf，但模型返回[]

修复步骤 #

1. 统一断言的对比格式

将业务函数的输出转换为模型格式（键值对列表）后再与模型结果对比，修改两个测试用例：

修改prop_delete_model

prop_delete_model() ->
    ?FORALL({K, T}, {atom_key(), bst(atom_key(), int_value())},
        equals(model(delete(K, T)), model_delete(K, model(T)))).

（注：假设model/1函数可正确将BST转为键值对列表，比如model(leaf)返回[]，model({branch, leaf, a, 0, leaf})返回[{a,0}]）

修改prop_union_model

prop_union_model() ->
    ?FORALL({T1, T2}, {bst(atom_key(), int_value()), bst(atom_key(), int_value())},
        equals(model(union(T1, T2)), model_union(model(T1), model(T2)))).

2. 修复model_union中的错误调用

model_union处理的是键值对列表，但原代码中调用了业务函数delete(K, T2)（该函数操作BST结构），应替换为模型的删除函数model_delete(K, T2)：

-spec model_union([{Key, Value}], [{Key, Value}]) -> [{Key, Value}].
model_union([], T2) -> T2;
model_union(T1, []) -> T1;
model_union([{K, V1} | Rest1], T2) ->
    case lists:keyfind(K, 1, T2) of
        {K, _V2} -> [{K, V1} | model_union(Rest1, model_delete(K, T2))];
        false -> [{K, V1} | model_union(Rest1, T2)]
    end.

（注：若原find/2是自定义的列表查找函数，可保留，否则用lists:keyfind更简洁）

验证要点 #

• 确认model/1函数的正确性：必须准确映射BST结构到键值对列表
• 测试join/2函数：删除节点时的合并逻辑需保证生成合法的BST，避免后续测试出现其他问题

内容的提问来源于stack exchange，提问作者Arraytics New