UV Manual: GUI Representation

Warning

This page is under construction.

Interface Components

In the following we describe the various parts of the standard graphical user interface of the UV system as it is supplied with the standard installation of the uvwish shell. The command line interface of uvwish is not included in this description.

When interacting with the UV system through its graphical interface the user deals with the following parts:

The Command Window: gives access to system commands, displays system messages, and allows the user to interactively parse input.
Document Windows: are created for each document file in use and allow the user to edit, save and parse documents.
The Program Table Window: lists all current programs and allows the user to examine them and to perform operations on them.
The Property Table Window: lists all current properties and allows the user to examine them and to perform operations on them.
The Expression Table Window: lists information about all current expressions.
Property Information Windows: displays status information about a selected property.

The Command Window

The command window consists of the following four parts arranged from top to bottom:

The Menu Bar: provides access to various system operations.
Command Buttons: invoke operations on the command window.
The System Message Area: displays system messages such as parser error messages or status messages.
The User Input Area: allows the user to interactively parse UV input.

An example of a typical command window is shown in the following figure:

The Command Menu

The menu bar contains one pull-down menu with the following operations:

File

The File menu offers commands for handling documents and terminating a session:

New: creates a document window for a new empty document.
Open...: prompts the user to locate a document file via a file selection dialog and creates a document window for that file.
Quit: terminates the UV program.

The Command Window Command Buttons

There are two buttons with the following operations:

Parse User Input: runs the UV parser on the entire content of the user input area of the command window. Status and error messages produced by the parser are displayed in the message area of the command window, the error position is indicated in the user input area by highlighting the token that caused the error.
Clear: clears both the message area and the user input area of the command window.

Document Windows

A document window provides the user with means for viewing and editing input to the UV system, and to filing and parsing operations on such input documents. A document window consists of the following three parts listed from top to bottom as the appear in the layout of the window:

Command Buttons: allow the user to perform filing and parsing operations on the document.
The Message Area: displays messages as a result of performing operations on the document.
The Document Content Area: is an editable text area where the user can write or modify the document content.

A typical document window is show in the following figure:

The Document Window Command Buttons

There are four buttons with the following operations:

Parse: runs the UV parser on the entire document content of the document window. Status and error messages produced by the parser are displayed in the message area of the document window, the error position is indicated in the document content area by highlighting the token that caused the error.
Close: closes the document window. Changes made to the document content that have not been saved are lost.
Save: saves the document to a file. If the document was opened from a file changes are saved to that file. If the document was newly created. the user is prompted for a new filename under which the document is to be saved.
Save As...: saves the document to a file, but always prompts the user for a filename under which the document is to be saved.
Clear Messages: clears the message area for the document window.

The Program Table Window

All programs currently in use are listed in the program table window. The window consists of the following three parts given in the top to bottom order as they appear in the layout of the window:

Command Buttons: allow the user to perform operations on selected programs.
Radio Buttons for Option Settings: can be used to specify options for how operations on programs are to be performed.
The List of Programs: is a scrollable list of all currently used programs with one entry of one line for each program. Programs in the list can be selected for performing operations on them.

An example of a program table window is shown in the following figure:

Program Table Command Buttons

There is currently one command button with the following operation:

Compute Strongest Invariant

Program Table Options

This set of radio buttons allows the user to specify which technique is to be used when computing the strongest invariants of programs. Three options are available:

Frontier Forward: selects forward chaining using the frontier set. This is often the fastest and most space efficient way of computing the strongest invariant.
Forward: is similar to frontier forward chaining, with the only difference that at any iteration step all states reached so far are subjected to the successor state computation, as opposed to only those states that had been added in the previous iteration.
Iterative Squaring: selects iterative squaring over the transition relation. Although this technique is potentially converging exponentially faster than the above two methods, the intermediate results generated often grow too big to be practical.

The Program Table List

Each entry denotes one program currently in use and contains the following information:

a unique external name for the program of the form #prog<num>,
the program name as given in the program text,
an indicator for the invariant established so far for the program.

The invariant indicator can be any of the following three:

type invariant: indicates that only the type invariant has been established for the program,
current invariant: indicates that some invariant stronger than the type invariant has been established for the program,
strongest invariant: indicates that the strongest invariant for the program has been computed.

Program entries are selected for subsequent operations with the first mouse button, or with the first mouse button while holding down the shift key to extend an already made selection.

The Property Table Window

