1. A method for verifying whether a trace can be produced by a generator, comprising: receiving a specification for the generator, wherein the generator is a finite state machine that defines a set of inputs and outputs, and wherein the generator may contain parametric inputs to model non-determinism; receiving the trace, wherein the trace is a sequence of assignments of non-parametric inputs and outputs for the generator, and wherein the trace does not contain assignments of parametric inputs; using the specification to build a data structure that can be used to determine if a non-parametric input and output are consistent with the current state of the generator; and verifying elements of the trace, wherein verifying a given element involves using the data structure to determine if there exists any parametric input assignment that causes a match between non-parametric inputs and outputs of the generator with the ones specified in the given element of the trace.