TVLA bugs

1   Known Bugs

• Defining a message where the beginning of the message part may contain something that looks like a formula may result in a syntax error. For example,
  %message !(E(v) pvar(v)) ® pvar + " is possibly NULL..." results in a syntax error. A workaround for this is inserting "" after the implication sign. For example,
  %message !(E(v) pvar(v)) ® "" + pvar + " is possibly NULL..." solves the problem.
  
• Since the TVLA parser does its job in one-pass predicates need to be declared before they are used, e.g., when
  writing a nested foreach block containing predicate declarations with associated constraints TVLA may claim that the predicate was used but not declared. The workaround in this case is to separate the loop into two loops - the first for the predicates declarations and the second for the constraints definition.
  
• The Focus algorithm doesn't handle embedding.
  
  It is desired that the Focus algorithm remove structures when there are other structures, which embed them. (This is called the max operation in the parametric framework article). Using the -j2 option may help to reduce this problem.

2   Bug History

• 17/11/2001 A bug that caused Focus not to terminate when an unbound binary predicate formula is specified and the structure contains a summary node connected with an indefinite node (of the specified predicate). This caused Focus to continue bifurcating nodes and discovering new indefinite nodes over and over again.
  
  The revised Focus algorithm detects such conditions and aborts the execution.
  
  However, if -quiet is specified Focus recovers by not bifurcating any given summary node more than once. This is done by considering only the satisfying assignments of the input structure, such that, if a node is bifurcated then the new indefinite edges are not considered. One consequence of this is that in these situations Focus terminates, but the specified formula will not necessarily evaluate to a definite value.
  
  
• 1/8/2001 A bug in automatic constraint generation for instrumentation predicates.
  
  On certain inputs, such as is[sel,other](v) = E(v₁,v₂) (sel(v₁,v)   &   other(v₂,v)) the closure operator generates constraints with a mismatch between the free variables of the head and the free variables of the body and throws an exception. This is only a sanity check and does not necessarily indicates an error in the definition. This information is now revealed to the user only in debug mode (-d).
  
  
• 14/7/2001 A bug in debug mode output.
  
  The first coerce stage did not print its result (running TVLA with the -d option).
  
  
• 6/5/2001 A bug when focus reaches an indefinite edge between two summary nodes - an exception is thrown (Focus cannot continue working on this edge, since this will result in an infinite number of structures).
  After the fix, a warning message is output and if afterwards a similar case is encountered (almost always) no more messages are printed on this subject.
  
  
• 6/5/2001 A bug in the Focus algorithm in Single mode.
  
  Focusing on binary function predicates with definite edges pointing to maybe-active nodes resulted in structures without the definite edge.
  
  
• 6/5/2001 Nullary predicates were not abstraction predicates by default.
  
  
• 19/4/2001 A bug in the treatment of update formulae.
  
  In cases where variables on the left-hand side of the formula don't appear on the right-hand side as well.
  
  
• 31/12/2000 abs/nonabs was ignored for nullary predicates.

This document was translated from L^AT_EX by H^EV^EA.