Manual

User Manual:

Open the PDF directly: View PDF .
Page Count: 3

Download
Open PDF In Browser	View PDF

TLACE Visualizer — User Manual
Simon Busard
December 7, 2011
TLACE Visualizer is a tree-like annotated counter-examples (TLACEs) visualizer and browser.
It displays TLACEs in a graph structure and allows their browsing. This manual gives a brief
description of the tool, its usage and features. It assumes that TLACE Visualizer is compiled and
launched.

How-to
The input format supported by TLACE Visualizer is given by the grammar at the end of this
manual. This format is an XML format containing tree-like annotated counter-examples. Several
counter-examples can be imported in TLACE Visualizer and accessed through to the tabulations
at the top of the tool.
When imported, the counter-example is displayed in a graph structure where each vertex is a
node of the counter-example and each edge a transition. The graph is laid out using a custom

1

layout designed to keep the structure of the counter-example, displaying vertical main path and
oblique branches. Parts of the graph can be rearranged by drag-and-drop.
Nodes information can be accessed by popup menus (right-clicking on the corresponding vertex).
This popup menu displays the values of state variables of the model in the state of the node. It also
gives its annotation and the list of branches. Each branch can be inspected as a path or fold/unfold
through this menu. When a branch is fold, it disappears of the graph with its sub-branches. It can
be unfolded again through the same menu.
The tool allows also to inspect a particular path in the graph. To do so, select a node with
CTRL pressed (or CMD for Mac OSX) and then select another node. If there is a path in the
graph from the first node to the second one, a side panel is opened and displays the information of
all nodes of the path.

Options
The tool has several options. Some options are common to imported counter-examples and located
in the top-level menu bar.
• Set default layout sets the layout used for future imported counter-examples.
• Set default info panel sets the way the path information are given.
• Open counter-examples fully folded asks the tool to display imported counter-examples
as a single initial node from which branches can be unfolded manually.
Other options are particular to each imported counter-example and located in the tabulations.
• Set layout changes the layout of the graph.
• Set info panel sets the way the path information are given for this counter-example.
• Display values on the graph allows the user to choose which state and input variables are
displayed on the graph, in the nodes and on the transitions, respectively.
• Show only changed variables, when activated, displays only variables which value changes
from the previous state in the list of nodes of the path description.

2

XML Format
XML

::= 
CNTEX
CNTEX
::= 
NODE

NODE
::= 
STATE
ATOMIC*
EXISTENTIAL*
UNIVERSAL*

STATE
::= 
VALUE+

VALUE
::= VAL
ATOMIC
::= 
EXISTENTIAL ::= 
PATH

| 
UNIVERSAL
::= 
PATH
::=NODE (INPUT NODE)+ LOOP?
INPUT
::=
VALUES*


VALUES*

LOOP
::= INPUT


3



---

Source Exif Data:

File Type                       : PDF
File Type Extension             : pdf
MIME Type                       : application/pdf
PDF Version                     : 1.5
Linearized                      : No
Page Count                      : 3
Producer                        : pdfTeX-1.40.12
Creator                         : TeX
Create Date                     : 2011:12:07 16:45:34+01:00
Modify Date                     : 2011:12:07 16:45:34+01:00
Trapped                         : False
PTEX Fullbanner                 : This is pdfTeX, Version 3.1415926-2.3-1.40.12 (TeX Live 2011) kpathsea version 6.0.1

EXIF Metadata provided by EXIF.tools