У меня есть следующий модуль Alloy и команда запуска:
sig A { x : set A }
run {all a: A| #a.x<3 and #a.x>1} for exactly 2 A, 2 int
С параметром «Запретить переполнение: нет» анализатор сплавов версии 4.2 (дата сборки: 25 сентября 2012 г.) не находит экземпляр. Я считаю, что причина в том, что из-за переполнения константы 3 предикат запуска читается как {all a: A| #a.x<-1 and #a.x>1}.
При выборе «Запретить переполнение: Да» анализатор сплавов находит экземпляр.
---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. Он не находит экземпляр. Такое поведение ожидаемо.
