A circularity error occurs if there is a cycle of zero-delay assignments amongst the union of all assignments in all layers. Thus for example, the following program:
layer Q : {
x := y;
}
layer P : {
y := x;
next(x) := y;
}
P refines Q;
is erroneous, even though it is functionally equivalent to the
non-circular program:
y := x;
next(x) := y;