Должен ли я иметь следы в «подмодулях» Alloy

Question

Это вопрос «передового опыта», а не вопрос о самом языке.

Я работаю над разбиением своего проекта на модули, следуя советам в книге Software Abstraction.У меня есть подписи, факты и предикаты для каждого маленького кусочка моей большой модели в отдельных файлах.Я правильно включил их в «основной файл».

Для нескольких небольших модулей я счел полезным «проверить» конструкцию, добавив следы на этом уровне.Трассировки - это просто факты, поэтому, когда я запускаю трассы, которые я создал в своем основном файле, я получаю странные результаты («два временных шага за раз» и т. Д.).

Я вижу два варианта (после любого из которых я могу просто завершить трассировки моего основного файла):

1. закомментировать трассировки в «подмодулях»
2. make«подмодуль» прослеживает чуть менее строгие ограничения, чтобы допустить возможность для ничего происходить

Выглядит ли что-нибудь из этого правильным?Или это обычно делается по-другому?

Answer 1

Одна из лучших вещей, которую я обнаружил при использовании Alloy, - это не использовать факты, а использовать предикаты.Вы можете контролировать, какие предикаты активны в прогоне или утверждать.Вы всегда можете комбинировать предикаты, чтобы не доставлять неудобств.