Write UCLID5 code to complete the following task.

> Regard the program graph for the instructions A and B of the parallel program below, where action A is on the left of the ||| and action B is on the right: x:=2*x ||| x:=x+1 We assume that initially x=3. Build a model of this transition system, with a shared variable and two actions that act on the same shared variable x. Use the variable name x.

Reply with your UCLID5 code inside one unique code block.

I can definitely do that! Here is the UCLID5 code:
```
