Actually, the program has a causality problem since the clocks are not uniquely determined. At first, the clock constraint cannot be satisfied with the definition of y and the given input stream for input a as it is discussed in part b). However, there is another problem concerning causality. For the discussion, we may focus on the following subset of the equations and I will write X for absent values:
x := z $init 1
y := 0 cby pre(a)
z := y default x
y ^= aWith input a and the definition y := 0 cby pre(a) or y := 0 fby pre(a), the stream y is completely determined: First considering y := 0 cby pre(a), we get
a = 1 3 X 4 X X 2 X 7 8
b = X 5 X X 2 X X 7 X 6
y = 0 ⊥ 1 3 X 4 X X 2 X 7 8More difficult are the definitions of x and z which determine each other. By definition z := y default x, we know that whenever y has a present value, that will also be the value of z, and otherwise, we fetch the value from x at that moment. Hence, we have the following values for z for sure
a = 1 3 X 4 X X 2 X 7 8
b = X 5 X X 2 X X 7 X 6
y = 0 ⊥ 1 3 X 4 X X 2 X 7 8
z = 0 ⊥ 1 3 4 2 7 8
By definition x := z $init 1, the clock of x must be the clock of z, and therefore either both have present values or none of them may have a present value. We start with an initial value of 1 and then emit the values of z in the same order whenever z is present next. That starts as follows
a = 1 3 X 4 X X 2 X 7 8
b = X 5 X X 2 X X 7 X 6
y = 0 ⊥ 1 3 X 4 X X 2 X 7 8
z = 0 ⊥ 1 3 4 2 7 8
x = 1 0 ⊥ 1
Looking at the first not yet determined value of z, we are in trouble: The value should be the same as the value of x, and x should emit at the next point of time where z is present value 3. If we would say that the next value shall be present, then x would have value 3 and z must then also have that value. However, we may also say that x is not present and then also z will not be present which will also satisfy all the equations.
The same problem also occurs when using the definition of y := 0 fby pre(a), then we get
a = 1 3 X 4 X X 2 X 7 8
b = X 5 X X 2 X X 7 X 6
y = 0 1 3 X 4 X X 2 X 7 8
z = 0 1 3 4 2 7 8
x = 1 0 1
The program therefore requires a clock constraint to work properly. A possible clock constraint would by z ^= y which would then determine the clocks of x and z as the clock of y. If we use that clock constraint, we would get the following for y := 0 cby pre(a)
a = 1 3 X 4 X X 2 X 7 8
b = X 5 X X 2 X X 7 X 6
y = 0 ⊥ 1 3 X 4 X X 2 X 7 8
z = 0 ⊥ 1 3 X 4 X X 2 X 7 8
x = 1 0 ⊥ 1 X 3 X X 4 X 2 7and using y := 0 fby pre(a), we would get
a = 1 3 X 4 X X 2 X 7 8
b = X 5 X X 2 X X 7 X 6
y = 0 1 3 X 4 X X 2 X 7 8
z = 0 1 3 X 4 X X 2 X 7 8
x = 1 0 1 X 3 X X 4 X 2 7
The other streams are simply determined by their definitions in terms of the above streams.
So, what is now a correct solution? There are many correct solutions, since the program does not determine unique streams.
You can also argue with the clocks of x and z: If y is absent, then z should equal x, but x will be present if and only if z is present. Hence, if y is absent then either both x and z are both present or x and z are both absent. In the streams shown in part a), the solutions were both present, but that is not the only possible solution. The program therefore requires further clock constraints like z ^= y which will then enforce that if y is absent then also x and z are both absent.
