specification exa4_8_P2[a,b] : exit

  behaviour

    a;
     (b; exit
      []
      b; exit )

endspec