TVLA Release Notes
version 0.91, 4.2.2002

Changes since 0.9:

• Fixed a bug that caused the DOT output with messages to ignore -rotate for structures.
• Improved the DOT output of the CFG, so that the graph nodes are organized in a more intuitive manner.
• Added an option -canonstat that's used to collect statistical information about canonic names.
• Modified the TVP syntax to allow empty predicate update sections.
• Use tvla with one of the options -h, -help, ?, /? or no options to get version information and information about the available
  options.
• Nullary predicates are no longer presented as diamonds. A box containing the names of the nullary predicates serves instead.
  The names are colored according to the usual convention - black for 1, green for 1/2 and red for 0.
• A new option -trace can be used to create trace outputs to use with Alexsa.For convenience, new activation scripts -
  tvla_trace and tvmc_trace (for multithreading analyses) have been added.
• A new option -mode has been added to choose between analysis engines. Currently, the default is set to -mode tvla.
  A multithreading analysis engine can be chosen with the -mode tvmc. More information on TVMC will available soon, but for
  now consult the link. The -ddfs option can be used along with -mode tvmc to choose a double-DFS multithreading engine.
• A tvla diff utility, which can be used to compare two outputs. Use the tvla_diff activation script to get more information.
• The -tvs option can be used to create an output in TVS format (similar to the syntax used for .tvs files). This is useful in cases
  where the graphical presentation does not fit in the page and for comparing outputs.
• The option -quiet was added to avoid seeing information during analysis time. Some information is still printed to the console,
  and the -log option to direct it to a log file can be used to avoid any information being printed to the console.
• The -back option can be used to reverse the direction of CFG edges, which may be usefully for backward analyses.
• The -dot option can be used to create an output in DOT format. In the past, this output was printed to
  the standard output and redirected to a .dt file by the activation script. This version contains an activation script which uses
  the -dot option, which gives more control to the users.
• Various improvements and bug fixes for the DOT presentation (see the bug history for details).
• Various performance optimizations.
• More statistical information is presented, including memory usage and the number of messages that were encountered during
  analysis. If the -log option is used, then the log file also contains the command-line options which were passed to TVLA.
• A new option -sparse optimizes the Join and Blur algorithms for very sparse structures, i.e., structures with many predicates
  in which most predicate interpretations are 0. This is the case when a pre-processing is done by a front-end to find live variables
  and once a variable turns "dead" it is set to 0.
• The -skip option pre-processes the CFG before the main analysis starts. It does so to remove chains of do-nothing actions. Such
  chains typically arise when the input is created by a front-end.
• The option -x presents information about non-standard and experimental options. These options may not have been thoroughly
  tested and may contain bugs. Other options are intended for the use of TVLA developers.
• For the latest information access the TVLA home page.

Known issues and limitations: