As we talked in class, a program with two integer variables is universal. Now, we consider a special form of four variableprograms. Let G = (V; E) be a directed graph, where V is a finite set of nodes, and E ⊆V X V be the set of (directed) edges (arcs). In particular, we identify a node as the initial node, and a node as the final node. Let x1; x2; x3; x4 be four non-negative integer variables. Further, we decorate each edge with one of the following instructions: (1 ≤i≤ 4)

xi:= xi + 1;

xi:= 0;

xi == c? (c is a non-negative integer)

The result is called a decorated graph (we still use G to denote it). The semantics of a decorated graph is straightforward. It executes from the initial node with x1; x2; x3; x4 being 0, then walks along the graph. G can walk an edge (v, v') if all of the following conditions are satisfied: for each 1 ≤i≤4,

• if the edge is decorated with instruction xi:= xi + 1 for some i, the new value of xi is one more than the old value, and all the other xj(j ≠i) is unchanged.
• if the edge is decorated with instruction xi:= 0, the new value of xi is set to 0, and all the other xj (j ≠i) is unchanged.
• if the edge is decorated with instruction xi == c?, the value of xi must be c.

If at a node, G has more than one edge that can be walked, then G non-deterministically chooses one. If at a node G has no edge that can be walked, then G crashes (i.e., do not walk any further). We say that a decorated graph G is terminating if G can walk from an initial node to a final node and at the final node the values of x1; x2; x3; x4 satisfy the following constraint:

x1 = x2 = x3 = x4:

Show me an algorithm that answers (yes/no) whether G is terminating or not. (To correct a common misunderstanding, I shall point out that a walk could be arbitrarily long even though there are only 10 nodes in the graph! So, don't even try depth/breadth first search.)