specification exa4_1a[a,b] : exit

  behaviour

    P1[a,b]

  where

    process P1 [one, two] : exit :=

       one; two; exit

    endproc

endspec