alloy - 合金でコマンドスコープを実行する

Question

In alloy consider

sig Queue{ link : Queue, elem: Int }

consider that I have some predicate predicate-1, How would I define scope when I run predicate-1 for Queue <=1 , int ={-3,-2,0,2}. I have not listed the predicate here

run predicate-1 for 1 Queue, int scope here

don't know what would be the syntax for int scope

Answer 1

構文は次のとおりです。

run predicate1 for 1 Queue, 3 Int

整数のスコープは常にビット幅であるため、Int セットに正確に {-3. -2. 0.2}; ビット幅のみを指定でき、そのビット幅内のすべての整数が使用されます。上記の例では、Int セットには -4 から 3 までのすべての整数が含まれます。