Имам следния модул Alloy и стартирам команда:
sig A { x : set A }
run {all a: A| #a.x<3 and #a.x>1} for exactly 2 A, 2 int
С „Забрана на препълването: Не“ Alloy Analyzer 4.2 (дата на компилация: 2012-09-25) не намира екземпляр. Вярвам, че причината е, че поради препълването на константата 3 предикатът за изпълнение чете {all a: A| #a.x<-1 and #a.x>1}.
С "Forbid Overflow: Yes" Alloy Analyzer намира екземпляр.
---INSTANCE---
integers={-2, -1, 0, 1}
univ={-1, -2, 0, 1, A$0, A$1}
Int={-1, -2, 0, 1}
seq/Int={0}
String={}
none={}
this/A={A$0, A$1}
this/A<:x={A$0->A$0, A$0->A$1, A$1->A$0, A$1->A$1}
Alloy Evaluator ми казва, че предикатът {all a: A| #a.x<3 and #a.x>1}, използван в командата за изпълнение, се оценява на false.
Може ли някой да обясни това поведение? Има ли разлика в сематиката на целочислените сравнения в Оценителя и Анализатора?
Редактиране: Забелязах, че поведението е различно в най-новата експериментална версия: Alloy 4.2_2014-03-07. Не намира екземпляр. Това поведение е очаквано.
