specification exa4_9_P2[a,b,c] : exit

  behaviour

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

endspec