specification exa4_3[a,b,c] : exit

  behaviour

    P1[a,b]
    []
    P1[a,c]

  where

    process P1 [one, two] : exit :=

       one; two; exit

    endproc

endspec