specification exa4_6[a,b] : exit

  behaviour

    a; i; i; b; exit
    ||
    i; a; i; b; exit

endspec