SPECIFICATION Spec
\* Add statements after this line.
CONSTANTS Val = {v1}
          Address = {a1, a2, a3} \* , a4}
          Dummy = a1
          Procs = {p1, p2} \* , p3}
          null = null