UV Manual: System Structure
Warning
This page is under construction.
The UV system is built using the Tcl/Tk system. It consists of two main
parts, with which the user can interact in different ways:
- The
uvwish shell
- is an extension of the standard Tcl/Tk shell
wish. In
addition to all wish commands several UV specific
commands have been added. The user can interact directly with the
command line interface of the uvwish shell.
- The Graphical User Interface
- is entirely written as Tcl/Tk scripts on top of
uvwish.
Everything that can be done with the graphical user interface can
also be accomplished with the uvwish shell alone, although
often in a much less convenient way. On the other hand certain operations
of the uvwish shell are not (yet) accessible through the
graphical user interface.
The overall system structure of the UV system is illustrated in the following
figure:
As can be seen, the uvwish program itself consists of roughly
three parts:
- The Tcl/Tk Library and Parser
- provide all the regular
wish commands and the system
initialization, as well as the main event loop for the entire program.
- Specific UV Tcl Commands
- access the special functionality and data representations of the UV system
core through a well defined script command interface. Typical such
comands are
uv_init for initializing the UV workspace, and
uv_parse for parsing a string as a UV input (e.g. as a
property).
- The UV Workspace
- holds all the essential data objects generated and manipulated during a
verification session, such a formulae, programs, and properties. It
containes a BDD package for the symbolic representation of boolean
functions and many auxiliary data structures. It also implements the
actual system operations such as UV parsing and model checking.
There are also several scripts in addition to the executable
uvwish program that define how the UV system is executed:
uvwish.tk
- defines the entire graphical user interface. It is executed as last
part of the UV system setup. Alternative user interfaces can be
provided by setting the
UVINIT environment variable.
uvwish.init.tcl
- parses command line options, maintaines the preference file,
and controls the startup of the UV system.
It is not intended to be customized (however, the command line parsing
will have to be moved into a different customizable script).
~/.uvwishrc
- is a user supplied resource
script that can contain additional setup or customization scripts.
~/.uvwish-prefs
- is a preference file generated and maintained by the
uvwish.init.tcl script. It is not intended to be
edited directly by the user.
[Go back to the Manual Contents Page]
This page was last updated on 03-Nov-1995.
markus@cs.utexas.edu