Поведение противоречивых мягких ограничений

У меня есть тестовый пример, в котором поведение кажется неправильным. Я вижу, что во всех поколениях num_of_red_shoes высокое, хотя я ожидал бы более равномерного распределения. В чем причина такого поведения и как это можно исправить?

<'
struct closet {
    kind:[SMALL,BIG];

    num_of_shoes:uint;
    num_of_red_shoes:uint;
    num_of_black_shoes:uint;
    num_of_yellow_shoes:uint;

    keep soft num_of_red_shoes < 10;
    keep soft num_of_black_shoes < 10;
    keep soft num_of_yellow_shoes < 10;

    keep num_of_yellow_shoes + num_of_black_shoes + num_of_red_shoes == num_of_shoes;

    when BIG closet {
        keep num_of_shoes in [50..100];
    };
};

extend sys {
    closets[100]:list of BIG closet;
};
'>

Результаты генерации:

item   type        kind        num_of_sh*  num_of_re*  num_of_bl*  num_of_ye* 
---------------------------------------------------------------------------
0.     BIG closet  BIG         78          73          1           4           
1.     BIG closet  BIG         67          50          8           9           
2.     BIG closet  BIG         73          68          0           5           
3.     BIG closet  BIG         73          66          3           4           
4.     BIG closet  BIG         51          50          0           1           
5.     BIG closet  BIG         78          76          1           1           
6.     BIG closet  BIG         55          43          7           5           
7.     BIG closet  BIG         88          87          1           0           
8.     BIG closet  BIG         99          84          6           9           
9.     BIG closet  BIG         92          92          0           0           
10.    BIG closet  BIG         63          55          3           5           
11.    BIG closet  BIG         59          50          9           0           
12.    BIG closet  BIG         51          44          2           5           
13.    BIG closet  BIG         82          76          1           5           
14.    BIG closet  BIG         81          74          2           5           
15.    BIG closet  BIG         97          93          2           2           
16.    BIG closet  BIG         54          41          8           5           
17.    BIG closet  BIG         55          44          5           6           
18.    BIG closet  BIG         70          55          9           6           
19.    BIG closet  BIG         63          57          1           5

specman e
person SpecUser    schedule 22.07.2015    source источник

Ответы (4)


arrow_upward
3
arrow_downward

При наличии противоречащих друг другу мягких ограничений Specman не рандомизирует применяемые мягкие ограничения, а отдает приоритет ограничениям, которые были записаны последними. Поскольку мягкость на красных туфлях была первой в тесте, она всегда отменяется.

Если известно, что софты взаимоисключающие (в данном случае это не так), вы можете использовать простой флаг, чтобы случайным образом выбрать, какой софт должен храниться. например код будет выглядеть так:

flag:uint[0..2];

keep soft read_only(flag==0) => num_of_red_shoes < 10;
keep soft read_only(flag==1) => num_of_black_shoes < 10;
keep soft read_only(flag==2) => num_of_yellow_shoes < 10;

Однако, поскольку здесь заранее не известно, сколько софтов предполагается вместить (а возможно и два или все три будут удовлетворены), следует принимать более сложное решение. Вот код, который делает эту рандомизацию:

struct closet {
    kind:[SMALL,BIG];

    num_of_shoes:uint;
    num_of_red_shoes:uint;
    num_of_black_shoes:uint;
    num_of_yellow_shoes:uint;

    //replaces the original soft constraints (if a flag is true the correlating
    //right-side implication will be enforced
    soft_flags[3]:list of bool;
    keep for each in soft_flags {
        soft it == TRUE;
    };

    //this list is used to shuffle the flags so their enforcement will be done
    //with even distribution
    soft_indices:list of uint;
    keep soft_indices.is_a_permutation({0;1;2});

    keep soft_flags[soft_indices[0]] => num_of_red_shoes < 10;
    keep soft_flags[soft_indices[1]] => num_of_black_shoes < 10;
    keep soft_flags[soft_indices[2]] => num_of_yellow_shoes < 10;

