Выполнение команды управления с ограничением количества подписей в сплаве

Question

Первый код, не удалось найти ни одного экземпляра в Alloy Analyzer 4.2, но второй - хорошо! В чем отличия? Мое ожидание состоит в том, что #> 0 и # = 1 действуют как одно и то же, когда я выполняю «run show for 1».

1:

sig Fruit {} 
pred show() { #Fruit > 0} 
run show for 1 

2:

sig Fruit {} 
pred show() { #Fruit = 1} 
run show for 1 

Answer 1

При запуске команды вы увидите, что битовой (который определяет максимальную Int для сплава) 0.

Executing "Run show for 1" 

    Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 
    0 vars. 0 primary vars. 0 clauses. 2ms. 
    No instance found. Predicate may be inconsistent. 0ms. 

Вы можете изменить это путем явного изменения ширины полосы:

sig Fruit {} 
pred show() { #Fruit>0} 
run show for 1 but 2 int 

Executing "Run show for 1 but 2 int" 
    Solver=sat4j Bitwidth=2 MaxSeq=1 SkolemDepth=1 Symmetry=20 
    1 vars. 1 primary vars. 1 clauses. 3ms. 
    . found. Predicate is consistent. 3ms. 

Я думаю, что при использовании оператора '>' вам потребуется битрейт, но когда вы используете '=', это не требуется.

Работа с Int действительно обескураженный в сплаве.