如何生成尚不存在的列表？

Question

我有一个列表列表，我想生成一个不在旧列表中的新列表，如何自动执行此操作？

DB : list of list of uint;
generate_new_data() is {
    for i from 1 to 10 {
        var new_list : list of uint;
        gen new_list keeping {
           it.size() == n;
           it not in DB;
        };
        DB.add( new_list );
    };
};

新列表可以是旧列表的排列，我想在列表项中有不同的值，它可以是一个或全部不同（我希望这是随机的）

Answer 1

请考虑以下内容，如果两个列表不相等，则至少有一个位置的值不同。因此

l1 is different than l2  if and only if there exists a 'diff_at' such that l1[diff_at]!=l2[diff_at]

使用此方法，可以在单个 CFS 中生成整个数据库：

struct db_wrapper_s {
    DB : list of list of uint;
    diff_at : list of list of uint;
    keep DB.size() == diff_at.size();
    keep for each in diff_at {
        it.size() == index;
        for each in it {
            it < read_only(DB[index].size());
        };
    };
    keep for each (diff_i) using index (i) in diff_at {
        for each (diff_i_j) using index (j) in diff_i {
            DB[i][diff_i_j] != DB[j][diff_i_j];
        };
    };
};
generate_new_data() is {
    var genDB : db_wrapper_s;
    var db_sz : uint = 10;
    var l_sz : uint = 5;
    gen genDB keeping {
        it.DB.size() == read_only(db_sz);
        for each in it.DB {
            it.size() == read_only(l_sz);
        };
    };
    print genDB.DB;
};

上述问题是，如果数据库中的列表数量和列表大小很大，则可能会受到较长的求解时间的影响。

从 Specman 14.2 开始，随机生成器支持生成列表索引：

keep foo()[gen_var] == ... ;

（该功能在 14.2/15.1 中被禁用，需要通过"config gen -use_generative_list_index=TRUE"打开）。

使用此功能，您可以逐个列表构建数据库列表：

struct new_list_wrapper_s {
    new_list : list of uint;
    diff_at : list of uint;
};
!DB : list of list of uint;
generate_new_data() is {
    var n : uint = 5;
    for i from 1 to 10 {
        var new_list_wrapper : new_list_wrapper_s;
        gen new_list_wrapper keeping {
            it.diff_at.size() == read_only(DB.size());
            it.new_list.size() == read_only(n);
            for each (diff_loc) in it.diff_at {
                diff_loc < read_only(n);
                it.new_list[diff_loc] != read_only(DB[index])[diff_loc];
            };
        };
        DB.add( new_list_wrapper.new_list );
    };
    print DB;
};