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 := x−1, 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 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). 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. Design an algorithm that answers (yes/no) whether G is terminating or not.