Description
In the current state of smbf, parametric bug patterns can have sets of fields (i.e. sets of values that appear in a message). For instance, let's take a look at wrong_certificate_type.dot from the dtls/client catalogue:
init -> certreq [label="I_CERTIFICATE_REQUEST[CTset:=cert_type]"]
init -> init [label="other"]
certreq -> certreq [label="other"]
certreq -> bug [label="O_CERTIFICATE[kt:=key_type] where cert_type(kt) !in CTset"]
Here we keep a set of field values which appear in I_CERTIFICATE_REQUEST and go to certreq state when this message is produced. Then, iff a parametric O_CERTIFICATE is produced whose field is not one of the values in I_CERTIFICATE_REQUEST's set we go to the bug state.
The question is: why does it have to be a set? And also what message sequence could fill in the set with more than one value? In the code this set is always instantiated with a single value and I do not see how a set could be formed from the messages of a Mealy machine. What I understand is that when ONE parametric I_CERTIFICATE_REQUEST is produced, this transition is triggered and then if one parametric O_CERTIFICATE (with a different parametric value) is produced then we catch a bug.
Could anyone present a different rationale about how sets are needed in this bug pattern?