All properties currently in use are listed in the property table window. The window consists of the following three parts given in the top to bottom order as they appear in the layout of the window:

Command Buttons: allow the user to perform operations on selected properties.
Radio Buttons for Option Settings: can be used to specify options for how operations on properties are to be performed.
The List of Properties: is a scrollable list of all currently used properties with one entry of one line for each property. Propertiess in the list can be selected for performing operations on them.

An example of a property table window is shown in the following figure:

Property Table Command Buttons

There is currently one command button with the following operation:

Check Selected Properties

Property Table Options

This set of radio buttons allows the user to specify which invariant is to be used when invoking the model checker on properties. Three options are available:

Type: selects the type invariant of the program associated with each property to be used. The type invariant is the invariant derived from the program text asserting that every program variable takes on values of its type only.
Current: selectes the current invariant of the program associated with each property to be used. The current invariant is the conjunction of all invariants so far established for the program.
Strongest: selects the strongest invariant (if it has been computed) of the program associated with each property to be checked. The strongest invariant corresponds to the set of reachable states of the program.

The Property Table List

Each entry denotes one property currently in use and contains the following information:

a unique external name for the property of the form #prop<num>,
the name of the program associated with the property,
the checking status of the property,
a textual representation of the property.

The checking status of a property can be one of the following four:

new: indicates that no checking attempt has been made for the property.
?: indicates that the property has not been proved yet to be satisfied by the associated program, but that there might be a suitably strong invariant with respect to which the property could still be proved.
ok: indicates that the property has been proved to be satisfied by the associated program.
fail: indicates that the property has been proved to be not satisfied by the associated program by checking it with respect to the strongest invariant of the program, and as such is not valid for the associated program.

Property entries are selected for subsequent operations with the first mouse button, or with the first mouse button while holding down the shift key to extend an already made selection. Double clicking on a property entry with the first mouse button furthermore brings up a property info window for that property containing more detailed information about the checking status.

The Expression Table Window

All expression currently in use are listed in the expression table window. The window consists of a list of entries of one line for each expression.

An example of an expression table window is shown in the following figure:

Each entry denotes one expression currently in use and contains the following information:

a unique external name for the expression of the form #expr<num>,
the type of the expression,
value information about the expression (for constants this is a literal value, otherwise it is a number in square brackets indicating the BDD size of the internal representation of the expression),
a textual representation of the expression.

Property Information Windows

For each property listed in the property table window a property info window can be displayed by double-clicking on the entry of the property in the property table list.

The property info window displays more detailed information about the property and is useful for analyzing model checker output and for debugging properties and their programs.

The information presented in a property info window includes

the name of the program associated with the property,
a textual representation of the property,
a list of status items, each providing information about a certain aspect of the checking status of the property.

An example of a property info window is shown in the following figure:

Property Information Status Information

Each status item in the status list of the property info window provides some information about the checking status of the property. Each entry is identified by a label.

Some of these status items have additional information available in the form of some relevant expression. If such an expression is present a button labeled Add Expr appears at the right of the status item line. Pressing that button causes the expression to be transfered to the expression table window, by which it becomes available as an external name for further investigation.

The following table lists all status items by their labels and describes the information available through them:

Status: shows the checking status of the property as displayed in the property table window.
Invariant: identifies the kind of invariant used for checking the property.
The checking invariant is available by pressing the Add Expr button.
Implication: states the result of the implication check required for co and invariant properties.
A predicate characterizing all states (within the checking invariant) falsifying the implication is available by pressing the Add Expr button.
Safety: states the result of the safety check required for co, unless, stable, invariant, constant and ensures properties, in particular it names a program statement violating the condition (if there is any).
If there is a violating statement then a predicate characterizing all states (within the checking invariant) from which an execution of the statement violates the safety condition is available by pressing the Add Expr button.
Transition: states the result of the helpful transition check required by transient and ensures properties, in particular it names a helpful program statement if present.
Value: shows a value for the expression of a constant property for which the stability condition is violated (if there is such a value).
If there is a value that is changed by some statement, then such a value is available by pressing the Add Expr button.
Iterations: presents the number of outer (least) and inner (greatest) fixpoint iterations in the checking of leads-to properties.
A predicate characterizing all states (within the checking invariant) for which there is a fair program execution not satisfying the leads-to property is available by pressing the Add Expr button.

Pressing the Close button closes the property info window.

[Go back to the Manual Contents Page]

This page was last updated on 20-Nov-1995.

markus@cs.utexas.edu