specification exa4_8_P1[a,b] : exit

  behaviour

    a; b; exit
    []
    a; b; exit

endspec