RT log viewer

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. The following overviews are presented in the log viewer: architecture, execution, a number of CPU views (one for each deployed CPU) and a diagram legend.

Architecture overview

This view shows a diagram of the deployed CPU's and BUS'es and how they are connected.

Execution overview

This view shows a diagram of the execution events for each of the deployed CPU's and BUS'es for each timespan between the given start time and end time. In addition if any validation conjecture violations are found these are displayed in a table below the diagram. It is possible to navigate to the conjecture by double clicking on the src time or dest time in the table.

CPU overview

The CPU view shows a diagram of the events of the concrete objects deployed on a given CPU for each timespan between the given start time and end time.

Diagram legend

Shows the legend for the execution and CPU diagrams.

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

On Linux the prompt asking to open the log file in the log viewer might freeze. If this happens the user should instead use the command VDM: Open real-time log in log viewer accessed through the command palette.

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.