Как создать список, который еще не существует?

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;
};