変数の制約を一度設定し、specmanで数回生成できますか？

Question

同じ関数で数回、同じ制約のセットで生成したい変数があります。一度制約を設定し、何度もgenだけ設定できますか？つまり、これの代わりに：

var a:uint;
gen a keeping {it in [100..120];};
// some code that uses a
.
.
.
gen a keeping {it in [100..120];};
// some code that uses a
.
.
.
gen a keeping {it in [100..120];};
// some code that uses a
// etc...

これを行いたい：

var a:uint;
keep a in [100..120];
.
.
.
gen a;
// some code that uses a
.
.
.
gen a;
// some code that uses a
.
.
.
gen a;
// some code that uses a
// etc...

そのようにしてa sの制約を変更したい場合は、一度だけ行う必要があります。

Answer 1

これを行うには、変数を囲んでいるオブジェクトのインスタンスメンバーにします。

a : uint;
keep a in [100..120];
my_method()@qualified_clk_rise_e is {

    gen a;
    ...
    gen a;
    ...
    gen a; 
};

この実装は、複数のmy_method（）が同じオブジェクトで同時に実行されている場合、スレッドセーフではありません。生成された「a」を「my_a」に割り当てることにより、[specman]スレッドセーフにできます。 'メソッドのスコープ内：

var my_a : uint;
gen a;
my_a = a;

または「a」を生成するメソッドを書くことができます：

gen_a(): uint is {
    gen result keeping { it in [100..120] };
};

my_method()@qualified_clock_rise_e is {
    var a : uint;
    ...
    a = gen_a();
    ...
    a = gen_a();
    ...
    a = gen_a();
    ...
};