Оптимизация общего заказа в Alloy и Kodkod

Об этом говорится в разных местах (например, здесь in-the-usu"> введите здесь описание ссылки или здесь), что отношение общего порядка запрограммировано для повышения эффективности анализа (и для того, чтобы имена атомов отображались в «естественном» порядке).

Насколько я понимаю, оптимизация сделана в Кодкоде (в этом фрагменте кода). Тем не менее, есть ли статья или документ, объясняющий более подробно (чем документация Java, которая говорит в терминах булевых матриц и не предоставляет аргументацию для алгоритма - что хорошо в документации исходного кода -) оптимизации, сделанные в Кодкод? Насколько я понимаю, в диссертации Э. Торлака о них ничего не сказано (в статье И. Шляхтера говорится о других оптимизациях, но я не знаю, реализованы ли они в Кодкоде или в Alloy).


person Grayswandyr    schedule 21.11.2016    source источник


Ответы (1)


Эта оптимизация сделана в Кодкоде, в месте кода, которое вы нашли. Это кратко описано в кандидатской диссертации Ильи Шляхтера (стр. 111, Раздел 4.5.5).

person emina    schedule 22.11.2016