У меня есть модель сплава в avlTree.als. В этой модели используется целочисленная арифметика, в частности, функции плюс и минус. В этой модели есть несколько утверждений, и я могу легко запустить их с помощью графического интерфейса Alloy Analyzer.
У меня есть другая модель сплава в test.als. Эта модель импортирует avlTree (используя «open avlTree»), а затем содержит некоторые утверждения об отношениях в модели avlTree. Но когда я пытаюсь запустить эти утверждения в графическом интерфейсе Alloy Analyzer, я получаю следующее сообщение:
Произошла синтаксическая ошибка:
Название "плюс" не найдено.
И ссылка на синтаксическую ошибку ведет меня к моей модели avlTree. Таким образом, кажется, что использование целочисленной математики в модели avlTree отлично работает, когда я запускаю эту модель саму по себе, но ломается, когда я пытаюсь импортировать ее в другую модель. Это можно как-то исправить?
У меня Alloy 4.2.
