Understanding recursively defined error in NuSMV

I have a piece of code in NuSMV which has sprung an error. The code is:-

MODULE main
VAR
    x1: {a,b,c,d,e};
    x2: {a,b,c,d,e};
ASSIGN

    next(x1) := case
        x1=a & x2=c: e;

        x1=d & next(x2)=c : a;
        TRUE : x1;
    esac;
    next(x2) := case
            x1=b & x2=b: c;

            x2=d & next(x1)=e : e;
            TRUE : x2;
        esac;

So when I compile this in NuSMV, it gives an error: recursively defined: x1

Now I can easily take care of this error by removing next statements associated with x2 for the transition rule of x1, meaning I replace x1=d & next(x2)=c : a; with x1=d : a; or x1=d & x2=d : a;

I want to understand the mechanics of the NuSMV software which is causing the error and why the above fix resolves the error. I think it has got something to with synchronous implementation blah blah blah which I don't understand. Can someone give a precise detailed technical explanation?

And also explain why there is no error with variable x2. Its transition rules are aslo defined using the next operator.

Solution

It's much simpler than that.

You have a circular dependency, and the software cannot resolve that for you.

next(x1) := case
     ... & next(x2) : ...
esac;

next(x2) := case
     ... & next(x1) : ...
esac;

How is the computer (or a human being) supposed to decide the values of x1 and x2 in the next state, when deciding such assignments requires knowing the answers in advance?

You violated the so-called circular dependency rule, as indicated in the docs, section 2.3.8

Rules for assignments

Assignments describe a system of equations that say how the FSM evolves through time. With an arbitrary set of equations there is no guarantee that a solution exists or that it is unique. We tackle this problem by placing certain restrictive syntactic rules on the structure of assignments, thus guaranteeing that the program is implementable.

The restriction rules for assignments are:

The single assignment rule – each variable may be assigned only once.

The circular dependency rule – a set of equations must not have “cycles” in its dependency graph not broken by delays.

[...]

If we have an assignment like x := y ;, then we say that x depends on y. A combinatorial loop is a cycle of dependencies not broken by delays. For instance, the assignments:
x := y;
y := x;
form a combinatorial loop. Indeed, there is no fixed order in which we can compute x and y, since at each time instant the value of x depends on the value of y and vice-versa We can introduce a “unit delay dependency” using the next() operator.
      x := y;
next(y) := x;
In this case, there is a unit delay dependency between x and y. A combinatorial loop is a cycle of dependencies whose total delay is zero. In NUSMV combinatorial loops are illegal. This guarantees that for any set of equations describing the behavior of variable, there is at least one solution.

[...]

You ask:

[...] why the above fix resolves the error.

It fixes the error because it breaks the combinatorial loop. After the change, the software still needs to compute the future value of x1 in order to compute the future value of x2. However, to compute the future value of x1 now it no longer needs to know the future value of x2 (or any other unavailable information, for all that matters), so it can resolve both assignments.

You ask:

And also explain why there is no error with variable x2. Its transition rules are aslo defined using the next operator.

Both assignments on x1 and x2, taken independently, are perfectly legal. However, the error is not on a single assignment but rather on the combination of these two assignments. Since there is only one circular dependency, involving two variables, the error gets reported only once as soon as it is spotted. So it doesn't really matter whether you fix it by changing the assignment over x1 or that over x2, as long as there no longer is a cycle in the dependency graph.