Menus

Menu classes

CocosimMenu

The main menu for CoCoSim which is displayed under Tools menu in Simulink. The menu has the following options:

• verify
• Create Property:
• Verify using ...
• Simplifier
• Compiler Validation (Experimental)
• Compile (Experimental)
• Check unsupported blocks
• Preferences

VerificationMenu

VerificationMenu is a class that has the following static functions:

• verify: starts the verification process using the options selected in preferences. It calls the function cocosim_window the current model.

• verifyUsing: Works with Lustre Compiler and Lustre Verifier. This menu allows the user to specify which model checker to be used in the backEnd. Currently it supports (Kind2, Zustre, and JKind).

• displayHtmlVerificationResults: see below.

• compositionalOptions: see below.

ValidationMenu

[to be completed]

UnsupportedBlocksMenu

[to be completed]

PropertyGenerationMenu

[to be completed]

PreprocessingMenu

[to be completed]

CocosimWindowMenu

[to be completed]

PreferencesMenu

All functions related to the preferences menu are located inside the folder src/preferences.

• PreferncesMenu class contains the static functions (getMiddleEnd, getCompositionalAnalysis, getKind2Binary, getVerificationTimeout) which corresponds to menu items described here. These functions updates a variable called CoCoSimPreferences which is stored in src/preferences/preferences.mat.

• loadCoCoSimPreferences function loads preferences from the src/preferences/preferences.mat and creates defaults preferences if this file is missing.

PreContextMenu

This menu is invoked when the user right clicks on an empty space in the model.

The menu has the following options:

VerificationMenu.displayHtmlVerificationResults

This menu item appears after verification is finished, and displays verification results as HTML page. Its call back does the following:

• Reads the verification results stored in the model workspace.
• Reads the HTML template file src/backEnd/verification/cocoSpecVerify/utils/htmlverificationResultsTemplate.html
• Replaces [(verificationResults)] in the template with the json encoding of the verification results, and [(modelPath)] with the path of the model, and saves the new HTML into a temporary file.
• Adds the requierd css and js files to the temporary folder.
• Opens the html file using MATLAB Web browser.

VerificationMenu.compositionalOptions

This menu item appears after verification is finished. It displays the analyses performed by Kind2 for verification as check boxes and groups them by the name of the top subsystem (node). The check boxes in a group act as radio buttons (MATLAB doesn't supports radio buttons in Simulink menus). When a specific analysis is selected by the user, the model is changed to display the result of that analysis. This is achieved by calling the function displayVerificationResults.

MiscellaneousMenu.replaceInportsWithSignalBuilders

This menu item replaces the current inports of the diagram with string builders to enable the user to test the behavior of the model using specific input values. It does so as follows:

• Reads the inport blocks in the top diagram.
• Reads the type of each inport after compiling the model.
• Disconnects inports from other blocks.
• Removes inport blocks.
• Adds a signal builder to each inport. Adds conversion blocks for signal builders to match the inport type because signal builders always generate signals of type double.
• Connects the signal builders with blocks which were connected to the removed inports.