Как заставить сплав работать с набором данных, чтобы проверить все правила

ИМХО, Alloy не подходит для анализа больших наборов данных.

При этом я считаю, что вы могли бы использовать aRby, встраивание Alloy на Ruby, который позволит вам не только заскриптовать импорт вашего набора данных, но и указать так называемые «частичные экземпляры», т.е. экземпляры, частично заполненные вашими данными, которые можно дополнить анализом.

Если вы предпочитаете использовать Java, вы можете работать напрямую с Alloy API (добавьте банку Alloy в путь сборки проекта).

Прежде чем начать, убедитесь, что масштабируемость не является ключевым требованием, поскольку оба подхода, безусловно, потребуют от вас определенного объема работы и самоотверженности при их реализации.

Я работал над правильным API для Alloy, в настоящее время он находится в PR. на Гитхабе. С этим API довольно легко использовать Alloy в качестве верификатора.

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

Понятно, что вы можете использовать и существующий API, но новый API предназначен для ваших и других целей. Понятно, что это незавершенная работа, но вы всегда можете связаться со мной, если возникнут проблемы.