A program with two integer variables are universal. Now, we consider a spcial form of two variable programs. Let G = (V,E) be a directed graph, where V is a finite set of nodes, and E V 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 x and y be two non-negative integer variables. Further, we decorate each edge with one of the following instructions: x := x + 1; x := x - 1; x == 0?; y := y + 1; y := y - 1; y == 0?; 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 x and y being 0, then walks along the graph. G can walk an edge (v, v') if all of the following conditions are satisfied:

• if the edge is decorated with instruction x := x+1, the new value of x is one more than the old value, and y is unchanged.
• if the edge is decorated with instruction x := x 1, the new value of x must be non-negative and is one less than the old value, and y is unchanged.
• if the edge is decorated with instruction x == 0?, the value of x must be 0.
• the case for instructions y := y + 1,y := y 1,y == 0? are similar.

If at a node, G has more than one edge that can be walked, then G nondeterministically 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 further require that each variable behaves as follows: a number of increments followed by a number of decrements but after that, it will NOT be incremented again. We say that a decorated graph G is terminating if G can walk from an initial node to a final node. Show me an algorithm that answers (yes/no) whether G is terminating or not.