У меня есть следующая очень простая модель в Alloy:
abstract sig Object {}
pred show(){}
run show for 5
когда я выполняю эту модель, почему анализатор сплавов по-прежнему создает экземпляр Object, хотя он определен как абстрактный!
sig является абстрактным, но анализатор сплава делает его экземпляр
Ответы (1)
Абстрактная подпись может содержать атомы, если у нее нет субсигнатур. Это сделано для того, чтобы вы могли постепенно строить и анимировать модель, поэтому вы можете пометить сигнатуру как абстрактную, ожидая, что субсигнатуры будут введены позже.
person
Daniel Jackson
schedule
07.12.2014