    keep num_of_yellow_shoes + num_of_black_shoes + num_of_red_shoes == num_of_shoes;
};
person Reuven Naveh    schedule 23.07.2015

arrow_upward
1
arrow_downward

Я не с Каденс, так что не могу дать вам определенного ответа. Я думаю, что решатель попытается сломать как можно меньше ограничений и просто выберет первое, если найдет (в вашем случае для красных туфель). Попробуйте изменить порядок и посмотрите, изменится ли это (если первым будет черное ограничение, я думаю, вы всегда будете получать больше черных туфель).

В качестве решения вы можете просто удалить мягкие ограничения, когда у вас большой шкаф:

when BIG closet {
    keep num_of_red_shoes.reset_soft();
    keep num_of_black_shoes.reset_soft();
    keep num_of_yellow_shoes.reset_soft();
    keep num_of_shoes in [50..100];
};

Если вы хотите случайным образом выбрать, какой из них отключить (иногда более 10 красных ботинок, иногда более 10 черных ботинок и т. д.), вам понадобится вспомогательное поле:

when BIG closet {
    more_shoes : [ RED, BLACK, YELLOW ];

    keep more_shoes == RED => num_of_red_shoes.reset_soft();
    keep more_shoes == BLACK => num_of_black_shoes.reset_soft();
    keep more_shoes == YELLOW => num_of_yellow_shoes.reset_soft();
    keep num_of_shoes in [50..100];
};

Это зависит от того, что вы подразумеваете под «более равномерным распределением».

person Tudor Timi    schedule 22.07.2015

arrow_upward
1
arrow_downward

Невозможно удовлетворить все ваши жесткие и мягкие ограничения для БОЛЬШОГО шкафа. Поэтому Specman пытается найти решение, игнорируя некоторые из ваших мягких ограничений. Решатель ограничений IntelliGen не игнорирует все мягкие ограничения, а пытается найти решение, все еще используя подмножество. Это объясняется в «Руководстве пользователя поколения Specman» (sn_igenuser.pdf):

[S]мягкие ограничения, которые загружаются позже, считаются имеющими более высокий приоритет, чем мягкие ограничения, загруженные ранее».

В данном случае это означает, что Specman отбрасывает мягкое ограничение на красные туфли, и поскольку он может найти решение, все еще подчиняющееся другим мягким ограничениям, он их не отбрасывает.

Если вы объедините все свои мягкие ограничения в одно, то вы, вероятно, получите результат, на который надеялись:

 keep soft ((num_of_red_shoes    < 10) and (num_of_black_shoes < 10) and
            (num_of_yellow_shoes < 10));

Есть преимущества в предоставлении более поздним ограничениям приоритета: это означает, что с помощью АОП вы можете добавлять новые мягкие ограничения, и они получат наивысший приоритет.

person Hackonteur    schedule 23.07.2015

arrow_upward
1
arrow_downward

Для более распределенных значений я бы предложил следующее. Я уверен, что вы тоже можете следовать предполагаемой логике.

var1, var2 : uint;
keep var1 in [0..30];
keep var2 in [0..30];

when BIG closet {
    keep num_of_shoes in [50..100];
    keep num_of_yellow_shoes == (num_of_shoes/3) - 15 + var1;
    keep num_of_black_shoes == (num_of_shoes - num_of_yellow_shoes)/2 - 15 + var2;
    keep num_of_red_shoes == num_of_shoes - (num_of_yellow_shoes - num_of_black_shoes);

keep gen (var1, var2) before (num_of_shoes);
    keep gen (num_of_shoes) before (num_of_yellow_shoes, num_of_black_shoes, num_of_red_shoes);
    keep gen (num_of_yellow_shoes) before (num_of_black_shoes, num_of_red_shoes);
    keep gen (num_of_black_shoes) before (num_of_red_shoes);
};
person Mithun Guddethota    schedule 06.03.2017