Previous: , Up: Using Verum-Dezyne   [Contents][Index]


4.3 Component Simulator

Input for the component simulator is a trace of events of a single component and its ports; such a trace is either a witness of a verification error, or a hand-crafted use case description. The simulator interprets the trace, using the Dezyne semantics, and outputs a more detailed trace, where the state of the component and its interfaces is included. It also outputs a list of ’eligible’ events: events that are a valid extension of the input trace.