3

動作が間違っているように見えるテストケースがあります。すべての世代で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
4

4 に答える 4

3

矛盾するソフト制約がある場合、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;

ただし、ここでは、いくつのソフトが保持されると予想されるかが事前にわかっていないため (2 つまたは 3 つすべてが満たされる可能性があります)、より複雑なソリューションを作成する必要があります。このランダム化を行うコードは次のとおりです。

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;
};
于 2015-07-23T18:06:19.267 に答える
1

私はケイデンスと一緒ではないので、明確な答えを出すことはできません. ソルバーはできるだけ少ない制約を破ろうとし、見つかった場合は最初の制約 (あなたの場合は赤い靴の制約) を選択するだけだと思います。順序を変更してみて、これが変わるかどうかを確認してください (黒の制約が最初にある場合は、常により多くの黒の靴が得られると思います)。

解決策として、大きなクローゼットがある場合は、ソフト制約を削除するだけです。

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

それは、「より均一な分布」が何を意味するかによって異なります。

于 2015-07-22T14:57:50.217 に答える
1

BIG クローゼットのハード面とソフト面の制約をすべて満たす方法はありません。したがって、Specman は、ソフト制約の一部を無視して解決策を見つけようとします。IntelliGen 制約ソルバーは、すべてのソフト制約を無視するわけではありませんが、サブセットを使用しながら解決策を見つけようとします。これについては、「Specman Generation ユーザー ガイド」(sn_igenuser.pdf) で説明されています。

[S]後でロードされるソフト制約は、以前にロードされたソフト制約よりも優先度が高いと見なされます。」

この場合、Specman は赤い靴のソフト制約を破棄し、他のソフト制約にまだ従っている解を見つけることができるため、それらを破棄しないことを意味します。

すべての柔軟な制約を 1 つに結合すると、おそらく期待どおりの結果が得られます。

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

後で制約を優先することには利点があります。これは、AOP を使用して新しいソフト制約を追加し、それらが最高の優先度を取得できることを意味します。

于 2015-07-23T11:39:22.233 に答える
1

より分散された値については、次のことをお勧めします。あなたも意図したロジックに従うことができると確信しています。

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);
};
于 2017-03-06T07:34:02.450 に答える