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

Question

У меня есть тест, в котором поведение кажется неправильным. Я вижу, что во всех поколениях 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 

Answer 1

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

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

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

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

Answer 2

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

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

.

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

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

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

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

Answer 3

Когда есть противоречивые мягкие ограничения, Спецман не производит рандомизацию мягких программ, которые принудительно применяются, а скорее придает приоритет ограничениям, которые были записаны последним. Так как мягкие на красных туфлях были первыми в тесте, это тот, который всегда переопределяется.

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

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

Answer 4

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

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