How does recursion work in the Alloy Analyzer?

I see there is an option in the Alloy Analyzer to allow recursion up to a certain depth (1-3).

But what happens when a counterexample cannot be found because of the limited recursion depth?

Will there be an error or a warning, or are such counterexamples silently ignored?

Solution

Alloy basically does not support recursion. When it encounters recursion, it unrolls the code the max number of times. Therefore, if it cannot found a solution, it just, well, cannot find a solution. If it could only generate an error if it knew there was a potential solution, which would solve the original problem.

This is, imho, one of the weakest spots in Alloy. Recursion is extremely important in almost all specifications.

algorithm using recursive function
Different behaviour of recursion-based powerset in C and Python
Why do I get a recursion error when the depth of the expected recursion should be way less than 999?
Using JavaScript what's the quickest way to recursively remove properties and values from an object?
Is there a way to achieve currying with a local variable
In C++, how can we write a recursive function that returns a range?
Understanding the Time Complexity Difference of Two Ways to Generate Subsets
How to implement a recursive factorial function without using the multiplication operator?
How to fully understand and implement a recursive factorial function?
pgrep -P, but for grandchildren not just children
Creating Internal Loops Dynamically
Convert a python non-tail recursive function adding sub-folders info to a loop
How to write a resillient object oriented method for SQL Update Table with retry in catch
c# find max value recursive (fastest)
Recursive regex pattern not matching all characters as expected (PHP differs from Perl implementation)
Recursive functions in R to apply regex within nested parentheses
Build a tree / run recursive query in Kusto Azure Data Explorer
Python: Maximum recursion depth exceeded
Retrieve last state of model inside model itself?
Explanation of lists:fold function
Importing file, recursive function and infinite loop in Lua
Runtime Error Hangup(SIGHUP) for recursion solution to sum of series problem
Finding "crossover" index with modified binary search algorithm in Python
How to implement tree made from possible moves in game Othello (Reversi)
How can I export a recursive directory & file listing to a text file in Linux Bash shell with an SSH command?
Change recursive into iterative function
Recursively convert all keys from camelCase to snake_case
Recursively change case and append a character to all keys and values of a multidimensional array
How can you determine if a number is sum of some squared numbers?
Is it possible to iterate through a binary tree using iteration instead of recursion?