Missing validation on call sequences

[joeseibel]

In section 5.2, (L3) states, "Only one subprogram call sequence can apply to a given mode." This is not validated and the following model should produce an error:

thread implementation t.i
  calls
    sequence1: {
      call1: subprogram sp;
    };
    sequence2: {
      call2: subprogram sp;
    };
end t.i;