RT log viewer - overturetool/vdm-vscode Wiki

Opening The Log Viewer

The log viewer can be utilised in the context of a VDM-RT project. More specifically it can be used to display the events found in the log that is generated by executing a given launch configuration with the value enableLogging set to true in a VDM-RT project. Any logs that are generated will then be placed in the folder .generated/rtlogs of the project and named after the given launch configuration and time of execution. There might be two log file types in the folder, namely: .rtlog and the accompanying file type .rtlog.violations. If a log file of the type .rtlog is opened a prompt will appear asking if the log file should be displayed in the log viewer.

Utilising the Log Viewer

The interface and functionality of the log viewer closely resembles that of the log viewer tool found in Overture. The usage of the log viewer tool is detailed by the following GIF and its accompanying usage description.

Settings

By default the log viewer utilises colours from the current theme of the editor and elements in the log viewer are scaled relative to the current font size of the editor. This behaviour can be changed by the settings outlined below. The font family always follows that of the editor.

Setting Description Default Value
Scale With Editor Font Enabled: The size of the elements of the log viewer are scaled relative to the current font size of the editor. Disabled: The size of the elements of the log viewer are scaled relative to the font size defined by the log viewer setting Font Size. Enabled (true)
Match Theme Enabled: The colours utilised by the log viewer are from the current theme of the editor. Disabled: Predefined colours will be utilised by the log viewer. Enabled (true)
Font Size Defines the font size to be used for the relative scaling of the elements in the log viewer if the setting Scale With Font is disabled 15

The settings can be found at Settings > Extensions > VDM VSCode > Other.

Known issues

Due to size limitations of the underlying HTML canvas used for the diagrams found in the log viewer, it is possible that all events for a given time frame cannot be displayed. This can happen if either a large enough amount of objects are active on a single CPU for a single time frame or a large enough amount of events are present for a single time frame.

NOTE: Reducing the font size used for the scaling of elements in the log viewer might make it possible to fit all the events.