Validator Block

'libs/contract/contract_callback.m'

This function controls the mask of the validator block. It does the following:

• Reads the parameters inserted by the user (assume ports, guarantee ports, mode ports, and the checkbox for creating inports automatically).
• Compares the number of ports with previous values and increases/decreases the number of ports accordingly.
• Generates new assume, guarantee, require, ensure, and mode blocks if necessary and connects them.
• Create inports if the create Inports Checkbox is enabled.
• Call saveValidatorParameters to save the current parameters.

'libs/contract/saveValidatorParameters.m'

This function is used by contract_callback to detect the changes made by the user for the mask parameters of the validator. It stores the number of assume ports, guarantee ports, mode Ports. It also stores the ports connectivity and port handles.

'libs/contract/contract.m'

This is the MATLAB S-Function for the validator block. This function plays no role in the verification, however it simulates the validator behavior at run time. The function does the following:

• Reads the assume, guarantee, and mode ports during the setup step.
• Allocates a temporary Boolean variable block.Dwork(1) to hold the result of sofar.
• Initializes the temporary variable block.Dwork(1) with true during the start step.
• Update block.Dwork(1) during the update step so that block.Dwork(1) = The conjunction of block.Dwork(1) and the current simulated values of assume ports.
• Computes the output value of the validator outport valid following the formulas in contract semantics during the Outputs step.