Как работает рекурсия в Alloy Analyzer?

Question

Я вижу, что в анализаторе сплавов есть возможность разрешить рекурсию до определенной глубины (1-3).

Но что происходит, когда контрпример не может быть найден из-за ограниченной глубины рекурсии?

Будет ли ошибка или предупреждение, или такие контрпримеры молча игнорируются?

Answer 1

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

Это, imho, одно из самых слабых мест в Alloy.Рекурсия чрезвычайно важна практически во всех спецификациях.