specification exa4_9_P1[a,b,c] : exit

  behaviour

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

endspec