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 B be two non-negative integer variables. Further, we decorate each edge with one of the following four instructions:

x := x + 1;

x := x 1;

x == 0?;

x == B?;

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 some non-negative values of B and x (satisfying 0 x B), then walks along the graph. G can walk an edge (v,v0) if all of the following conditions are satisfied:

if the edge is decorated with instruction x := x+1, the new value of x must satisfy 0 x B.

if the edge is decorated with instruction x := x1, the new value of x must satisfy 0 x B.

if the edge is decorated with instruction x == 0?, the value of x must be 0.

if the edge is decorated with instruction x == B?, the value of x must equal the value of B.

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). It is noticed that B can not be changed during any walk. However, its initial value can be any non-negative integer. We say that a decorated graph G is terminating if there are nonnegative initial values for B and x (satisfying 0 x B) such that 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.