ation is considered as progress during non- progress loop detection. Timer check level: 1: when verifying an MSC, 0 means that checking of timer events is not performed, 1 means that checking of timer events is performed, but a timer event can be missing in the MSC, and 2 means that checking of timer events is performed and that timer events in the SDL model and in the MSC must match exactly. MSC condition check: Off: conditions in MSC are ignored. Symbol time: Zero: if the SDL model is not blocked, a set timer cannot timeout. If set to undefined, as soon as a timer is set, it can be timed-out. Max state size: 100000: do not change. 8.1.9.9 Report actions The menu command Options1 > Report can be used to change the default actions after the detection of an event triggering a report. The default is Prune - Log one for each event. For example, by default, after reaching a state where the maximum number of signals in an input queue is exceeded, the simulation does not continue beyond this state (prune means cut), and backtracks to explore another state, if any. The other values are abort, meaning that the simulation will stop, or continue, meaning that the simulation will continue beyond this state and explore its successors. Log one means that even if the event occurs more than once, only one report will be generated. The other values are log all, where each occurrence of the event will generate a report, and log off, where no report is generated. Here is the list of reports sorted alphabetically, and their meaning: Assertion: the predefined procedure Report has been called (which calls the function xAs- sertError), generally from an observer process. See the observer process example. ChannelOutput: error in channel output, rarely used. Choice: error in CHOICE. Create: error in create. Deadlock: deadlock detected. Decision: error in a decision. ImplSigCons: implicit signal consumption, no input or save specified for a received signal. Import: error in import. Index: array index out of range. 278 Validation of Commu